The easy parallel algorithm specification language
MIT License
The easy parallel algorithm specification language.
This is a small, imperative, untyped, pseudocode-like language for describing simple parallel algorithms. The language "compiles" to TLA+ so that it can be exhaustively checked.
There are no binary distributions. You will need to install the Stack build system and compile this tool from source:
git clone https://github.com/Calvin-L/ezpsl.git
cd ezpsl
stack build
stack test # optional!
cp `stack exec -- which ezpsl` .
Usage:
./ezpsl FILE
If the file is a .tla
file, then the tool looks for a line of the form
\* #include FILE.ezs
and replaces that line with the compiled TLA+ code.
If a compilation was previously done, then the old compilation is replaced with
the new one.
If the file is a .ezs
file, then the tool prints the compiled TLA+ code on
standard out.
You can use the -o OUT
option to control where the output gets written,
regardless of the input file extension.
For instance, to compile the Test example, run:
./ezpsl examples/Test.ezs
Or, to update the Test TLA+ module, run:
./ezpsl examples/Test.tla
Example file:
\* ----------------
\* Global variables
var v1 := 2;
var v2 \in {3, 4};
\* ----------------
\* Procedures
proc helper(x) {
var tmp := x + 1;
return tmp;
}
@entry
proc main() {
v1 := call helper(v2);
}
Comments begin with \*
and are completely ignored by the tool.
All global variables must be listed before any procedures, and local variables
within a procedure must be declared first, before any statements in the
procedure. Variables must be initialized. They can either be initialized with
an exact value using :=
or nondeterministically (as an arbitrary element of a
set using \in
or as an arbitrary subset of a set using \subseteq
).
Procedures may be listed in any order.
Each procedure may have zero or more annotations. Annotations may be listed in any order.
@entry
annotation indicates that a procedure is an "entry point",@entry
@can_restart
annotation indicates that a process can crash and restartyield
or await
point, or after terminating. This annotation has@entry
.Expressions: a subset of TLA+ including integers and records. Additionally,
the special constant self
refers to the current thread ID. EzPSL also has a
different set-comprehension syntax than TLA+. For example:
{ f[x] : x <- S, x > 0 }
- find all positive elements of S
andf
to each one.The TLA+ comprehensions {x \in S : P}
and {e : x \in S}
are not supported,
since they can be expressed using the general set-comprehension primitive.
Statements:
x := e;
- assignmentpick x \in set : predicate;
- nondeterministic choice. You may omit the: predicate
part, in which case the predicate defaults to TRUE
. If the\subseteq
instead of \in
as a shorter way to writepick x \in SUBSET set;
.if (e) { s } else { s }
- if-then-elsewhile (e) { s }
- loopingeither { s } or { s }
- nondeterministic branchingskip;
- no-opyield;
- pause the current thread and allow others to runawait e;
- wait for a condition to become true. There is an impliedyield
before each await
.assert e;
- assert that the expression is truecall p(arg, arg, ...);
- call a procedure and ignore its return valuex := call p(arg, arg, ...);
- call a procedure and save its return value.call
statement.return e;
- return a value. If the expression is omitted (return;
),EzPSL's TLA+ output always requires that your specification EXTENDS
the
following built-in modules:
Sequences
(for modeling the call stack)Integers
(for comparing sequence lengths)TLC
(for constructing maps using the :>
and @@
operators, and forPermutations
operator)The generated TLA+ declares the following constants:
PROC_calls
for each @entry
procedure, where PROC
is the procedure_Undefined
, a special token that is used for a number of purposes. DuringThe generated TLA+ declares the following variables:
var
in the code, with the exact same names_pc
(a stack of program counter values for each process)_frames
(a stack of "call frames" for each process, containing local variables)_globalsScratch
(the actor's scratch space for globals between yield points)_ret
(the most recently returned value for each process)_actor
(the thread that is currently acting, or _Undefined
if anyThe generated TLA+ declares the following operators:
Init
(the initial state predicate)Next
(the next action predicate)symmetry
(a symmetry set consisting of all process IDs)vars
(a tuple of all declared variables, including internal variables)NoAssertionFailures
(an invariant stating that no process fails anassert
)NOTE: The generated TLA+ system uses one step per statement, meaning that a logically atomic block of code goes through multiple TLA+ states. However, the global variables only change when a process yields or terminates. Between yield points, processes use a private snapshot of the global variables and all changes are applied simultaneously when the process yields or terminates.
If you are curious for more details about the TLA+ output, look through the
compiled TLA+ output in the examples
folder.
The compiled TLA+ code always contains an invariant definition named
NoAssertionFailures
asserting that no process has failed an assert
statement. You can tell TLC to check NoAssertionFailures
as an invariant to
find assertion failures.
To write a global invariant, place the invariant's definition after the compiled output. Even if a process makes multiple changes to the global variables between yield points, the global variables are only modified when the process yields. Therefore, your invariant will never "see" intermediate states between yield points.
Refinement works the same way as global invariants. See
examples/Refinement.tla
for an example.
EzPSL generates TLA+ that supports deadlock checking. Deadlock checking is enabled by default in TLC.
EzPSL is similar to PlusCal, another simple imperative language that can be compiled to TLA+ for model checking.
There are a few ways in which EzPSL is better than PlusCal:
yield
statements.yield
There are also ways in which PlusCal is better than EzPSL: