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".