projects:trickytraces

- t2's rd observes t0's wr, so t1's sync block can commute with t2's sync block, even though the two sync blocks have conflicting accesses on
`x`

.t0 t1 t2 acq m wr x 1 rel m wr x 2 acq m rd x 2 rel m

- However, if t2's rd observes t1's wr, then the two sync blocks cannot commute: happens-before consistency would be violated.
t0 t1 t2 acq m wr x 1 rel m wr x 2 acq m rd x 1 rel m

- This trace has no predictable HB race on
`x`

, because swapping the sync blocks would violate happens-before consistency in JMM: t0's read of`y`

observes t1's write of`y`

; swapping the sync blocks would make t0's read of`y`

happen-before t1's write of`y`

by 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

- A variation with no predictable HB (or HBrel) race on
`x`

.t0 t1 wr x acq m rel m wr y 5 rd y 5 acq m rel m rd x

- This trace has one race (on
`x`

) according to HBCO, and two races according to HB.t0 t1 wr y wr x rd x rd y

- This trace has 0 HB races, 0 HBCO races, 1 MBCO race, and 2 MB races, where MB = (PO + (SO \intersect MBCO)*)*.
t0 t1 wr y wr x acq m rel m acq m rel m rd x rd y

- An example from IFL: there is no HB race on
`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`y`

are 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

- Another example from IFL: there is no predictable HB race on
`z`

, since t2's access to`z`

happens-after the read of`y`

, and changing that read's value may cause the`z`

access 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

- Another early IFL example. This trace has no HB race on
`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

- This is the canonical example that race prediction should always be able to catch.
t0 t1 wr x acq m rel m acq m rel m wr x

- This example shows why we act on
*closed*traces: there might be more operations, as yet unseen, that may introduce extra dependencies. Here, one might predict`x`

to be racy in`t2`

, while an additional observation of`y`

in`t1`

negates 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

- This example shows that the witness trace may be non-serial, as either interleaving of the two sync blocks givs a HB edge on the accessex to x (for main-cf.tex proof based on BB and MB). sync m = acq m; rel m. v and w are volatiles
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

- This example demonstrates our notion of equivalence ≈ may not be general enough: the two writes to
`x`

are related by HB and BB but not MB; hence the MB race on`x`

. Indeed, this race on`x`

is 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

projects/trickytraces.txt · Last modified: 2010/05/02 18:23 by jaeheon