Collective Assertions

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.

@InProceedings{siegel-zirkel:2011:assert,
  Author = {Stephen F. Siegel and Timothy K. Zirkel},
  Crossref = {vmcai2011},
  Pages = {387--402},
  Title = {Collective Assertions}
}
@Proceedings{vmcai2011,
  Booktitle = {Verification, Model Checking, and Abstract Interpretation: 12th International Conference, {VMCAI} 2011, Austin, TX, January 23--25, 2011, Proceedings},
  Title = {Verification, Model Checking, and Abstract Interpretation: 12th International Conference, {VMCAI} 2011, Austin, TX, January 23--25, 2011, Proceedings},
  Editor = {Ranjit Jhala and David Schmidt},
  Series = {Lecture Notes in Computer Science},
  Volume = {6538},
  Year = 2011
}