Relaxed Memory Model Zoo

Memory model
← Back to the map

End-to-End Sequential Consistency EtE-SC

2012 · Singh, Narayanasamy, Marino, Millstein, Musuvathi · language, formal

An approach to providing end-to-end sequential consistency for a language, enforced jointly by an SC-preserving variant of the LLVM compiler and modified x86 hardware. To curb the overhead it enforces SC only for accesses to shared mutable variables, classifying memory regions as thread-local, shared-immutable, or shared-mutable via a combination of static compiler analysis and hardware-assisted dynamic analysis. Reported overhead is 6.2% on average (17% maximum) versus stock LLVM and x86. Like the other SC-preserving designs it admits exactly the SC behaviours.

Ordering relationships

Equivalent to
  • Sequential Consistency (SC) — EtE-SC restores end-to-end sequential consistency via an SC-preserving LLVM compiler and modified x86 hardware; it admits exactly the SC outcomes, differing from SC only in enforcement mechanism and performance, not in allowed behaviours.

References

  • Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy. A Case for an SC-Preserving Compiler. PLDI 2011, 2011. doi:10.1145/1993316.1993522
  • Abhayendra Singh, Satish Narayanasamy, Daniel Marino, Todd Millstein, Madanlal Musuvathi. End-to-End Sequential Consistency. ISCA 2012, 2012. doi:10.1109/ISCA.2012.6237045
  • Evgenii Moiseenko, Anton Podkopaev, Dmitrii Koznov. A Survey of Programming Language Memory Models. Programming and Computer Software 47(6), pp. 439–456, 2021. doi:10.1134/S0361768821060050