On the Lamb Vector Divergence in Navier-Stokes Flows|
C.W. Hamman, J.C. Klewicki, R.M. Kirby. In Journal of Fluid Mechanics, Vol. 610, pp. 261--284. 2008.
Unified Volume Format: A General System For Efficient Handling Of Large Volumetric Datasets|
J. Krüger, K. Potter, R.S. MacLeod, C.R. Johnson. In Proceedings of IADIS Computer Graphics and Visualization 2008 (CGV 2008), pp. 19--26. 2008.
PubMed ID: 20953270
With the continual increase in computing power, volumetric datasets with sizes ranging from only a few megabytes to petascale are generated thousands of times per day. Such data may come from an ordinary source such as simple everyday medical imaging procedures, while larger datasets may be generated from cluster-based scientific simulations or measurements of large scale experiments. In computer science an incredible amount of work worldwide is put into the efficient visualization of these datasets. As researchers in the field of scientific visualization, we often have to face the task of handling very large data from various sources. This data usually comes in many different data formats. In medical imaging, the DICOM standard is well established, however, most research labs use their own data formats to store and process data. To simplify the task of reading the many different formats used with all of the different visualization programs, we present a system for the efficient handling of many types of large scientific datasets (see Figure 1 for just a few examples). While primarily targeted at structured volumetric data, UVF can store just about any type of structured and unstructured data. The system is composed of a file format specification with a reference implementation of a reader. It is not only a common, easy to implement format but also allows for efficient rendering of most datasets without the need to convert the data in memory.
Implementing Efficient Dynamic Formal Verification Methods for MPI Programs|
S. Vakkalanka, M. DeLisi, G. Gopalakrishnan, R.M. Kirby, R. Thakur, W. Gropp. In Recent Advances in Parallel Virtual Machine and Message Passing Interface Lecture Notes in Computer Science, Dublin, Ireland, Vol. 5205, pp. 248--256. September, 2008.
We examine the problem of formally verifying MPI programs for safety properties through an efficient dynamic (runtime) method in which the processes of a given MPI program are executed under the control of an interleaving scheduler. To ensure full coverage for given input test data, the algorithm must take into consideration MPI’s out-of-order completion semantics. The algorithm must also ensure that nondeterministic constructs (e.g., MPI wildcard receive matches) are executed in all possible ways. Our new algorithm rewrites wildcard receives to specific receives, one for each sender that can potentially match with the receive. It then recursively explores each case of the specific receives. The list of potential senders matching a receive is determined through a runtime algorithm that exploits MPI’s operation ordering semantics. Our verification tool ISP that incorporates this algorithm efficiently verifies several programs and finds bugs missed by existing informal verification tools.
Scheduling Considerations for Building Dynamic Verification Tools for MPI|
S. Vakkalanka, M. DeLisi, G. Gopalakrishnan, R.M. Kirby. In Proceedings of the 6th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, Seattle, WA, PADTAD '08, Vol. 3, ACM, pp. 1--6. 2008.
Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings|
S. Vakkalanka, G. Gopalakrishnan, R.M. Kirby. In Computer Aided Verification Lecture Notes in Computer Science , Vol. 5123, pp. 66--79. July, 2008.
Dynamic verification methods are the natural choice for debugging real world programs when model extraction and maintenance are expensive. Message passing programs written using the MPI library fall under this category. Partial order reduction can be very effective for MPI programs because for each process, all its local computational steps, as well as many of its MPI calls, commute with the corresponding steps of all other processes. However, when dependencies arise among MPI calls, they are often a function of the runtime state. While this suggests the use of dynamic partial order reduction (DPOR), three aspects of MPI make previous DPOR algorithms inapplicable: (i) many MPI calls are allowed to complete out of program order; (ii) MPI has global synchronization operations (e.g., barrier) that have a special weak semantics; and (iii) the runtime of MPI cannot, without intrusive modifications, be forced to pursue a specific interleaving because of MPI’s liberal message matching rules, especially pertaining to ‘wildcard receives’. We describe our new dynamic verification algorithm ‘POE’ that exploits the out of order completion semantics of MPI by delaying the issuance of MPI calls, issuing them only according to the formation of match-sets, which are ample ‘big-step’ moves. POE guarantees to manifest any feasible interleaving by dynamically rewriting wildcard receives by specific-source receives. This is the first dynamic model-checking algorithm with reductions for (a large subset of) MPI that guarantees to catch all deadlocks and local assertion violations, and is found to work well in practice.
A Formal Approach to Detect Functionally Irrelevant Barriers in MPI Programs|
S. Sharma, S. Vakkalanka, G. Gopalakrishnan, R.M. Kirby, R. Thakur, W. Gropp. In Proceedings of EuroPVM-MPI 2008, Dublin, Ireland, Vol. 5205, pp. 265--273. September, 2008.
We examine the unsolved problem of automatically and efficiently detecting functionally irrelevant barriers in MPI programs. A functionally irrelevant barrier is a set of MPI_Barrier calls, one per MPI process, such that their removal does not alter the overall MPI communication structure of the program. Static analysis methods are incapable of solving this problem, as MPI programs can compute many quantities at runtime, including send targets, receive sources, tags, and communicators, and also can have data-dependent control flows. We offer an algorithm called Fib to solve this problem based on dynamic (runtime) analysis. Fib applies to MPI programs that employ 24 widely used two-sided MPI operations. We show that it is sufficient to detect barrier calls whose removal causes a wildcard receive statement placed before or after a barrier to now begin matching a send statement with which it did not match before. Fib determines whether a barrier becomes relevant in any interleaving of the MPI processes of a given MPI program. Since the number of interleavings can grow exponentially with the number of processes, Fib employs a sound method to drastically reduce this number, by computing only the relevant interleavings. We show that many MPI programs do not have data dependent control flows, thus making the results of Fib applicable to all the input data the program can accept.
Building Blocks for Computer Vision with Stochastic Partial Differential Equations|
T. Preusser, H. Scharr, K. Krajsek, R.M. Kirby. In International Journal of Computer Vision, Vol. 80, No. 3, Springer, pp. 375--405. July, 2008.
Examination and Analysis of Implementation Choices within the Material Point Method (MPM)|
M. Steffen, P.C. Wallstedt, J.E. Guilkey, R.M. Kirby, M. Berzins. In Computer Modeling in Engineering & Sciences, Vol. 31, No. 2, pp. 107--127. 2008.
CRA-NIH Computing Research Challenges in Biomedicine Workshop Recommendations|
D. Reed, C.R. Johnson. Note: Computing Research Association (CRA), 2007.
Dynamically identifying and tracking contaminants in water bodies|
C.C. Douglas, M.J. Cole, P. Dostert, Y. Efendiev, R.E. Ewing, G. Haase, J. Hatcher, M. Iskandarani, C.R. Johnson, R.A. Lodder. In Proceedings of the 7th International Conference on Computational Science (ICCS) 2007, Part I, Beijing, China, Lecture Notes in Computer Science (LNCS), Vol. 4887, Edited by Y. Shi and G.D. van Albada and P.M.A. Sloot and J.J. Dongarra, Springer-Verlag, Berlin Heidelberg, pp. 1002--1009. May, 2007.
Dynamic data-driven application systems for empty houses, contaminat tracking, and wildland fireline prediction|
C.C. Douglas, D. Bansal, J.D. Beezley, L.S. Bennethum, S. Chakraborty, J.L. Coen, Y. Efendiev, R.E. Ewing, J. Hatcher, M. Iskandarani, C.R. Johnson, M. Kim, D. Li, R.A. Lodder, J. Mandel, G. Qin, A. Vodacek. In Grid-Based Problem Solving Environments, IFIP series, Edited by P.W. Gaffney and J.C.T. Pool, Springer-Verlag, Berlin, pp. 255-272. 2007.
BioMesh3D: A Meshing Pipeline for Biomedical Models|
SCI Institute Technical Report, M. Callahan, M.J. Cole, J.F. Shepherd, J.G. Stinstra, C.R. Johnson. No. UUSCI-2007-009, University of Utah, 2007.
Hexahedral Mesh Generation for Biomedical Models in SCIRun|
SCI Institute Technical Report, J.F. Shepherd, C.R. Johnson. No. UUSCI-2007-008, University of Utah, 2007.
A Meshing Pipeline for Biomedical Computing|
M. Callahan, M.J. Cole, J.F. Shepherd, J.G. Stinstra, C.R. Johnson. In Engineering with Computers, Special Issue on Computational Bioengineering, pp. (in press). 2007.
NSF Blue Ribbon Panel Report on Simulation Based Engineering Science|
J.T. Oden, J. Fish, C.R. Johnson, A. Laub, D. Srolovitz, T. Belytschko, T.J.R. Hughes, D. Keys, L. Petzold, S. Yip. Note: NSF Report, 2006.
Purpose: To explore the emerging discipline of Simulation Simulation-Based Engineering Science, its major components, its importance to the nation, the challenges and barriers to its advancement, and to recommend to the NSF and the broader community concerned with science and engineering in the United States, steps that could be taken to advance development in this discipline.
Towards Stable Coupling Methods for High-Order Discretizations of Fluid-Structure Interaction: Algorithms and Observations|
R.M. Kirby, Z. Yosibash, G.E. Karniadakis. In Journal of Computational Physics, Vol. 223, No. 2, pp. 489--518. 2006.
A One-Dimensional Model of the Navier-Stokes|
SCI Institute Technical Report, H. Marmanis, C.W. Hamman, R.M. Kirby. No. UUSCI-2006-012, University of Utah, 2006.
Biomedical Computing and Visualization|
C.R. Johnson, D.M. Weinstein. In Proceedings of the Twenty-Ninth Australasian Computer Science Conference (ACSC2006): Conferences in Research and Practice in Information Technology (CRPIT), Hobart, Australia, Vol. 48, Edited by Vladimir Estivill-Castro and Gill Dobbie, pp. 3-10. 2006.
Advanced Reaction-Diffusion Models for Texture Synthesis|
A.R. Sanderson, R.M. Kirby, C.R. Johnson, L. Yang. In Journal of Graphics Tools, Vol. 11, No. 3, pp. 47--71. 2006.
Parallel and Distributed Model Checking in Eddy|
I. Melatti, R. Palmer, G. Sawaya, Y. Yang, R.M. Kirby, G. Gopalakrishnan. In Model Checking Software: Proceedings of the 13th International SPIN Workshop (SPIN 2006), Austria, Vol. 3925/2006, pp. 108--125. 2006.