Description | File |
Code matching Section 4 of the paper | santa-paper-4.occ |
Code matching Section 6 of the paper | santa-paper-6.occ |
Code matching Appendix F of the paper | santa-paper-f.occ |
Include file with protocol code. Matches code in Appendix B plus elves-in-waiting-room message needed by santa-paper-6.occ. |
protocol.occ |
Include file with implementation of a partial barrier. Matches code in section 4.2 and Appendix C. |
partial-barriers.occ |
Include file with code for random waits. | random-stuff.occ |
Include file code needed for displaying messages. | display.occ |
tar file with the above 7 files. | toplas-santa-occ.tar | Generic version with mobile processes. Not shown in the TOPLAS paper. | santa6.tar |
Description | CSP file | FDR CSP Script for section 5.4 | paper-5-4.csp | FDR CSP Script for section 5.5 | paper-5-5.csp | FDR CSP Script for section 6.1 | paper-6-1.csp | FDR CSP Script for section 6.2 | paper-6-2.csp | FDR CSP Script for section 6.3 (a) | paper-6-3a.csp | FDR CSP Script for section 6.3 (b) | paper-6-3b.csp | FDR CSP Script for section 6.4 (a) | paper-6-4a.csp | FDR CSP Script for section 6.4 (b) | paper-6-4b.csp |
paper-5-4.csp | ||
SYSTEM deadlock free [F] | 36 sec | 2,101,288 ticks |
SYSTEM deadlock free [FD] | 124 sec | 2,101,288 ticks |
SYSTEM livelock free | 126 sec | 2,101,288 ticks |
paper-5-5.csp | ||
SYSTEM deadlock free [F] | 3,579 sec | 156,210,432 ticks |
SYSTEM deadlock free [FD] | 18,396 sec | 156,210,432 ticks |
SYSTEM livelock free | 21,063 sec | 156,210,432 ticks |
CHECK_A_SYSTEM deadlock free [F] | 3,571 sec | 156,210,432 ticks |
CHECK_A_SYSTEM deadlock free [FD] | 35,578 sec | 156,210,432 ticks |
CHECK_A_SYSTEM livelock free | 17,819 sec | 156,210,432 ticks |
paper-6-1.csp | ||
SYSTEM deadlock free [F] | 220 sec | 12,829,998 ticks |
SYSTEM deadlock free [FD] | 438 sec | 12,829,998 ticks |
SYSTEM livelock free | 466 sec | 12,829,998 ticks |
not CHECK_B_SYSTEM deadlock free [F] | 53 sec | 6,227 ticks |
not CHECK_B_SYSTEM deadlock free [FD] | 53 sec | 6,227 ticks |
CHECK_B_SYSTEM livelock free | 499 sec | 12,829,998 ticks |
paper-6-2.csp | ||
SYSTEM deadlock free [F] | 171 sec | 9,622,242 ticks |
SYSTEM deadlock free [FD] | 381 sec | 9,622,242 ticks |
SYSTEM livelock free | 383 sec | 9,622,242 ticks |
CHECK_B_SYSTEM_WR deadlock free [F] | 166 sec | 9,622,242 ticks |
CHECK_B_SYSTEM_WR deadlock free [FD] | 392 sec | 9,622,242 ticks |
CHECK_B_SYSTEM_WR livelock free | 388 sec | 9,622,242 ticks |
paper-6-3a.csp | ||
SYSTEM deadlock free [F] | 186 sec | 12,420,848 ticks |
SYSTEM deadlock free [FD] | 382 sec | 12,420,848 ticks |
SYSTEM livelock free | 387 sec | 12,420,848 ticks |
not CHECK_C_SYSTEM_WR deadlock free [F] | 10 sec | 606,103 ticks |
not CHECK_C_SYSTEM_WR deadlock free [FD] | 83 sec | 606,103 ticks |
CHECK_C_SYSTEM_WR livelock free | 396 sec | 12,346,928 ticks |
paper-6-3b.csp | ||
SYSTEM_WR deadlock free [F] | 180 sec | 10,641,968 ticks |
SYSTEM_WR deadlock free [FD] | 427 sec | 10,641,968 ticks |
SYSTEM_WR livelock free | 424 sec | 10,641,968 ticks |
CHECK_C_SYSTEM_WR deadlock free [F] | 195 sec | 10,641,968 ticks |
CHECK_C_SYSTEM_WR deadlock free [FD] | 446 sec | 10,641,968 ticks |
CHECK_C_SYSTEM_WR livelock free | 428 sec | 10,641,968 ticks |
paper-6-4a.csp | ||
SYSTEM_WR deadlock free [F] | 166 sec | 10,663,088 ticks |
SYSTEM_WR deadlock free [FD] | 330 sec | 10,663,088 ticks |
SYSTEM_WR livelock free | 329 sec | 10,663,088 ticks |
paper-6-4b.csp | ||
WG3 [T= SYSTEM_WR | 138 sec | 10,653,224 ticks |
SYSTEM_WR [T= WG3 | none reported | 10,653,224 ticks |
33,461 states | ||
WG3 [F= SYSTEM_WR | 218 sec | 10,653,224 ticks |