An Extension of PlusCal for Modeling Distributed Algorithms - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2020

An Extension of PlusCal for Modeling Distributed Algorithms

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

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

Identifiants

  • HAL Id : hal-03143502 , version 1

Citer

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⟩
149 Consultations
187 Téléchargements

Partager

Gmail Facebook X LinkedIn More