Mathematizing C++ Concurrency
ACM SIGPLAN Notices, 2011 · paper · Computer science
Establishes a mathematical semantics for C++ shared-memory concurrency, following the draft standard closely while proposing fixes to its problems. Proves a proposed x86 implementation correct against the x86-TSO model and describes the CPPMEM tool for exploring examples.
Checked: PDF from user.it.uu.se, fetched 4 Oct 2026. Page numbers are those of that PDF.
4 findings
Substance Worst-case count "with m reads and n writes ... there might be O(m^(n+1) · m! · (m + n)!) possible choices of an rf, modification-order and sc relation": the rf and mo factors appear to swap m and n.
- p. 11 §6 'Choosing instantiations of existential quantifiers'
O(m^(n+1) · m! · (m + n)!)
- p. 11 Choosing instantiations of existential quantifiers
O(m(n+1) · m! · (m + n)!)
Only the authors can say what is right here.
Judge's note: The crop shows m^(n+1) as a superscript, and m!. My own count: each of the m reads takes its value from one of the n writes or from none, giving (n+1)^m. Modification order is a total order over the n writes, giving n!. sc over all m+n actions gives (m+n)!. As printed, the expression is not an upper bound. With m=1 and n=3, my count is 4*6*24=576 but the printed expression gives 1*1*24=24. With m=10 and n=1, the rf factor alone is 2^10=1024 against the printed 10^2=100. The paper does not define the count any other way.
Second check: another model agreed
Report a problem with this finding
Reference or label 'having a read from a write (the read-modify-write (a)) that is sequenced-before-hidden by (c)'; in the figure (c) is the read c:R_SC x=1, and the hiding write is b:W_SC x=2.
- p. 8 §4 Coherence requirements, text below the two executions
modify-write (a)) that is sequenced-before-hidden by (c).
- p. 8 §4 Coherence requirements, text below the right-hand figure
modify-write (a)) that is sequenced-before-hidden by (c)
- p. 8 §4 'Coherence requirements', paragraph after the two execution diagrams
that is sequenced-before-hidden by (c)
- p. 8 Coherence requirements paragraph
sequenced-before-hidden by (c)
Judge's note: Page 8 right-hand figure: a:RMW_REL x=0/1 →(sb,mo) b:W_SC x=2 →(sb,vse) c:R_SC x=1, with a →rf c. CoWR (p.6) concerns a write that is hidden by a later write in modification order. Here that write is (b), since a mo→ b and b sb→ c. (c) is the read itself and cannot hide (a). The argument stands with (b) substituted, so the wrong letter is a pointer error. The 'sequenced-before-hidden' terminology (note 5) is consistent, because sb is a subset of hb.
Second check: another model agreed
Report a problem with this finding
Reference or label §2.10 cites 'inter-thread-happens-before (§2.8)' and 'consistent_inter_thread_happens_before ∧ (§2.8)', but both are defined in §2.9 'Happens-before'; the happens-before entry '(§2.1, §2.2, §2.3, §2.8)' likewise omits §2.9.
- p. 7 §2.10, list of derived relations
inter-thread-happens-before (§2.8)
- p. 7 Sec 2.10 consistent execution conjunction
consistent inter thread happens before ∧
- p. 7 consistent_execution table
consistent inter thread happens before ∧ (§2.8)
Judge's note: Page 7 image: §2.9 'Happens-before' defines inter-thread-happens-before, consistent_inter_thread_happens_before and the complete happens-before. §2.8 (p.6) defines only carries-a-dependency-to and dependency-ordered-before. The other pointers in the list (e.g. dob §2.8, sc_order §2.6) are correct, so these are wrong section pointers.
Second check: another model agreed
Report a problem with this finding
Wording §2.6: "the derived notion of a release sequence, of writes that follow (in some sense) a write-acquire" — the head of a release sequence is a write-release.
- p. 5 §2.6, left column, paragraph after first sw example
derived notion of a release sequence, of writes that follow (in some sense) a write-acquire.
- p. 5 §2.6, paragraph before the right-hand example
sense) a write-acquire.
- p. 5 Sec 2.6, before release-sequence definition
of writes that follow (in some sense) a write-acquire
- p. 5 Section 2.6
follow (in some sense) a write-acquire
Judge's note: Checked on the p5 image. The definition requires 'is_release a_rel', and the right column says 'The release sequence is headed by the release'. In §2.6 the acquire actions are reads and fences, so 'write-acquire' should read 'write-release'.
Second check: another model agreed
Report a problem with this finding
13 minor (typos and the like; most checked by the judge only)
Reference or label §2.8 diagrams label the accesses to the non-atomic 'int data' as 'a:WSC data=1' and 'd:RSC data=1', but the program declares 'int data;'.
- p. 6 §2.8, release/acquire and release/consume execution diagrams
a:WSC data=1
- p. 6 §2.8 program
int data; atomic_address p;
- p. 6
c:RACQ p=data d:RSC data=1 sw sb sb,dd a:WSC data=1 b:W
Only the authors can say what is right here.
Judge's note: Page 6 image: the program declares 'int data; atomic_address p;' and writes 'data=1', a non-atomic access. Both diagrams still show a:W_SC data=1 and d:R_SC data=1. Elsewhere the paper labels non-atomic accesses as Wna/Rna (§2.7 diagram; the MP example on p.7). For a different figure, §4 says the SC labels are 'shown as SC atomics for emphasis', but no such remark appears in §2.8. The labelling may be deliberate, so this is a query for the authors. The repeated 'sb' in reviewer note 3 comes from diagram edge labels in the text layer and is not a defect.
Second check: another model agreed, code check
Report a problem with this finding
Reference or label In the left candidate execution for y=(x==x), the constraint is "?v1 != ?v2", yet the diagram shows "e:Wna y=1", the same as the right candidate whose constraint is "true".
- p. 11 §6, left candidate execution for y=(x==x)
Constraint: ?v1 != ?v2 ... e:Wna y=1
- p. 11 §6, left candidate-execution diagram for the x==x program
e:Wna y=1
- p. 11
v1 e:Wna y=1 Constraint: true sb sb sb sb,dd sb,dd Late
Only the authors can say what is right here.
Judge's note: Page 11 crop: both candidates show e:Wna y=1. The program in §2.1 is y = (x==x). If the reads differ, the comparison yields 0, so the left candidate's write should be y=0 (or a symbolic value), not a concrete 1. The left execution is later ruled out, so this is only an inconsistency within the figure. The repeated 'sb' in reviewer note 3 is just diagram labels in the text layer.
Second check: another model agreed, code check
Report a problem with this finding
Wording Introduction: "We show that any x86-TSO execution of a translated C++ candidate execution gives behaviour that the C++ semantics would admit" does not mention the restrictions of Theorem 3 ("no undefined behaviour ... no SC fences, forks, joins, locks, or unlocks").
- p. 2 Introduction, Contributions
We show that any x86-TSO execution of a translated C++ candidate execution gives behaviour
- p. 10 Theorem 3
Suppose also that p contains no SC fences, forks, joins, locks, or unlocks.
Judge's note: Checked the crops of p2 and p10 and the §5 text. §5 says it proves "a version of the above prototype". It says locks, unlocks, forks and joins are left out "Following the prototype", and that SC fences are also left out. Since the prototype itself has no locks, forks or joins, the introduction's "the proposed prototype x86 implementation" mostly covers those. The SC-fence exclusion and the no-undefined-behaviour condition, though, appear only in §5. This is a minor scope abbreviation in the introduction. The restrictions are stated plainly in §5, so it is an observation, not an error.
Second check: another model agreed
Report a problem with this finding
Wording 'mo' is used for the memory-order parameter ("a memory order, mo", §2.4; "memory order parameter mo", §2.5) and also for the relation "modification order (mo)" (§2.5, figure edge labels).
- p. 4 §2.4
by a memory order, mo, that specifies how much synchronisa-
- p. 4 §2.5, Xwitness description
rf, sc, and modification order (mo)
Judge's note: Both definitions can be seen on the p4 image, and on p5 the figure edge label is 'sb,mo,rs'. Context (an action subscript versus a relation) usually tells them apart, so this is a minor notational ambiguity.
Second check: another model agreed
Report a problem with this finding
Wording The example is introduced as "With relaxed atomics there can be consistent executions in which it is impossible to disentangle the two into any sequence", but the program uses default (SC) x.store(1)/x.load(), and the diagram labels are b:WSC x=1, c:RSC x=0 and d:RSC x=1.
- p. 9 §4, thin-air discussion, top of left column
With relaxed atomics there can be consistent executions
- p. 9 §4 example program and diagram
b:WSC x=1
- p. 9
b:WSC x=1 d:RSC x=1 e:Wna y=0 rf rf,sc sc sb sb 5. Corr
Only the authors can say what is right here.
Judge's note: Page 9: the left-column sentence leads into an example whose code uses seq_cst defaults. Its diagram shows only SC atomic actions, and the same sentence refers to "the SC-write of x". The authors may mean that this happens even with SC atomics, but as written the sentence describes an SC example as a relaxed-atomics one. The repeated 'rf' in reviewer note 3 is just diagram labels in the text layer and is not a defect.
Second check: another model agreed, code check
Report a problem with this finding
Wording The proof outline says "if a and b are sequentially consistent atomics and a rf→ b, then a immediately precedes b in sc restricted to that address". This cannot hold when two SC reads read the same SC write.
- p. 10 §5, 'Sequentially consistent atomics', end of second paragraph
then a immediately precedes b in sc restricted to that address
Only the authors can say what is right here.
Judge's note: I checked this on the page-10 image. My own reworking: write a is W_SC x=1, and reads b and c are both R_SC x=1 with a rf→ b and a rf→ c. sc restricted to x is a total order on {a,b,c} with a before b and a before c. Only one of b and c can come immediately after a, so in every linearisation the stated property fails for one rf edge. The weaker property in §2.7 (a is the last sc-prior write to the address) does follow from the linearisation, so Theorem 3 stands; only this proof-outline step is misstated.
Second check: another model agreed
Report a problem with this finding
Typo §2.2: asw edges go "from sequenced-before-maximal actions of the parent thread ... to sequenced-before-minimal edges of the child"; the second 'edges' should be 'actions'.
- p. 3 §2.2, paragraph after thread-creation example
to sequenced-before-minimal edges of the child
- p. 3 §2.2, paragraph after thread example
before-minimal edges of the child
Judge's note: Checked on the p3 image. The example edge a -asw-> e joins two actions, and the same sentence's parallel phrase says 'sequenced-before-maximal actions'. This is a word slip.
Second check: none (judge only)
Report a problem with this finding
Typo §2.2: "We now integrate C++-0x threads into the model" uses 'C++-0x', whereas the paper elsewhere writes 'C++0x'.
- p. 3 §2.2, first sentence
We now integrate C++-0x threads into the model.
- p. 3 §2.2 first sentence
integrate C++-0x threads
Judge's note: The p3 image shows the hyphen. On p4 (§2.3, §2.4) and in the rest of the text the paper writes 'C++0x'.
Second check: none (judge only)
Report a problem with this finding
Typo §2.5 twice calls asw "additional-synchronized-with", whereas §2.2, §2.6 and the definitions call it "additional-synchronizes-with".
- p. 4 §2.5, description of Xopsem
additional-synchronized-with (asw)
- p. 3 §2.2
additional-synchronizes-with
Judge's note: The p4 image (§2.5) shows 'additional-synchronized-with (asw)' and 'additional-synchronized-with contains additional edges'. p3 (§2.2) and the formula labels on p4 and p5 show 'additional-synchronizes-with'. The same relation has two names.
Second check: none (judge only)
Report a problem with this finding
Typo Duplicated word: 'using sequentially consistent consistent atomics'.
- p. 7 §3 Store Buffering (SB)
using sequentially consistent consistent atomics
- p. 7 §3 Store Buffering paragraph
sequentially consistent consistent atomics
- p. 7
me program using sequentially consistent consistent atomics (with non-a
Judge's note: The page 7 image (Store Buffering paragraph) shows 'consistent consistent' on the same line.
Second check: code check
Report a problem with this finding
Typo Unbalanced parentheses in the thin-air example: 'r1 = x.load(mo_relaxed));' and 'r2 = y.load(mo_relaxed));'.
- p. 8 §4 'Overlapping executions and thin-air reads', program listing
r1 = x.load(mo_relaxed));
- p. 8 thin-air example code
r2 = y.load(mo_relaxed));
Judge's note: The page 8 image shows the doubled ')' on both load lines of the program listing.
Second check: none (judge only)
Report a problem with this finding
Typo §4 writes the committee as '(TC1/SC22/WG21)', while the paper's own reference [Bec10] gives 'ISO/IEC JTC1 SC22 WG21 N3092'.
- p. 8 §4, first paragraph
(TC1/SC22/WG21)
- p. 12 Reference [Bec10]
ISO/IEC JTC1 SC22 WG21 N3092
- p. 8 Section 4 first paragraph
TC1/SC22/WG21
Judge's note: The page 8 image shows 'TC1/SC22/WG21'. The page 12 reference [Bec10] reads 'ISO/IEC JTC1 SC22 WG21'. The two disagree internally, and the missing 'J' is evident.
Second check: none (judge only)
Report a problem with this finding
Typo "can be linked in with the rest of the CPPSEM tool": everywhere else the tool is named CPPMEM.
- p. 11 §6 'Checking code extracted from Isabelle'
can be linked in with the rest of the CPPSEM tool
- p. 11 §6 'Checking code extracted from Isabelle'
the rest of the CPPSEM tool
- p. 11 Checking code extracted from Isabelle
linked in with the rest of the CPPSEM tool
- p. 11 Checking code extracted from Isabelle
rest of the CPPSEM tool
Judge's note: The page-11 crop shows 'CPPSEM' in small caps. Searching the text finds CPPMEM at lines 24, 171, 180, 183 and 1612, and CPPSEM only here. No component called CPPSEM is introduced anywhere.
Second check: none (judge only)