Transfer Principles for Reasoning 
about Concurrent Programs 

Stephen Brookes 
Carnegie Mellon University 

Abstract 
In previous work we developed a transition trace semantic model, 
suitable for shared-memory parallel programs as well as networks of 
asynchronous communicating processes, abstract enough to support 
compositional reasoning about safety and liveness properties. We now 
use this framework to formalize and generalize some techniques used 
more or less informally in the literature to facilitate reasoning about 
the behavior of concurrent systems, typically without explicit atten- 
tion to semantic foundations. Speciﬁcally, we identify a key sequential- 
to-paral lel transfer theorem which, when applicable, allows us to re- 
place a piece of a parallel program with another piece which is se- 
quential ly equivalent, with the guarantee that the safety and liveness 
properties of the overall program are unaﬀected. 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 ﬁne-grained version of trace semantics, assuming diﬀerent degrees 
of atomicity, and we provide a coarse-to-ﬁne-grained transfer theorem 
which, when applicable, allows replacement of a code fragment by an- 
other fragment which is coarsely equivalent, with the guarantee that 
the safety and liveness properties of the overall program are unaﬀected 
even if we assume ﬁne-grained atomicity. Both of these results permit 
the use of a simpler, more abstract semantics, together with a no- 
tion of semantic equivalence which is easier to establish, to facilitate 
reasoning about the behavior of a parallel system.