An Extension of PlusCal for Modeling Distributed Algorithms

Overview & Synopsis

The PlusCal language combines the expressive power of TLA+ with the “look and feel” of imperative pseudo-code in order to allow users to express algorithms at a high level of abstraction. PlusCal algorithms are translated to TLA+ specifications and can be formally verified using the TLA+ Toolbox. We propose a small extension of PlusCal, tentatively called Distributed PlusCal, intended for simplifying the presentation of distributed algorithms in PlusCal. Distributed systems consist of nodes that communicate by message passing. It is convenient to model a node as running several threads that share local memory. For example, one thread may execute the main algorithm, while a separate thread listens for incoming messages. Although PlusCal offers processes, they have a single thread of execution. Different threads of the same node must therefore be modeled as individual processes, and variables representing the local memory of a node must be declared as global variables, obscuring the structure of the code. Our first extension allows a PlusCal process to have several code blocks that execute in parallel. Besides, Distributed PlusCal explicitly identifies variables representing communication channels and introduces associated send and receive operations. In contrast to using ordinary variables and writing macros or operator definitions for channel operations, making channels part of the language gives us some more flexibility in the TLA+ translation.