Chalice is an experimental language that explores specification and verification of concurrency in programs. The language supports dynamic object creation, dynamic thread creation (fork and join), mutual-exclusion and readers-writers locks, monitor invariants, thread pre- and postconditions. The language allows fine-grained locking via specifications that track fractional permissions for memory locations. The research project also includes an automatic static program verifier for Chalice.
Because of its permissions model, Chalice has also been used as a test bed for stepwise refinement. Using refinement, one can write an abstract program (call it pseudo-code) and then provide a more concrete implementation for that pseudo-code. The pseudo-code and its refinements all become part of the program text, and the Chalice verifier checks the correctness of the refinement steps. An episode of Verification Corner shows how this is done.
Chalice is available for download as open source from the Boogie open-source repository. There is also a nightly build that contains the binaries, available from "planned" releases on the Download tab.
If you want to program in Chalice or learn how its specifications are used (or, for that matter, to learn the basics of what makes a concurrent program correct), the Chalice tutorial is for you:
K. Rustan M. Leino, Peter Müller, and Jan Smans. Verification of Concurrent Programs with Chalice. In Foundations of Security Analysis and Design V: FOSAD 2007/2008/2009 Tutorial Lectures, volume 5705 of LNCS, pages 195-222. Springer, 2009. [PDF]
It may also helpful to see animations of permissions transfers in Chalice: [slides]
The following paper explains the model behind specifications in Chalice:
K. Rustan M. Leino and Peter Müller. A basis for verifying multi-threaded programs. In ESOP 2009, volume 5502 of LNCS, pages 378-393. Springer 2009. [PDF]
However, since that paper, the meaning of the rd access predicate and the ease with which fractional permissions can be specified have been improved. Read all about it in:
Chalice also supports copy-free, multiple-writer multiple-reader, infinite-slack channels:
K. Rustan M. Leino, Peter Müller, and Jan Smans. Deadlock-free Channels and Locks. In ESOP 2010, volume 6012 of LNCS, pages 407-426. Springer, 2010. [PDF]
The refinement features in Chalice are shown in an episode of Verification Corner, and you can also read about them:
K. Rustan M. Leino and Kuat Yessenov. Stepwise Refinement of Heap-Manipulating Code in Chalice. 2010. [PDF]
- K. Rustan M. Leino, This is Boogie 2, no. MSR-TR-2008-194, 24 June 2008.