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

fairness assumptions assumed about the algorithm's execution, which underly
the proof of liveness properties. Rather, the user must add these as temporal
logic formulas to the module generated by the PlusCal compiler. It is therefore
necessary to understand not only TLA + , but also the translation of PlusCal
to TLA + . An effort was made in the design of the PlusCal language to keep
the translation simple. For example, the compiler tries to preserve the names
of PlusCal variables in the TLA + specification. However, this is not always
possible, for example if variables of the same name are declared in different
procedures. Also, local variables of processes are represented as arrays in TLA + ,
and the user must be aware of this when annotating the TLA + model.
Lack of process hierarchy and of scoping. Another serious restriction motivated
by the need for a simple translation is that PlusCal processes can only be
declared at top level, without any nesting. As we will illustrate in section 3 using
Lamport's distributed mutual exclusion algorithm, many distributed algorithms
are more naturally expressed using hierarchies of processes.
A related issue is the lack of scoping rules in PlusCal. Although variables
may be declared locally to processes, scoping is not enforced and local variables
can in fact be accessed throughout the program. Beyond being a possible cause
of errors, the lack of a proper hierarchy of processes and of scoped local variables
makes it much more dicult to implement optimizations for verification, such
as partial-order reduction.
Restrictions in specifying atomicity. An important concern in modeling con-
current and distributed algorithms is the specification of the proper unit of
atomicity: which (blocks of) statements can be considered to be executed with-
out interleaving with statements of other processes? Whereas too coarse-grained
atomicity may hide errors that arise in the implementation due to unexpected in-
terleavings, too fine-grained atomicity introduces unnecessary details and causes
state space explosion in verification. PlusCal uses a simple but powerful idea
for expressing atomicity: the user may decorate statements with labels, and in-
terleaving is only allowed at labeled statements. However, the user is not entirely
free where labels may or may not be placed, as these are also serve for internal
purposes of compilation. Typically, more labels must be introduced than would
be necessary, hence aggravating state space explosion.
Technical limitations. Lamport's PlusCal imposes a number of other limita-
tions, again motivated by the desire to keep the translation simple. For example,
although sets are the basic construct for representing data, PlusCal does not
contain a primitive for iterating over the elements of a set. The programmer has
to introduce an auxiliary variable for iteration and keep track of the elements
that have already been handled. Without special care, these auxiliary variables
will again lead to state space explosion during model checking. Another technical
restriction enforced in PlusCal is to disallow multiple assignments to the same
variable within an atomic step.