Indeed, there exist schedules that let the synchronization points occur in the incorrect order. I added two assertions and a counter to the framework that make sure that the program is actually following the schedule. Note that these assertions are outside any kind of lock, of course:
...
printf("[%d] replayWait ends ------------------------\n", tid);
/*-------------------------------------------------------------
* Assert that the events are happening in the correct order */
atomic{
printf("@@@@@ Asserting actual [%d %d] == expected [%d %d] @@@@@\n",
code, tid, schedule[outScheduleIndex], schedule[outScheduleIndex+1]);
assert(code == schedule[outScheduleIndex]);
assert(tid == schedule[outScheduleIndex+1]);
outScheduleIndex = outScheduleIndex + 2;
}
Now I let SPIN simulate all possible interleavings while checking for violated assertions, and at least one violating schedule was found:
pan: assertion violated (tid==schedule[(outScheduleIndex+1)]) (at depth 76)
pan: wrote pan_in.trail
pan: reducing search depth to 75
pan: wrote pan_in.trail
pan: reducing search depth to 73
pan: wrote pan_in.trail
pan: reducing search depth to 71
pan: wrote pan_in.trail
pan: reducing search depth to 69
pan: wrote pan_in.trail
pan: reducing search depth to 69
pan: wrote pan_in.trail
pan: reducing search depth to 65
pan: wrote pan_in.trail
pan: reducing search depth to 61
pan: wrote pan_in.trail
pan: reducing search depth to 60
pan: wrote pan_in.trail
pan: reducing search depth to 59
pan: wrote pan_in.trail
pan: reducing search depth to 58
pan: wrote pan_in.trail
pan: reducing search depth to 56
pan: wrote pan_in.trail
pan: reducing search depth to 54
pan: wrote pan_in.trail
pan: reducing search depth to 53
pan: wrote pan_in.trail
pan: reducing search depth to 52
(Spin Version 4.2.3 -- 5 February 2005)
+ Partial Order Reduction
Full statespace search for:
never claim - (not selected)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 192 byte, depth reached 139, errors: 14
953 states, stored
615 states, matched
1568 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.194 equivalent memory usage for states (stored*(State-vector + overhead))
0.706 actual memory usage for states (unsuccessful compression: 363.30%)
State-vector as stored = 729 byte + 12 byte overhead
2.097 memory used for hash table (-w19)
0.002 memory used for DFS stack (-m52)
0.082 memory lost to fragmentation
2.724 total actual memory usage
Here’s a summary of the shortest trace that violates the assertions. It looks exactly as I suspected last night:
preparing trail, please wait...done
Starting :init: with pid 0
1: proc 0 (:init:) line 22 "pan_in" (state 1)
[schedule[0] = 1]
...
10: proc 1 (thread) line 12 "waitalgo.pml" (state 1)
[printf('[%d] replayWait(%d, %d)\\n',tid,code,tid)]
...
28: proc 1 (thread) line 95 "waitalgo.pml" (state 63)
[printf('[%d] sync point match at index = %d\\n',tid,replayIndex)]
...
[1] replayWait ends ------------------------
36: proc 1 (thread) line 236 "waitalgo.pml" (state 159)
[printf('[%d] replayWait ends ------------------------\\n',tid)]
37: proc 2 (thread) line 22 "waitalgo.pml" (state 2)
[((algo_lock==0))]
...
45: proc 2 (thread) line 95 "waitalgo.pml" (state 63)
[printf('[%d] sync point match at index = %d\\n',tid,replayIndex)]
...
[2] replayWait ends ------------------------
53: proc 2 (thread) line 236 "waitalgo.pml" (state 159)
[printf('[%d] replayWait ends ------------------------\\n',tid)]
...
54: proc 2 (thread) line 243 "waitalgo.pml" (state 161)
[assert((code==schedule[outScheduleIndex]))]
spin: line 244 "waitalgo.pml", Error: assertion violated
spin: text of failed assertion: assert((tid==schedule[(outScheduleIndex+1)]))
#processes: 4
54: proc 3 (thread) line 17 "waitalgo.pml" (state 156)
54: proc 2 (thread) line 244 "waitalgo.pml" (state 162)
54: proc 1 (thread) line 240 "waitalgo.pml" (state 164)
54: proc 0 (:init:) line 30 "pan_in" (state 12)
4 processes created
Assertions are a good thing, but it’s always sad when they are violated, along with your hopes.
