User Tools

Site Tools


projects:trickytraces

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
projects:trickytraces [2010/05/02 18:09]
jaeheon
projects:trickytraces [2010/05/02 18:23] (current)
jaeheon
Line 177: Line 177:
                rel p                rel p
              rel o              rel o
-</​code>​ 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 ≈. <​code>​+</​code>​ 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 ​≈. <​code>​
 t0           ​t1 ​       ​ t0           ​t1 ​       ​
              acq o              acq o
projects/trickytraces.txt · Last modified: 2010/05/02 18:23 by jaeheon