Checking a Multithreaded Algorithm with +CAL
International Symposium on Distributed Computing (DISC) |
On a Wednesday afternoon in March of this year, my colleague Yuan Yu told me that Detlefs et al.  had described a multithreaded algorithm to implement a shared two-sided queue using a double-compare-and-swap (DCAS) operation, and that Doherty et al.  later reported a bug in it. I decided to rewrite the algorithm in +cal  and check it with the TLC model checker, largely as a test of the +cal language. After working on it that afternoon, part of Sunday, and a couple of hours on Monday, I found the bug. This is the story of what I did. A +cal speciﬁcation of the algorithm and an error trace that it produced are available on the Web . I hope my experience will inspire computer scientists to model check their own algorithms before publishing them. +cal is an algorithm language, not a programming language. It is expressive enough to provide a practical alternative to informal pseudo-code for writing high-level descriptions of algorithms. It cannot be compiled into eﬃcient executable code, but an algorithm written in +cal can be translated into a TLA+speciﬁcation that can be model checked or reasoned about with any desired degree of formality. Space does not permit me to describe the language and its enormous expressive power here. The two-sided queue algorithm is a low-level one, so its +cal version looks much like its description in an ordinary programming language. The features of +cal relevant to this example are explained here. A detailed description of the language along with the translator and model-checker software are on the Web.
Yuan Yu told me about a multithreaded algorithm that was later reported to have a bug. I thought that writing the algorithm in PlusCal (formerly called +CAL)  and checking it with the TLC model checker  would be a good test of the PlusCal language. This is the story of what I did. The PlusCal specification of the algorithm and the error trace it found are available here.