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

DOI10.1007/S00446-013-0205-0MaRDI QIDQ2256965zbMATH OpenOpenAlexFDO

Authors Steven Cheng, Lisa Higham, Jalal Kawash

Publication date 23 February 2015

Published in Distributed Computing (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1306.0077

zbMATH Keywords

correctness of distributed implementationsdistributed-shared memorypartial-order broadcastprocessor consistencysequential consistencyweak memory consistency models

Mathematics Subject Classification ID

Distributed systems (68M14)

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.

Recommendations

• scientific article; zbMATH DE number 1979557
• scientific article; zbMATH DE number 1903349
• The complexity of weak consistency
• Programmer-centric memory consistency modelling
• A formal hierarchy of weak memory models

Cites work

• A semantics for concurrent separation logic
• A unified theory of shared memory consistency
• Capturing Register and Control Dependence in Memory Consistency Models with Applications to the Itanium Architecture
• Formalising Java’s Data Race Free Guarantee
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 1301859 (Why is no real title available?)
• scientific article; zbMATH DE number 1330044 (Why is no real title available?)
• scientific article; zbMATH DE number 1179121 (Why is no real title available?)
• Implementing sequentially consistent programs on processor consistent platforms
• Mathematizing C++ concurrency
• On interprocess communication. I: Basic formalism
• Reactive Systems
• The equational theory of pomsets
• The Java memory model
• Time, clocks, and the ordering of events in a distributed system

Cited in

(2)

• scientific article; zbMATH DE number 1859710 (Why is no real title available?)
• Y-invalidate: A new protocol for implementing weak consistency in DSM systems

Describes a project that uses

Uses Software

• Checkfence

This page was built for publication: Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2256965)