Extending PlusCal for Modeling Distributed Algorithms

Horatiu Cirstea, Stephan Merz

Abstract

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.

Available as: PDF

Reference

@InProceedings{cirstea:extending,
  author =       {Horatiu Cirstea and Stephan Merz},
  title =        {Extending {PlusCal} for Modeling Distributed Algorithms},
  booktitle = {18th Intl. Conf. Integrated Formal Methods (iFM 2023)},
  year =      2023,
  editor =    {Paula Herber and Anton Wijs},
  volume =    14300,
  series =    {Lecture Notes in Computer Science},
  pages =     {321-340},
  address =   {Leiden, The Netherlands},
  publisher = {Springer},
}