Sat Oct 3 20:33:50 CEST 2009
SPIN/Promela and TLC/TLA+ by Jose Faria. The paper compares two
formal specification tools based on a case study: an algorithm to deal
with non-blocking linked-lists based on the compare-and-swap (CAS addr
old new) instruction. CAS atomically compares the contents of a
location addr with an old replaces it with a new value in case of a
match, returning a boolean to indicate whether the substitution took
place or not.
This primitive allows to detect significant conflicts in the case of
list operations: some other process might have modified the list in
such a way that is incompatible with the intermediate state of a list
operation, in which case the whole operation can simply be restarted
based on the result of the CAS.
TLA+ is a specification language for describing and reasoning about
asynchronous nondeterministic concurrent systems. TLC is an
explicit-state model checker for specs written in TLA+. A spec in
TLA+ is summarized in a single formula that describes a state machine
in erms of an initial condition, a next state relation and possibly
some liveness conditions.
Promela is the specifically developed input language of SPIN, an
on-the-fly explicit-state model checker (as TLC, while TLC was
designed after TLA+).
The Wikipedia page on linear temporal logic (LTL) summarizes the
useful properties as the ability to express safety (something bad
never happens) and liveness (something good keeps happening).