|
Program | time (s) | size | success | comments | options |
|
Peterson mutual exclusion algorithm |
|
peterson2 |
1.3 | (141,227) | yes | | |
|
peterson2inline |
0.1 | (24,38) | yes | | |
|
peterson2rec |
3.4 | (217,486) | yes | unbounded recursion | |
|
Kessel mutual exclusion algorithm |
|
kessel2 |
2.0 | (168,273) | yes | | |
|
kessel2inline |
0.2 | (48,82) | yes | single-procedure version | |
|
kessel2rec |
4.0 | (248,552) | yes | unbounded recursion | |
|
Synchronisation barrier algorithm with counter (and loops with numerical variables) |
|
global2 |
3.2 | (110,156) | yes | version with global loop counters | -widening false 1 1 2 -guided true |
|
global2a |
3.8 | (116,171) | no | version with additional call outside the loop | -widening false 1 1 2 -guided true |
|
|
4.1 | (116,171) | yes | Success by combining forward and backward analysis | -widening false 1 1 2 -guided true -analysis fb |
|
|
4.5 | (116,171) | yes | Additional descending step | -widening false 1 1 3 -guided true |
|
global2inline |
1.4 | (60,95) | no | singe-procedure version | -widening false 1 1 2 -guided true |
|
| 1.5 | (60,95) | yes | singe-procedure version | -widening false 1 1 4 -guided true |
|
global2ainline |
2.0 | (88,147) | yes | single-procedure version | -widening false 1 1 5 -guided true |
|
local2 |
2.6 | (110,156) | no | version with local loop counters. Does not work either by combining forward and backward analysis | -widening false 1 1 5 -guided true |
|
local2inline |
1.6 | (60,95) | yes | single-procedure version | -widening false 1 1 4 -guided true |
|
local2ainline |
1.8 | (88,147) | yes | single-procedure version | -widening false 1 1 5 -guided true |
|
Example of POPL04 paper of Quadee, Rajamani & Rehof |
|
peterson |
7.0 | (438,735) | yes | using Peterson mutual exclusion algorithm |
|
|
