SC-Haskell SC-Hs
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.
Properties
Property vector survey-sourced — from Tables 1–2 of the Moiseenko et al. survey, except cells that cite a specific source.
- Compilation optimal mapping to
- no x86
- no POWER
- no Armv7
- no Armv8
- Reordering sound
- no Store→Load
- no Store→Store
- no Load→Load
- no Load→Store
- Elimination sound
- yes Store/Load
- yes Store/Store
- yes Load/Load
- yes Load/Store
- Other local transformations
- yes Irrelevant load elim.
- yes Speculative load intro.
- yes Roach motel
- yes Inverse roach motel Poetzl & Kroening 2015
- yes Strengthening
- yes Trace preserving
- no Common subexpr. elim.
- Global transformations
- yes Register promotion
- yes Thread inlining
- Reasoning guarantees
- yes External DRF
- yes Coherence
- yes No undefined behaviour
- yes In-order execution
- yes No out-of-thin-air
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
- Daniel Poetzl, Daniel Kroening. Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models. arXiv:1510.07171, 2015. arxiv.org/abs/1510.07171