SCI Publications

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.

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.

The stability and accuracy of the generalized interpolation material point (GIMP) Method is measured directly through carefully-formulated manufactured solutions over wide ranges of CFL numbers and mesh sizes. The manufactured solutions are described in detail. The accuracy and stability of several time integration schemes are compared via numerical experiments. The effect of various treatments of particle “size” are also considered. The hypothesis that GIMP is most accurate when particles remain contiguous and non-overlapping is confirmed by comparing manufactured solutions with and without this property.

Keywords: Material point method, Manufactured solutions, Time integration, MPM, GIMP, MMS, PIC

The problem of body fitting meshes that are both adaptive and geometrically accurate is important in a variety of biomedical applications in a multitude of clinical settings, including electrocardiology, neurology, and orthopedics. Adaptivity is necessary because of the combination of large-scale and smallscale structures (e.g. relatively small blood vessels spanning a human head). Geometric accuracy is important for several reasons. In some cases, such as computational fluid dynamics, the fine-scale structure of the fluid domain is important for qualitative and quantitative accuracy of the solutions. More generally, finite element approximations of elliptic problems with rough coefficients require increased spatial resolution normal to material boundaries [3]. The problem of constructing meshes from biomedical images is particularly difficult because of the complexity and irregularity of the structures, and thus tuning or correcting meshes by hand is quite difficult and time consuming. Many researchers and, indeed, commercial products simply subdivide the underlying hexahedral image grid and assign material properties to tetrahedra based on standard decomposition of each hexahedron into tetrahedra.

This paper presents a small case study of the results of a recently developed method for multimaterial, tetrahedral meshing of biomedical volumes [6]. The method uses an iterative relaxation of surface point point positions that are constrained to subsets of the volume that correspond to boundaries between different materials. In this paper we briefly review the method and present results on a set of MRI head images for use in bioelectric field simulation and source localization.

Numerical integration formulas in n-dimensional nonsymmetric Euclidean space of degree two, consisting of n+1 equally weighted points, are discussed, for a class of integrals often encountered in statistics. This is an extension of Stroud's theory [A.H. Stroud, Remarks on the disposition of points in numerical integration formulas, Math. Comput. 11 (60) (1957) 257–261; A.H. Stroud, Numerical integration formulas of degree two, Math. Comput. 14 (69) (1960) 21–26]. Explicit formulas are given for integrals with nonsymmetric weights. These appear to be new results and include the Stroud's degree two formula as a special case.

Keywords: Numerical integration, Cubature formulas

The topic of studying the growth of human brain development has become of increasing interests in the neuroimaging community. Cross-sectional studies may allow comparisons between means of different age groups, but they do not provide any growth model that integrates the continuum of time, nor do they present any information about how individuals/population change over time. Longitudinal data analysis method arises as a strong tool to address these questions. In this paper, we use longitudinal analysis methods to study tissue development in early brain growth; a novel approach of multivariate longitudinal analysis is applied to study the associations between the growth of different brain tissues. We present in this paper the methodologies to statistically study scalar (univariate) and vector (multivariate) longitudinal data, and our exploratory results in the study of neonatal-pediatric brain tissue development. We obtained growth curves as a quadratic function of time for all three tissues. The quadratic terms were then tested to be statistically signicant, showing that there was indeed a quadratic growth of tissues in early brain development. Moreover, our result shows that there is a positive correlation between repeated measurements of any single tissue, and among those of different tissues. Our approach is generic in natural and thus can be applied to any longitudinal data with multiple outcomes, even brain structures. Also, our joint mixed model is flexible enough to allow incomplete and unbalanced data, i.e. subjects do not need to have the same number of measurements, or be measured at the exact time points.

Keywords: ucnia

In applying stateless model checking methods to realistic multithreaded programs, we find that stateless search methods are ineffective in practice, even with dynamic partial order reduction (DPOR) enabled. To solve the inefficiency of stateless runtime model checking, this paper makes two related contributions. The first contribution is a novel and conservative light-weight method for storing abstract states at runtime to help avoid redundant searches. The second contribution is a stateful dynamic partial order reduction algorithm (SDPOR) that avoids a potential unsoundness when DPOR is naively applied in the context of stateful search. Our stateful runtime model checking approach combines light-weight state recording with SDPOR, and strikes a good balance between state recording overheads, on one hand, and the elimination of redundant searches, on the other hand. Our experiments confirm the effectiveness of our approach on several multithreaded benchmarks in C, including some practical programs.

The Utah normal heptane mechanism compiled from submechanisms in the literature was extended into a detailed normal decane combustion mechanism, which is a subset of the Utah surrogate mechanisms. Few species have greater impact on the concentrations of other species than the allyl radical CH₂CH=CH₂ . Reactions involving the allyl radical and its isomers determine the concentration levels of all olefins, most higher unsaturated species, and benzene. To correctly predict the concentration of benzene, the reaction rates involving allyl-radical-related species need to be accurate and the concentration profiles of these species need to be satisfactory. Kinetic rates found in the literature are compared in the current work for various reference reactions that involve the allylic radicals. The improvements in numerical predictions of unsaturated species are achieved after a rigorous study in finding reliable reaction rates and kinetic correlations between various species. Some of these rates are adopted as the generic rates that have been used in the Utah surrogate mechanisms in previous studies. The modified mechanism is able to predict the concentration profiles of unsaturated species in n-decane and n-heptane flames with good numerical accuracy. The concentrations of these species are closely related to those of various allylic radicals, and reliable kinetics of allylic reactions are critical in predicting the concentrations of benzene and higher aromatics.

To study the formation of air pollutants and soot precursors (e.g., acetylene, 1,3-butadiene, benzene, and higher aromatics) from aliphatic and aromatic fractions of gasoline fuels, the Utah Surrogate Mechanisms is extended to include submechanisms of gasoline surrogate compounds using a set of mechanism generation techniques. The mechanism yields very good predictions of species concentrations in premixed flames of n-heptane, isooctane, benzene, cyclohexane, olefins, oxygenates, and gasoline using a 23-component surrogate formulation. The 1,3-butadiene emission comes mainly from minor fuel fractions of olefins and cyclohexane. The benzene formation potential of gasoline components shows the following trends as functions of (i) chemical class: n-paraffins isoparaffns olefins nphthalnes alkylbenzees cycloparaffis toluene; (ii)carbon number: n-butane < n-pentane < n-hexane; and (iii) branching: n-hexane ne 2,4-trimethylpentane utane. In contrast, fuel structure is not the main factor in determining acetylene formation. Therefore, matching the benzene formation potential of the surrogate fuel to that produced by the real fuel should have priority when selecting candidate surrogate components for combustion simulations.