Pretending Atomicity

Reasoning about concurrent systems is simpler if they have fewer separate atomic actions. To simplify reasoning about systems, we’d like to be able to combine multiple small atomic actions into a single large one. This process is called reduction. This paper contains a reduction theorem for multiprocess programs. It was accepted for publication, subject to minor revisions, in ACM Transactions on Programming Languages and Systems. However, after writing it, I invented TLA, which enabled me to devise a stronger and more elegant reduction theorem. Schneider and I began to revise the paper in terms of TLA. We were planning to present a weaker, simpler version of the TLA reduction theorem that essentially covered the situations considered in this report. However, we never finished that paper. A more general TLA reduction theorem was finally published in [123].