Partition consistency: A case study in modeling systems with weak memory consistency and proving correctness of their implementations

摘要

This paper provides a case study of specifying an memory consistency model, providing possible implementations for the model, and proving the correctness of implementations. Specifically, we introduce a class of memory consistency models called partition consistency. Existing consistency models such as sequential consistency, piplined-RAM, Goodman's processor consistency, and coherence are all members of the partition consistency class. A concrete message-passing network model is also specified. Implementations of partition consistency on this network model are then presented and proved correct. A middle level of abstraction is utilized to facilitate the proofs. All three levels of abstraction are specified using the same framework. The paper aims to illustrate a general methodology and techniques for specifying memory consistency models and proving the correctness of their implementations.