Extending PlusCal: A Language for Describing Concurrent and Distributed Algorithms

Sabina Akhtar (1) , Stephan Merz (1) , Martin Quinson (2)

1 VERIDIS - VERIfication pour les systèmes DIStribués
2 ALGORILLE - Algorithms for the Grid

The design of correct concurrent and distributed algorithms is notoriously difficult, and they are prone to errors such as deadlocks and race conditions. Model checking is one of the most successful formal techniques that are used to verify these algorithms. For example, TLC accepts models written in TLA+, a specification language based on mathematical set theory and the Temporal Logic of Actions. Such languages have a very different flavor from the (pseudo-)programming languages that algorithm designers typically use to express algorithms. PLUSCAL introduced by Leslie Lamport, is a high-level language for describing concurrent and distributed algorithms, from which TLA+ models are generated and then analyzed using TLC. Unfortunately, PLUSCAL suffers from a number of limitations that restricts its usefulness as an abstraction layer for the underlying TLA+ formalism.

Domaines: Autre [cs.OH]

Sabina Akhtar, Stephan Merz, Martin Quinson. Extending PlusCal: A Language for Describing Concurrent and Distributed Algorithms. Actes des deuxièmes journées nationales du Groupement De Recherche CNRS du Génie de la Programmation et du Logiciel, Mar 2010, Pau, France. ⟨inria-00544137⟩