This project is read-only.

Bug in DPOR implementation


I believe there is a bug in the dynamic partial-order reduction (DPOR) implementation that can lead to backtracking points being missed.

In FindConflict, say the op is a write and there are several prior read accesses from different threads. The most recent read gets passed to HandleConflict but this method may return where it says:

// No backtracking points necessary if something subsequent to bstep already has
// happens before with next prior to executing lookahead

At this point, I think one of the earlier reads could still trigger a backtracking point, but these will not be considered.

T1: read(x)
T2:              read(x), create(T3)
T3:                                              start(T3), write(x)
Assume the write(x) is being checked by FindConflict. T2's read(x) will be passed to HandleConflict but the method will return because the read happens-before T3. T1's read(x) should then be considered, but (I think) it is not.