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

inserted into the TLA + model generated by the compiler, requiring the user to
understand not only TLA + but also the translation. We do not expect users to
understand our compiler in any detail, or even to read the generated TLA + file.
Nested processes and scoped declarations. We allow for nested process declara-
tions, and this leads to a clearer representation of the (communication) structure
of algorithms. In our running example, we were able to declare the variables of
each site as local variables, with two threads (the main Site process and the
Communicator ) accessing them. In the original PlusCal, one would either have
two top-level process types that need to communicate via global variables (which
then must be declared explicitly as arrays by the user) or insert the message-
handling code between all transitions of the Site process. In either case, the
model becomes hard to understand, contradicting the purpose of a high-level
modeling language.
Unlike the original PlusCal, our compiler enforces proper scoping of vari-
ables, procedures, and definitions, avoiding potential errors by inadvertently ac-
cessing the variables of a different process. In future work, we plan to take advan-
tage of this locality information in order to implement partial-order reductions
for optimizing model checking.
More flexibility. As discussed in Section 3.2, the basic idea in PlusCal is to
specify atomicity via labels. We managed to lift some of the restrictions on label
placement that were present in the original PlusCal language, and our compiler
will add labels when they are required. The user can now enforce atomicity of
code blocks containing labels using the new atomic statement.
We also introduced several extensions, such as the for statement for iterating
over a set, or the possibility to have several assignments to the same variable
within a group of statements. On the technical side, we strived for better modu-
larity of translation so that it becomes easier to experiment with new language
primitives.
While our PlusCal variant retains most of the “look and feel” of the original
PlusCal language, it does not guarantee backward compatibility. For example,
programs that modify variables that are not currently in scope will be rejected
by the new PlusCal compiler. The current version also does not provide macros
that exist in Lamport's PlusCal.
There are many features that we deliberately did not implement. For example,
PlusCal does not provide primitives for message passing between processes.
Distributed algorithms use many different forms of message passing (synchronous
or not, lossy, duplicating, order preserving, . . . ), and these are better defined in a
standard library of procedures or definitions than hard-wired into the language.
4 Experiments
We have tested our language and implementation by modeling several concurrent
and distributed algorithms in it and verifying them using tlc. Our experience so