Moving around: Lipton's reduction for TSO - (Regular submission)

Abstract

We generalize Lipton's reduction theory, hitherto limited to SC, for TSO programs. We demonstrate the use of our theory by specifying the conditions under which a particular write is SC-like (i.e. placing a fence immediately after the write does not constrain the behavior of the overall program) and a library implementation can be safely used (i.e. compositionality). Our theory is complete: a program has only SC behaviors iff there is a proof that establishes that every write in the program is SC-like. We adapt the notion of program abstraction to TSO analysis via our theory. We define precisely what is meant by abstraction, and propose a methodology by which one can obtain via abstraction SC summaries of a program which may have non-SC behaviors. Finally, we show how checking whether a write instruction is SC-like can be mechanized. We describe a transformation in which the execution of each thread of the original program (under TSO) is simulated by the execution of two tightly coupled threads in the new program (under SC).