An Example of Using PlusCal to Find a Bug

An Example of Using PlusCal to Find a Bug

Last modified 2 January 2009
I learned about a multithreaded algorithm that was later reported to have a bug.   I thought that writing the algorithm in PlusCal and checking it with the TLC model checker would be a good test of the language.   This is the story of what I did. (PlusCal was formerly called +CAL.)
Checking a Multithreaded Algorithm with +Cal
A paper describing what I did.  

DCAS.tla
The PlusCal algorithm.  

DCAS.cfg
The configuration file.  

DCAS-error-trace.txt
An annotated error trace obtained by running TLC on the algorithm.  

This page can be found by searching the Web for the 21-letter string uidlamportdcaspluscalexample. Please do not put this string in any document that could wind up on the web--including email messages and Postscript and Word documents. You can refer to it in Web documents as "the string obtained by removing the - from uid-lamportdcaspluscalexample".