Relaxed Memory Model Zoo

Memory model
← Back to the map

Theory of Speculative Computation TSC

2010 · Boudol, Petri · language, formal, theoretical

A general framework for studying the effects of speculative computation in a shared-memory setting. The authors observe that under unrestricted speculation the external DRF theorem fails, while the internal DRF theorem can still be proved; the framework analyses speculation abstractly rather than proposing a concrete language model.

Ordering relationships

Incomparable with
  • C11/C++11 Memory Model — TSC is a general framework for the effects of speculative execution. Under unrestricted speculation the external DRF theorem fails (only internal DRF holds) and thin-air values appear; it studies speculation abstractly rather than refining C11, so the two are incomparable.

References

  • Gérard Boudol, Gustavo Petri. A Theory of Speculative Computation. ESOP 2010, 2010. doi:10.1007/978-3-642-11957-6_10
  • 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