A High-Level Language for Modeling Algorithms and Their Properties - Formal Methods: Foundations and Applications - page 61

Table 1. Number of states for some algorithms

Algorithm #proc.original PlusCal our PlusCal

Peterson 2 37 23

FastMutex 2 2679 2679

Naimi-Trehel 3 111749 53905

far has been quite satisfactory: we found that we could represent the algorithms
in a natural way and never had to touch the generated TLA + models. Table 1
shows the number of (distinct) states generated by tlc for the original PlusCal
and the new PlusCal models of three algorithms: Peterson's algorithm [13], a
model of which is included in the original PlusCal distribution, Lamport's
FastMutex algorithm [7], a model of which appears in the PlusCal reference
manual [10], and the distributed mutual-exclusion algorithm due to Naimi and
Trehel [12], which is a refinement of Lamport's algorithm shown in Figs. 1 and 2.
Models of all but the most trivial algorithms, and in particular of distributed
algorithms, tend to be much clearer in our version of PlusCal.Thenumbers
in Table 1 indicate that the added expressiveness does not come at the expense
of lost e ciency in verification, as the state spaces generated from the new
PlusCal models are not bigger than those for the same algorithm written in
the original PlusCal. 4 In some cases, we obtain smaller numbers of states
because of lifted labeling restrictions. The running times of tlc for these small
examples never exceeded a few seconds. In future work, we believe that we can
achieve significant improvements by exploiting the information about locality in
PlusCal for implementing partial-order reductions.
The simplicity of translation to TLA + was an important design objective
for the original PlusCal language. In particular, it is tolerable that counter-
examples generated by the model checker are displayed in terms of the generated
TLA + model, which the user has to understand anyway. Some of our extensions,
and in particular nested processes with local variables, complicate the translation
and the interpretation of counter-examples. We intend to implement a filter for
displaying counter-examples in terms of the original PlusCal model.

5 Related Work

There are many languages for modeling concurrent and distributed algorithms.
Promela [4] is the modeling language for verification of distributed systems
using the Spin model checker. A Promela model consists of processes, channels
and variables. Promela does not support nested processes, has fixed primitives
for communication, and rather low-level representations of data (fixed-width
subsets of integers, records, and channels). It is therefore better suited to lower-
level descriptions of algorithms and protocols. On the other hand, Spin offers
more ecient verification techniques than tlc.

4 Moreover, handwritten TLA + models of these algorithms that have comparable
“grain of atomicity” generate similar numbers of states.