Sat Oct 3 20:33:50 CEST 2009

Formal methods

SPIN/Promela and TLC/TLA+ by Jose Faria.  The paper[1] 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+[4] 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)[5] summarizes the
useful properties as the ability to express safety (something bad
never happens) and liveness (something good keeps happening).

[1] http://www.openlicensesociety.org/docs/FMethodsReport_ComparisonTLASpin.pdf
[2] http://en.wikipedia.org/wiki/Promela
[3] http://en.wikipedia.org/wiki/Temporal_logic
[4] http://en.wikipedia.org/wiki/Temporal_logic_of_actions
[5] http://en.wikipedia.org/wiki/Linear_temporal_logic