Extending PlusCal for Modeling Distributed Algorithms

PlusCal is a language for describing algorithms at a high level of abstraction. The PlusCal translator generates a TLA+ specification that can be verified using the TLA+ model checkers or proof assistant. We describe Distributed PlusCal, an extension of PlusCal that is intended to facilitate the description of distributed algorithms. Distributed PlusCal adds two orthogonal concepts to PlusCal: (i) processes can consist of several threads that share process-local variables, and (ii) Distributed PlusCal provides communication channels with associated primitives for sending and receiving messages. The existing PlusCal translator has been extended to support these concepts, and we report on initial experience with the use of Distributed PlusCal.