+++
title = "CompCertTSO"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a10c"]
forwardlinks = []
zettelid = "3a10d"
+++
CompCertTSO \[1\] builds a notion of finite memory model to support the
TSO shared memory model.
\[1\]
J. Ševčı́k, V. Vafeiadis, F. Zappa
Nardelli, S. Jagannathan, and P. Sewell, “CompCertTSO: A verified
compiler for relaxed-memory concurrency,” *J. ACM*, vol. 60, no. 3, Jun.
2013, doi: [10.1145/2487241.2487248].
[10.1145/2487241.2487248]: https://doi.org/10.1145/2487241.2487248