Relaxed Memory Model Zoo

Memory model
← Back to the map

SC-Haskell SC-Hs

2017 · Vollmer, Scott, Musuvathi, Newton · language, formal

An SC-preserving model for Haskell that separates thread-local from shared mutable memory using Haskell's strong type system, so the type checker enforces the discipline needed to preserve SC. A modified GHC was measured on 1,279 benchmarks with only a 0.4% geometric-mean slowdown (just 12 benchmarks above 10%), helped by Haskell's purely functional style minimising shared mutable state. It admits exactly the SC behaviours.

Ordering relationships

Equivalent to
  • Sequential Consistency (SC) — SC-Haskell preserves sequential consistency using Haskell's type system to separate thread-local from shared mutable state; it admits exactly the SC outcomes, differing from SC only in mechanism and performance.

References

  • Michael Vollmer, Ryan G. Scott, Madanlal Musuvathi, Ryan R. Newton. SC-Haskell: Sequential Consistency in Languages That Minimize Mutable Shared Heap. PPoPP 2017, 2017. doi:10.1145/3018743.3018746
  • 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