### Abstract

When verifying a concurrent program, it is usual to assume that memory is sequentially consistent. However, most modern multiprocessors depend on store buffering for efficiency, and provide native sequential consistency only at a substantial performance penalty. To regain sequential consistency, a programmer has to follow an appropriate programming discipline. However, naïve disciplines, such as protecting all shared accesses with locks, are not flexible enough for building high-performance multiprocessor software. We present a new discipline for concurrent programming under TSO (total store order, with store buffer forwarding). It does not depend on concurrency primitives, such as locks. Instead, threads use ghost operations to acquire and release ownership of memory addresses. A thread can write to an address only if no other thread owns it, and can read from an address only if it owns it or it is shared and the thread has flushed its store buffer since it last wrote to an address it did not own. This discipline covers both coarse-grained concurrency (where data is protected by locks) as well as fine-grained concurrency (where atomic operations race to memory). We formalize this discipline in Isabelle/HOL, and prove that if every execution of a program in a system without store buffers follows the discipline, then every execution of the program with store buffers is sequentially consistent. Thus, we can show sequential consistency under TSO by ordinary assertional reasoning about the program, without having to consider store buffers at all.

### License

BSD License

### Topics

- Computer science/Concurrency

### Session Store_Buffer_Reduction

- ReduceStoreBuffer
- ReduceStoreBufferSimulation
- PIMP
- SyntaxTweaks
- Abbrevs
- Variants
- Text
- Preliminaries

## Cite

×

Store_Buffer_Reduction-AFP

    @article{Store_Buffer_Reduction-AFP,
      author  = {Ernie Cohen and Norbert Schirmer},
      title   = {A Reduction Theorem for Store Buffers},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Store_Buffer_Reduction.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Jan 11, 2019 : Isabelle2018