When verifying a concurrent program, it is usual to assume sequentially consistent memory. However, most modern multiprocessors buffer their stores, providing native sequential consistency only at a substantial performance penalty. To regain sequential consistency, a programmer has to follow an appropriate programming discipline. However, existing na\"ive disciplines, such as protecting all shared accesses with locks to avoid data races, or flushing store buffers according to a protocol that allows arbitrary data races, 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). Instead of using concurrency primitives, such as locks, it is based on maintaining ownership information in ghost state, allowing the discipline to be expressed as a state invariant and verified through conventional program reasoning. We prove in Isabelle/HOL 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.

Online Copy

Updated version available as PDF-File (coming soon)

BibTeX Entry

@InProceedings{Cohen:ITP2010-, author = "Ernie Cohen and Bert Schirmer", title = "From Total Store Order to Sequential Consistency: {A} Practical Reduction Theorem", editor = "Matt Kaufmann and Lawrence Paulson and Michael Norrish", booktitle = "Interactive Theorem Proving (ITP 2010)", address = "Edinburgh, UK", year = "2010", publisher = "Springer", series = "Lecture Notes in Computer Science", note = "To appear.", }