Memory Consistency and Program Verification
Last modified: Wed Oct 20 21:51:45 2010 GMT.
Formal reasoning about concurrent programs is usually done with the assumption that the underlying memory model is sequentially consistent, i.e. the execution outcome is equivalent to an interleaving of instructions according to the program order. However, memory models in reality are weaker in order to accommodate compiler and hardware optimizations. To simplify the reasoning, many memory models provide a guarantee that data-race-free programs behave in a sequentially consistent manner, the so-called DRF-guarantee. The DRF-guarantee removes the burden of reasoning about relaxations when the program is well-synchronized. It is common belief that the current tools for program verification, such as Concurrent Separation Logic (CSL), yield DRF-programs. In principle, they can rely on the DRF-guarantee to ignore memory model issues. However, there is no rigorous evidence for that, given the fact that the work on memory models is not founded with a level of formalism adequate for program verification. It is a semantic gap between the two fields. This thesis provides seminal work towards bridging them together.
In this thesis, we formalize memory consistency models by giving a parameterized operational semantics to a concurrent programming language. Behaviors of a program under a relaxed memory model are defined as behaviors of a set of related programs under the sequentially consistent model. This semantics is parameterized in the sense that different memory models can be obtained by using different relations between programs. We present one particular relation, called command subsumption, that we believe accounts for many memory models and sequential optimizations. We then show that the derived relaxed memory model provides the DRF-guarantee, using, as intermediate, an auxiliary mixed-step semantics that is compatible with the subsumption relation. Finally, we bridge the soundness of CSL, and variations, to our relaxed semantics. We establish the soundness following a standard semantic approach. This shows that, indeed, programs verified with CSL are race-free and their execution in the relaxed memory model exhibits the same set of behaviors as in the interleaved semantics.
Copyright © 1996-2017 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science