We are interested in the verification, using model checking, of distributed programs that communicate asynchronously over standard communicationAPIs such as MPI. This is feasible only if the set of executions that the model checker explores is aggressively reduced to a subset of representative executions, using techniques such as dynamic partial-order reduction. We propose a small set of core primitives in terms of which such APIs can be defined and formally specify these primitives in TLA+.From this specification we derive theorems about the (in)dependence of invocations of the primitives, and use them in a DPOR-based verifier that runs within SimGrid, a simulation framework for distributed programming.Our preliminary experimental results indicate that we obtain good reductions, even though complex network operations are implemented in terms of the core commu nication primitives.
展开▼
