An Operational Relaxed Memory Model And Program Logic For Concurrency Verification

A memory model of a programming language specifies how memory accesses are made during program execution. It serves as a contract between programmers and the language implementation. In real world, most of architectures and compilers are de-signed based on the assumption of relaxed memory models, which means memory ac-cesses doesn’t rigorously follow the program order. Relaxed memory models can sup-port many optimizations. This dissertation explores a new relaxed memory model and proposes a new program logic for verifying concurrent algorithms in relaxed memory model.First, it presents OHMM, an operational variation of Happens-before Memory model(HMM). The model is specified by giving an operational semantics to a language running on an abstract machine designed to simulate HMM. Thanks to its generative nature, the model naturally prevents out-of-thin-air reads. On the other hand, it uses a novel replay mechanism to allow instructions to be executed multiple times, which can be used to model many useful speculations and optimization. The model is weaker than JMM for lockless programs, thus can accommodate more optimization, such as the re-ordering of independent memory accesses that is not valid in JMM. Program behaviors are more natural in this model than in JMM, and many of the anti-intuitive examples in JMM are no longer valid here. We hope OHMM can serve as the basis for new memory models for Java-like languages.Second, it proposes a new program logic for verifying concurrent algorithms in the TSO (Total Store Order) memory model, which has been used as the basis for x86and SPARC-TSO processor families, and in proposals for high-level programming lan-guages. The behaviors of programs running on TSO model are a subset of one on OHMMo Our logic extends LRG with explicit assertions for write buffers in TSO, which can specify locally buffered writes that are invisible to other threads yet. Like LRG, the logic supports both expressive rely/guarantee style reasoning for fine-grained concurrency and small-footprint local reasoning as in separation logic. The distinction of local memory from shared also gives us a more abstract and simplified view of TSO, in which local writes are done directly to memory and not buffered. We have applied the logic to verify several representative algorithms in TSO, including Peterson’s lock al-gorithm, Simpson’s four slot algorithm, a concurrent GCD algorithm and an optimized implementation of locks in TSO.