We introduce the notion of collective assertions for message-passing-based parallel programs with distributed memory, such as those written using the Message Passing Interface. A single collective assertion comprises a set of locations in each process and an expression on the global state. The semantics are defined as follows: whenever control in a process reaches one of the locations, a "snapshot"of the local state of that process is sent to a coordinator; once a snapshot has been received from each process, the expression is evaluated on the global state formed by uniting the snapshots. We have extended the Toolkit for Accurate Scientific Software (TASS), a verifier based on symbolic execution and explicit state enumeration, to check that collective assertions hold on all possible executions of a C/MPI program. We give several examples of such programs, show that many properties of them are naturally expressed as collective assertions, and use TASS to verify or refute these. © 2011 Springer-Verlag.
CITATION STYLE
Siegel, S. F., & Zirkel, T. K. (2011). Collective assertions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6538 LNCS, pp. 387–402). https://doi.org/10.1007/978-3-642-18275-4_27
Mendeley helps you to discover research relevant for your work.