|
Program | time (s) | size | success | comments | options |
|
Peterson mutual exclusion algorithm |
|
peterson2 |
3.7 | (267,490) | yes | | |
|
peterson2inline |
0.2 | (35,58) | yes | | |
|
peterson2rec |
8.3 | (435,1128) | yes | unbounded recursion | |
|
Kessel mutual exclusion algorithm |
|
kessel2 |
5.8 | (302,558) | yes | | |
|
kessel2inline |
0.5 | (63,110) | yes | single-procedure version | |
|
kessel2rec |
12.5 | (478,1230) | yes | unbounded recursion | |
|
Synchronisation barrier algorithm with counter (and loops with numerical variables) |
|
global2 |
8.5 | (186,400) | yes | version with global loop counters | -widening false 2 1 2 -guided true |
|
global2a |
14.6 | (199,452) | no | version with additional call outside the loop | -widening false 2 1 2 -guided true |
|
|
15.5 | (199,452) | yes | Success by combining forward and backward analysis | -widening false 2 1 2 -guided true -analysis fb |
|
global2inline |
2.4 | (117,230) | yes | singe-procedure version | -widening false 2 1 2 -guided true |
|
global2ainline |
2.9 | (171,357) | yes | single-procedure version | -widening false 2 1 2 -guided true |
|
local2 |
7.1 | (186,404) | no | version with local loop counters. Does not work either by combining forward and backward analysis | -widening false 2 1 2 -guided true |
|
local2inline |
2.1 | (117,234) | yes | single-procedure version | -widening false 2 1 2 -guided true |
|
local2ainline |
2.3 | (171,357) | yes | single-procedure version | -widening false 2 1 2 -guided true |
|
Example of POPL04 paper of Quadee, Rajamani & Rehof |
|
peterson |
22.0 | (743,1778) | yes | using Peterson mutual exclusion algorithm |
|
|
