t0 t1 t2 acq m wr x 1 rel m wr x 2 acq m rd x 2 rel m
t0 t1 t2 acq m wr x 1 rel m wr x 2 acq m rd x 1 rel m
x, because swapping the sync blocks would violate happens-before consistency in JMM: t0's read of
yobserves t1's write of
y; swapping the sync blocks would make t0's read of
yhappen-before t1's write of
yby the RA edge. From Oct 28, 2009.
t0 t1 rd y 5 rd x acq m rel m acq m rel m wr x wr y 5
t0 t1 wr x acq m rel m wr y 5 rd y 5 acq m rel m rd x
x) according to HBCO, and two races according to HB.
t0 t1 wr y wr x rd x rd y
t0 t1 wr y wr x acq m rel m acq m rel m rd x rd y
z, yet we'd like to find that race by swapping the sync blocks. When we do, operations that happen-after t1's read of
yare unknown, but we make the assumption that t1's release operation will (eventually) occur. From Sept 9, 2009.
t0 t1 rd z acq m wr y rel m acq m wr z rd y rel m
z, since t2's access to
zhappens-after the read of
y, and changing that read's value may cause the
zaccess to not occur. From Sept 9, 2009.
t0 t1 t2 rd z acq m wr x rel m acq m wr y rd x rel m acq m rd y wr z rel m
x. However, it is feasible to commute the two sync blocks, and then the HB race manifests. We don't know about the operations that happen-after t0's read inside the sync block, since the read will observe t1's write, but in some sense we don't care. This type of example motivated our brief inquiry into “prefix-equivalent” traces, where two traces are equivalent if the same read operation observes the same write across different traces, but if a read must observe a different write (after some commute), then operations that happen-after are removed from consideration, and the resulting truncated trace is “prefix-equivalent” to the original trace. From May 7, 2009.
t0 t1 rd x acq m rd x rel m acq m wr x rel m
t0 t1 wr x acq m rel m acq m rel m wr x
xto be racy in
t2, while an additional observation of
t1negates this prediction. When the trace is closed, no future operation can force addition of release-acquire edges to already-seen sync blocks.
t0 t1 t2 wr x acq m wr y rel m acq m fork t2 wr x --- at this point, x is apparently predictably racy wr y --- at this point, y introduces release-acquire edge, and x no longer predictably racy rel m
t0 t1 t2 t3 wr x wr v acq m0 sync m rd w rd v sync n rel m0 acq m3 sync n rd w rd v sync m rel m3 wr w rd x
Here is a witness.
t0 t1 t2 t3 wr x acq m0 sync m rd w acq m3 sync n rd w wr w rd x wr v rd v sync n rel m0 rd v sync m rel m3
xare related by HB and BB but not MB; hence the MB race on
x. Indeed, this race on
xis predictable, as shown by our witness trace (below).
t0 t1 acq m acq p wr pp rel p wr x acq o rel o rel m acq o acq m rel m wr x acq p wr pp rel p rel o
However, no swap of adjacent sequences gives us the witness trace to an HB race between these two writes to
x. Observe that PO and CO are preserved, and the trace is well-formed; it is obvious that the program can generate this “equivalent” trace. Unfortunately, our notion of equivalence does not provide a method of inductively identifying what operation or sync block to first commute out from between the two writes to
x to obtain this witness trace. This gap in equivalence prevents us from arguing that we can always obtain an equivalent trace containing an HB race. Strengthening MB in some way might allow us to retain the definition of ≈; alternatively, we could try redefining a more general ≈.
t0 t1 acq o acq m rel m acq m acq p wr pp rel p wr x wr x acq p wr pp rel p rel o acq o rel o rel m