Hexahedral Mesh Generation for Biomedical Models in SCIRun|
J.F. Shepherd, C.R. Johnson. In Engineering with Computers, Vol. 25, No. 1, pp. 97--114. 2009.
Comparison of Consistent Integration Versus Adaptive Quadrature for Taming Aliasing Errors|
SCI Technical Report, H. Mirzaee, C. Eskilsson, S.J. Sherwin, R.M. Kirby. No. UUSCI-2009-008, SCI Institute, University of Utah, 2009.
The SCIJump Framework for Parallel and Distributed Scientific Computing|
S.G. Parker, K. Damevski, A. Khan, A. Swaminathan, C.R. Johnson. In Advanced Computational Infrastructures for Parallel and Distributed Adaptive Applications, Edited by Manish Parashar and Xiaolin Li and Sumir Chandra, Wiley-Blackwell, pp. 149--170. 2009.
A Meshing Pipeline for Biomedical Models|
M. Callahan, M.J. Cole, J.F. Shepherd, J.G. Stinstra, C.R. Johnson. In Engineering with Computers, Vol. 25, No. 1, SpringerLink, pp. 115-130. 2009.
Formal Verification of Practical MPI Programs|
A. Vo, S. Vakkalanka, M. Delisi, G. Gopalakrishnan, R.M. Kirby, R. Thakur. In Proceedings of 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), Raleigh, NC, pp. 261--270. February 14-18, 2009.
Particle-based Sampling and Meshing of Surfaces in Multimaterial Volumes|
M.D. Meyer, R.T. Whitaker, R.M. Kirby, C. Ledergerber, H. Pﬁster. In IEEE Transactions on Visualization and Computer Graphics, Vol. 14, No. 6, pp. 1539--1546. 2008.
Hexahedral Mesh Generation Constraints|
J.F. Shepherd, C.R. Johnson. In Journal of Engineering with Computers, Vol. 24, No. 3, pp. 195--213. 2008.
Filtering in Legendre Spectral Methods|
J.S. Hesthaven, R.M. Kirby. In Mathematics of Computation, Vol. 77, No. 263, pp. 1425--1452. 2008.
An Approach to Formalization and Analysis of Message Passing Libraries|
R. Palmer, M. DeLisi, G. Gopalakrishnan, R.M. Kirby. In Proceedings of the 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007), Berlin, Germany, Vol. 4916/2008, Note: Awarded Best Paper., pp. 164--181. 2008.
Application of Stochastic Finite Element Methods to Study the Sensitivity of ECG Forward Modeling to Organ Conductivity|
S.E. Geneser, R.M. Kirby, R.S. MacLeod. In IEEE Transations on Biomedical Engineering, Vol. 55, No. 1, pp. 31--40. January, 2008.
A Comparison of Implicit Solvers for the Immersed Boundary Equations|
E.P. Newren, A.L. Fogelson, R.D. Guy, R.M. Kirby. In Computer Methods in Applied Mechanics and Engineering, Vol. 197, No. 25--28, pp. 2290--2304. 2008.
Investigation of Smoothness-Increasing Accuracy-Conserving Filters for Improving Streamline Integration Through Discontinuous Fields|
M. Steffen, S. Curtis, R.M. Kirby, J.K. Ryan. In IEEE Transactions on Visualization and Computer Graphics, Vol. 14, No. 3, pp. 680--692. 2008.
Analysis and Reduction of Quadrature Errors in the Material Point Method (MPM)|
M. Steffen, R.M. Kirby, M. Berzins. In International Journal for Numerical Methods in Engineering, Vol. 76, No. 6, pp. 922--948. 2008.
Volumetric Parameterization and Trivariate B-spline Fitting using Harmonic Functions|
T. Martin, E. Cohen, R.M. Kirby. In Proceedings of ACM Solid and Physical Modeling, Stony Brook, NY, Note: Awarded Best Paper, pp. 269-280. 2008.
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.