Partition Consistency: A Case Study in Modeling Systems with Weak Memory Consistency and Proving Correctness of their Implementations

TL;DR

This paper introduces partition consistency, a generalized memory model for multiprocess systems, and demonstrates a methodology for specifying and proving the correctness of its implementations across different abstraction levels.

Contribution

It presents a new, generalized memory consistency model and a formal methodology for specifying and verifying the correctness of its implementations.

Findings

Partition consistency generalizes existing models.

Correctness proofs for implementations on message-passing networks.

A unified framework for specifying and verifying memory models.

Abstract

Multiprocess systems, including grid systems, multiprocessors and multicore computers, incorporate a variety of specialized hardware and software mechanisms, which speed computation, but result in complex memory behavior. As a consequence, the possible outcomes of a concurrent program can be unexpected. A memory consistency model is a description of the behaviour of such a system. Abstract memory consistency models aim to capture the concrete implementations and architectures. Therefore, formal specification of the implementation or architecture is necessary, and proofs of correspondence between the abstract and the concrete models are required. This paper provides a case study of this process. We specify a new model, partition consistency, that generalizes many existing consistency models. 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.