SLAP: A
Static
Livelock
Analyzer for CSP
Processes
SLAP is a static livelock (or divergence) analyzer for CSP
processes. It takes as input a CSP process in a sub-dialect of
machine-readable CSP (CSPM) and conservatively estimates
whether the process can eventually livelock or not. If SLAP outputs
"LIVELOCK-FREE", then the process is genuinely livelock-free. However,
if SLAP outputs "POTENTIAL LIVELOCK", then no definite conclusion can
be drawn.
The source code for SLAP, version 0.1, is available for free download. Please read the
README file for licensing agreements.
The present distribution includes the source code (in ANSI-C), a
user's manual, and several sample input files.
Using SLAP requires familiarity with the syntax and semantics of CSP
-- we refer the user to the book
The Theory and Practice of Concurrency, by A. W. Roscoe,
Prentice-Hall International, 1997, for a comprehensive account of the
subject.
SLAP was implemented by Joel Ouaknine based on ongoing joint work
with James Worrell.
This is a beta release. Please send any bug
reports/comments/suggestions to REMOVE_THIS_joel@cs.ox.ac.uk.
Thanks, and enjoy!
Back to Joel Ouaknine's
home
page
Last updated in June 2005