diff options
Diffstat (limited to 'content/zettel/3a10d.md')
| -rw-r--r-- | content/zettel/3a10d.md | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/content/zettel/3a10d.md b/content/zettel/3a10d.md new file mode 100644 index 0000000..ec94b48 --- /dev/null +++ b/content/zettel/3a10d.md @@ -0,0 +1,28 @@ ++++ +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. + +<div id="refs" class="references csl-bib-body" markdown="1"> + +<div id="ref-sevcik13_compc" class="csl-entry" markdown="1"> + +<span class="csl-left-margin">\[1\] +</span><span class="csl-right-inline">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].</span> + +</div> + +</div> + + [10.1145/2487241.2487248]: https://doi.org/10.1145/2487241.2487248 |