Transfer Principles for Reasoning about Concurrent Programs

Stephen Brookes
Department of Computer Science
Carnegie Mellon University

In previous work we have developed a transition trace
semantic framework, suitable for shared-memory parallel programs and
asynchronously communicating processes, and abstract enough to support
compositional reasoning about safety and liveness properties. We now use
this framework to formalize and generalize some techniques used in
the literature to facilitate such reasoning.
We identify a sequential-to-parallel transfer theorem which, when applicable,
allows us to replace a piece of a parallel program with another code fragment
which is sequentially equivalent, with the guarantee that the safety and
liveness properties of the overall program are unaffected.
Two code fragments are said to be sequentially equivalent if
they satisfy the same partial and total correctness properties.
We also specify both coarse-grained and fine-grained versions of trace
semantics, assuming different degrees of atomicity, and we provide a
coarse-to-fine-grained transfer theorem which, when applicable, allows
replacement of a code fragment by another fragment which is coarsely
equivalent, with the guarantee that the safety and liveness properties of the
overall program are unaffected even if we assume fine-grained atomicity. Both of these results
permit the use of a simpler, more abstract semantics, together with
a notion of semantic equivalence which is easier to establish, to facilitate
reasoning about the behavior of a parallel system which would normally require
the use of a more sophisticated semantic model.