Modular progress proofs of asynchronous programs
Ernest Samuel Cohen · 1993
The usual way to reason about a concurrent program is to prove that it preserves certain state predicates; such predicates are said to be stable. However, many important techniques of concurrent program construction (e.g., pipelining) depend on commutativity conditions between actions, which cannot be directly expressed using stability; in fact, these techniques lie beyond ordinary state-based program reasoning. In this thesis, we show how to handle these techniques in a natural way by generalizing stability of predicates to stability of predicate transformers. Based on this generalization, we give semantic conditions under which we can that a program inherits progress properties from one of its components, and a rich calculus for constructing these components. Moreover, if a decoupled component restores the system to some predicate, then we can pretend that the predicate is stable (in a weak sense), and thus simplify the stats that have to be considered in analysing the program. We use our theory to reprove and extend some of Misra's results on loosely-coupled programs, and to construct new program-logical proofs of the window protocol for communication across noisy channels and the tree protocol for serializable transaction processing.