An Extension of PlusCal for Modeling Distributed Algorithms - Archive ouverte HAL Access content directly
Conference Papers Year :

An Extension of PlusCal for Modeling Distributed Algorithms

(1) , (2) , (1, 2)


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.
Fichier principal
Vignette du fichier
abstract.pdf (243.58 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03143502 , version 1 (16-02-2021)


  • 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⟩
106 View
159 Download


Gmail Facebook Twitter LinkedIn More