Skip to Main content Skip to Navigation
Conference papers

An Extension of PlusCal for Modeling Distributed Algorithms

Heba Alkayed 1 Horatiu Cirstea 2 Stephan Merz 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Tuesday, February 16, 2021 - 7:20:20 PM
Last modification on : Wednesday, November 3, 2021 - 7:09:21 AM
Long-term archiving on: : Monday, May 17, 2021 - 9:14:13 PM


Files produced by the author(s)


  • HAL Id : hal-03143502, version 1


Heba Alkayed, Horatiu Cirstea, Stephan Merz. An Extension of PlusCal for Modeling Distributed Algorithms. TLA+ Community Event 2020, Oct 2020, Freiburg (online), Germany. ⟨hal-03143502⟩



Les métriques sont temporairement indisponibles