occam-π Implementations

Back to Santa

On this page you can find several implementations of the Santa Claus code in occam-π. In general each implementation consists of the actual code file, a file containing the protocol specification, and a file containing the display process, as well as two smaller files containing implementations of the partial barrier and the parts of the code that deals with random wait time.

Santa Claus Source for the TOPLAS paper
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


FDR CSP Files
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



To correctly compile the provided occam files, the latest version of the occam-π is required (If you have an older version, the one-line claim will produce an error. Please visit the following three pages for more information about downloading and installing occam-π
The table below shows the results (time it took and the number of FDR ticks/states) of verifying the different CSP scripts in FDR on a 2.2 GHz. Mac Pro with 2 GB of RAM. If you wish to reproduce the results we strongly reccomend that you set the envrionment variable FDRPAGEDIR to a colon (:) separated list of directories with enough space free. FDR does its own page swapping, and thus can use a lot more memory than physically/virtually available.
FDR Results for Full Models (10 Elves and 9 Reindeer)
paper-5-4.csp
 SYSTEM deadlock free [F]36 sec2,101,288 ticks
 SYSTEM deadlock free [FD]124 sec2,101,288 ticks
 SYSTEM livelock free126 sec2,101,288 ticks
paper-5-5.csp
 SYSTEM deadlock free [F]3,579 sec156,210,432 ticks
 SYSTEM deadlock free [FD]18,396 sec156,210,432 ticks
 SYSTEM livelock free21,063 sec156,210,432 ticks
 CHECK_A_SYSTEM deadlock free [F]3,571 sec156,210,432 ticks
 CHECK_A_SYSTEM deadlock free [FD]35,578 sec156,210,432 ticks
 CHECK_A_SYSTEM livelock free17,819 sec156,210,432 ticks
paper-6-1.csp
 SYSTEM deadlock free [F]220 sec12,829,998 ticks
 SYSTEM deadlock free [FD]438 sec12,829,998 ticks
 SYSTEM livelock free466 sec12,829,998 ticks
 not CHECK_B_SYSTEM deadlock free [F]53 sec6,227 ticks
 not CHECK_B_SYSTEM deadlock free [FD]53 sec6,227 ticks
 CHECK_B_SYSTEM livelock free499 sec12,829,998 ticks
paper-6-2.csp
SYSTEM deadlock free [F]171 sec9,622,242 ticks
SYSTEM deadlock free [FD]381 sec9,622,242 ticks
SYSTEM livelock free383 sec9,622,242 ticks
CHECK_B_SYSTEM_WR deadlock free [F]166 sec9,622,242 ticks
CHECK_B_SYSTEM_WR deadlock free [FD]392 sec9,622,242 ticks
CHECK_B_SYSTEM_WR livelock free388 sec9,622,242 ticks
paper-6-3a.csp
SYSTEM deadlock free [F]186 sec12,420,848 ticks
SYSTEM deadlock free [FD]382 sec12,420,848 ticks
SYSTEM livelock free387 sec12,420,848 ticks
not CHECK_C_SYSTEM_WR deadlock free [F]10 sec606,103 ticks
not CHECK_C_SYSTEM_WR deadlock free [FD]83 sec606,103 ticks
CHECK_C_SYSTEM_WR livelock free396 sec12,346,928 ticks
paper-6-3b.csp
SYSTEM_WR deadlock free [F]180 sec10,641,968 ticks
SYSTEM_WR deadlock free [FD]427 sec10,641,968 ticks
SYSTEM_WR livelock free424 sec10,641,968 ticks
CHECK_C_SYSTEM_WR deadlock free [F]195 sec10,641,968 ticks
CHECK_C_SYSTEM_WR deadlock free [FD]446 sec10,641,968 ticks
CHECK_C_SYSTEM_WR livelock free428 sec10,641,968 ticks
paper-6-4a.csp
SYSTEM_WR deadlock free [F]166 sec10,663,088 ticks
SYSTEM_WR deadlock free [FD]330 sec10,663,088 ticks
SYSTEM_WR livelock free329 sec10,663,088 ticks
paper-6-4b.csp
WG3 [T= SYSTEM_WR138 sec10,653,224 ticks
SYSTEM_WR [T= WG3none reported10,653,224 ticks
33,461 states
WG3 [F= SYSTEM_WR218 sec10,653,224 ticks