summaryrefslogtreecommitdiffstats
path: root/content/zettel/3a10d.md
blob: ec94b488ec79d37861e6d96e836073472bf9b3c2 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
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