edits
[model-checker-benchmarks.git] / ms-queue / note.txt
1 We ran testcase1 (two enqueuers and 1 dequeuer) and get result1.txt, then we ran
2 testcase2 (1 enqueuers and 2 dequeuers) based on result1.txt and got
3 result2.txt. We can't infer the wildcard(4) to be acquire because we can't reach
4 "that case"!!! 
5 See
6 http://stackoverflow.com/questions/3873689/lock-free-queue-algorithm-repeated-reads-for-consistency
7
8
9 result1.txt -> 0m14.826s
10 result2.txt -> 0m1.289s
11
12 total -> 0m 16.115