**************************************************
* This is a user's manual for SLAP, version 0.1. *
* Copyright 2003, Joel Ouaknine.                 *
* Please read the LICENSE AGREEMENT at the end   *
* of this file before using SLAP.                *
**************************************************


Table of Contents:
------------------

1. Overview
2. Tutorial
3. Syntax guide
4. Notes for FDR/CSPm users
5. Comments on sample input files
6. Comments on the algorithm, general remarks, ongoing work
7. License agreement


1. Overview
-----------

SLAP is a Static Livelock Analyzer for CSP Processes. It takes as
input a CSP process in a sub-dialect of machine-readable CSP and
conservatively estimates whether the process may eventually diverge 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.

This user's manual assumes familiarity with the syntax and semantics
of CSP -- we refer the user to [Roscoe 1997] ("The Theory and Practice
of Concurrency", by A. W. Roscoe, Prentice-Hall International, 1997)
for a comprehensive account of the subject. We are also currently
preparing a paper, "Static livelock analysis in CSP", that describes
in detail the algorithms underlying SLAP; the paper will soon be
available on http://www.cs.cmu.edu/~ouaknine/pubs.html .

SLAP is implemented in ANSI-C by Joel Ouaknine based on ongoing joint
work with James Worrell. This is a beta release. Please send any bug
reports/comments/suggestions to joelo@andrew.cmu.edu . 
Thanks, and enjoy!


2. Tutorial
-----------

At the moment, SLAP can be compiled from a single C source file,
"slap.c", using, for instance, make or gcc. We assume the resulting
executable file is named "slap".

To run SLAP, you must first prepare an input CSP file containing a
description of the process you wish to test for livelock-freedom. The
syntax is a sub-dialect of machine-readable CSP, or CSPm. (CSPm is the
input language for the model checker FDR. More information on FDR and
CSPm may be found in [Roscoe 1997], as well as on the Formal Systems
(Europe) Limited website, http://www.fsel.com/ .) Some sample input
files (test1.csp to test4.csp) are included with this distribution;
information concerning these files can be found in Section 5.

A syntax guide for our sub-dialect of CSPm is given in the next
section. In an input file, the user can declare arbitrarily many
events, sets, renaming relations, and processes. The input file must
also contain a single final command, of the form "divcheck P", where P
is the process being investigated for livelock-freedom. Comments,
preceded by "--", are also allowed.

SLAP is then invoked by typing on the command line (on UNIX systems)
"./slap inputfile.csp", where "inputfile.csp" is the input file name.
SLAP will first analyze the contents of the input file. If it
encounters a syntax (or other) error, SLAP will output a (hopefully
helpful) error message together with the line number on which the
error was detected. Otherwise, SLAP will print out the whole alphabet,
sorted lists of all the user-defined sets and renaming relations, a
list of all user-defined processes, and the target process. SLAP will
then attempt to determine if the target process is livelock-free or
not.

If SLAP outputs "LIVELOCK-FREE", the target process is guaranteed to
be free of livelock over all its executions -- it will never become
divergent.

On the other hand, if SLAP outputs "POTENTIAL LIVELOCK", then no
definite conclusion can be drawn. 

When SLAP outputs "LIVELOCK-FREE", it also provides a "basis" for all
the "fair sets" of the process that it has found. A fair set S is a
subset of the process's alphabet with the property that any infinite
trace of the process is guaranteed to contain infinitely many events
from S. Any livelock-free process will have at least one fair set;
moreover, fair sets are upwards-closed: any superset of a fair set is
also a fair set. Thus SLAP lists only "minimal" fair sets, i.e., those
fair sets that are not supersets of any other fair set. The collection
of all such minimal fair sets is called a fair set "basis". It is,
by definition, unique.

SLAP computes fair set bases conservatively, i.e., in a sound but not
necessarily complete fashion: any set that it lists as fair is indeed
fair, but it may miss some fair sets.

SLAP can also be run with the option "-terse" 
("./slap -terse inputfile.csp"), in which case only the judgement
("LIVELOCK-FREE" or "POTENTIAL LIVELOCK") is output.

When preparing the input file, the user can choose to write down
processes using either the equational representation of recursion:

P = a -> Q
Q = b -> Q [] c -> P

or the functional representation of recursion:

P = mu X * (a -> mu Y * (b -> Y [] c -> X))

Only one style may be used in any given input file: one cannot mix the
equational and functional representations.

The default style is the equational style. However, since the
algorithms underlying SLAP assume the functional style, SLAP
translates vectors of mutually recursive equations into a single
functional process, using Bekic's theorem. The option "-bekic" makes
SLAP print out this translated process. 

In order to use the functional style directly, the option "-mu" must
be used.

The user may wish to immediately try SLAP with some of the sample
input files provided, test1.csp, test2.csp, etc. All of them use the
equational style.


3. Syntax guide
---------------

The CSP syntax that SLAP currently allows is a sub-dialect of
machine-readable CSP, or CSPm. The user familiar with CSPm may wish to
skip this section and instead consult the next one, in which we
highlight and discuss some differences between our syntax and
CSPm. All users are also invited to examine and run SLAP on some of
the input files included with this distribution (test1.csp to
test4.csp).

Our syntax follows very closely that of CSP; cf. [Roscoe 1997].

An input file usually defines a number of events, using the reserved
word "channel", as follows:

channel a,b,c
channel train.in, train.out

This defines five events. Events do not have to be defined all at
once, but they must be defined before they are used. Any number of
events may follow the reserved word "channel", but they must all be on
the same line. Each "channel" declaration must use a new line. 

Valid event names are identifiers (defined next) that are not reserved
words and that have not already been used. An identifier is any finite
string of (case-sensitive) alphanumeric characters, "_" (underscore),
"."  (period), and "'" (prime/apostrophe). Blank spaces (spaces and
tabs) between events are ignored, but events in a given "channel"
declaration must be separated by commas.

The user may also define any number of sets and renaming relations,
which are essentially macros to be subsequently used in process
definitions. For example,

S = {a,b,c}

defines a set S consisting of three elements. Set names and renaming
relation names must be identifiers. Set definitions must begin on a
new line, but may afterwards use as many lines as is desired: blank
spaces and newline characters are ignored.

The reserved word "SIGMA" stands for the set of all events (the
alphabet). Since "SIGMA" is evaluated only after the entire input file
has been read, "SIGMA" may include some events that are only defined
after it is used.

Much of what we said about sets holds for renaming relations. For
example, 

R = [a<-b, a<-c, train.in<-train.out]

defines a renaming relation R such that a R b, a R c, 
train.in R train.out, and every event other than "a" and "train.in" is
R-related to itself. Blank spaces and newline characters may be used
freely but must not break-up the "<-" symbol.

The general rule for defining renaming relations is this: in a given
renaming relation, if an event is never mentioned on the left-hand
side of a "<-" symbol, then it is assumed to be related to itself and
only to itself. If, on the other hand, an event is mentioned on the
left-hand side of a "<-" symbol, then that event relates to the event
on the right-hand side of the "<-" symbol, but not to itself, unless
somewhere in the renaming relation is there also a "<-"-assignement
specifically relating the event to itself.

As a matter of the semantics of renaming, let us record here that
(a -> STOP [] b -> STOP)[[a<-b]] is equivalent to b -> STOP rather
than to a -> STOP.

Processes are built according to the following grammar:

P = STOP         deadlock 
    a -> Q       prefix
    SKIP         successful termination
    P1 |~| P2    internal choice
    P1 [] P2     external choice
    P1 [|S|] P2  synchronized parallel 
    P1 ||| P2    interleaving
    P1 ; P2      sequential composition
    Q\S          hiding
    Q[R]         renaming      
    Q            process definition
    mu X * Q     recursion

In the above, "a" stands for an arbitrary event, "S" for an arbitrary
set, "R" for an arbitrary renaming relation, and Q, P1, and P2 for
arbitrary processes. Recursion is only allowed with the "-mu" option
on; in that case, the variable "X" is allowed to occur freely (as if
it were a bona fide process) within "Q"'s syntax. When the "-mu"
option is on, the process definition clause (and others) may still be
used, but only if Q (or P1, P2, etc.) is a fully defined process;
mutual recursion is not allowed with the "-mu" option.

Like sets and renaming relations, process names must be identifiers,
and processes are defined on a new line by using the "=" sign; for
example,

P = a -> P'
P' = b -> P

are valid definitions for both P and P' (when the "-mu" option is
off). Process definitions may be split over several lines.

Note that if R = [a<-b], you could write indistinguishably, e.g., 
Q[R] and Q[[a<-b]], but not Q[[R]] nor Q[a<-b], and likewise for sets.

Remark: Our semantics assumes that termination is distributed; in
other words, all components of a parallel process must terminate (with
a tick) for the whole process to terminate.

Operator precedence, from most tightly binding to most weakly binding,
is: 

1) Hiding and renaming
2) Prefixing and sequential composition
3) Internal and external choice
4) Parallel (and interleaving) operators
5) Recursion (mu) operator

Of course, parentheses may be used at will. Whenever associativity is
ambiguous, the operators associate to the left.

Finally, the input file must end with the command

divcheck P

where P is a process. The "divcheck" command must be on a new line,
but the process P may be split over several lines.

Comments may appear anywhere in the file where blank space would be
allowed. A comment is initiated by "--". Anything on a line following
"--" is ignored.


4. Notes for FDR/CSPm users
---------------------------

The syntax we use is a very restricted sub-dialect of machine-readable
CSP, or CSPm. SLAP essentially supports the whole of pure CSP syntax,
but not much more.

Events are defined using the "channel" declaration. However, no
datatype definitions or any kind of event constructors are
allowed. Although the "." (period) character is allowed, it is not a
event/channel constructor and is in fact indistinguishable from the
other identifier characters, i.e., (case-sensitive) alphanumeric
characters, "_" (underscore), and "'" (prime/apostrophe).

Our CSP operators have the same precedence and default associativity
as they do in CSPm; the operators allowed are those of pure CSP, the
list of which is given in Section 3. We do not have indexed/replicated
operators or parameterized recursion, but we do allow mutual recursion
(when the "-mu" option is off).

It is possible to define sets and renaming relations as "macros", as
in

S = {a,b,c}
R = [a<-b,b<-c]

P = Q[R] ||| d -> P\S

which is equivalent to

P = Q[[a<-b,b<-c]] ||| d -> P\{a,b,c}

Lastly, the "divcheck" command, as in

divcheck P

is semantically equivalent to the FDR command

assert CHAOS [FD= P

where CHAOS is defined to be the most nondeterministic livelock-free
process. There can however only be one "divcheck" command per input
file, and it must be the last item of the input file.

As in CSPm, comments are inserted by first typing "--"; any remaining
text on the line is ignored.


5. Comments on sample input files
---------------------------------

This distribution includes the following four sample input files,
test1.csp, test2.csp, test3.csp, and test4.csp.

test1.csp shows a simple livelock-free parallel process which a naive
analysis might classify as divergent. SLAP correctly evaluates
livelock-freedom.

test2.csp implements the infinite buffer B+ from 
[Roscoe 1997, p.103 and p.188]. In that text, an interesting and
instructive argument is given to show that B+ is livelock-free.
Indeed, this judgement is confirmed by SLAP. Note that B+ is an
infinite-state process, and can therefore not be handled by FDR.

test3.csp implements a toy example which dramatically highlights the 
efficiency of SLAP versus FDR in certain cases. test3.csp consists of
seven 10-state counters in non-synchronized (interleaved) parallel.
The resulting process therefore has 10 million states.
SLAP instantly recognizes the process to be livelock-free, but it 
takes FDR 2.78 approximately 10 minutes to reach the same conclusion
on a Pentium 4 2.00 GHz with 900 MB of RAM. (Using FDR's built-in
livelock-checking option is marginally faster, saving about a minute. 
On the other hand, compression techniques are of little use here,
since counters are notoriously refractory to them.)

test4.csp implements a toy communication protocol which illustrates
one of the ways in which SLAP is (currently) incomplete: SLAP wrongly
calculates the fair set basis of a particular process, so that if 
certain events are hidden, SLAP incorrectly assesses potential livelock.


6. Comments on the algorithm, general remarks, ongoing work
-----------------------------------------------------------

The algorithm underlying SLAP is sound but not complete, in that it
never flags a divergent process as "LIVELOCK-FREE", but may assign a
judgement of "POTENTIAL LIVELOCK" to a genuinely livelock-free
process (cf. test4.csp). That is because SLAP performs a "static"
analysis of processes, as opposed to a full state-space search such as
that carried out by FDR. 

On the flip-side, SLAP often terminates dramatically faster than FDR
(cf. test3.csp). SLAP is also able assign correct "LIVELOCK-FREE"
judgements to many "infinite-state" processes, such as 
P = a -> (P ||| P), which defeat FDR.

In general, for a fixed alphabet, the time complexity of SLAP is
linear in the syntactic size of the target process in the functional
(mu) representation. The algorithm, based on Bekic's theorem,
converting equational processes to their functional representation in
the worst case increases the size of the process quadratically,
although in our experience this seems to occur very rarely in practice
(the conversion is usually linear or slightly above linear). At any
rate, this makes the time complexity of SLAP worst-case quadratic in
the syntactic size of the target process in equational form. This
compares very favorably with the size of the state-space of the
process (which model checkers must deal with), which is usually
exponential in the syntactic size of processes.

When the alphabet is not fixed, the time complexity of SLAP is
unfortunately worst-case exponential in the size of the
alphabet. Although the exponential blow-up occurs very rarely in
practice, we have encountered it in some examples. In those cases, we
have found that modifying parts of the algorithm to use
state-of-the-art SAT solving technology helps tremendously. In our
prototype implementation, we have used the SAT solver ZChaff
(available from http://ee.princeton.edu/~chaff/zchaff.php) and have
been able to handle all previously problematic examples so far. We are
currently polishing this implementation and will release it in the
near future.

The algorithm underlying SLAP is based on an extension of Roscoe's
treatment of guarded recursions in [Roscoe 1997, Chapter 8]. As stated
in Section 1, we are currently preparing a paper on the subject.
We are also currently working on the following:

* Make SLAP complete for finite-state (tail-recursive) processes by
  iteratively unwinding processes and eliminating parallel operators.
  When no parallel operator remain, the SLAP judgement is exact, and
  "POTENTIAL LIVELOCK" means genuine livelock. However, a 
  "LIVELOCK-FREE" judgement may be obtained much sooner, after only
  a few unwindings.

* Work directly with processes in equational form, without first
  converting to functional form via Bekic's theorem.


7. License Agreement:
---------------------

 Copyright 2003, Joel Ouaknine (hereinafter AUTHOR). All rights
 reserved.  By using this software the USER indicates that he or she
 has read, understood and will comply with the following:

 --- AUTHOR hereby grants USER nonexclusive permission to use, copy
 and/or modify this software for internal, noncommercial, research
 purposes only. Any distribution, including commercial sale or
 license, of this software, copies of the software, its associated
 documentation and/or modifications of either is strictly prohibited
 without the prior consent of AUTHOR. Title to copyright to this
 software and its associated documentation shall at all times remain
 with AUTHOR. Appropriate copyright notice shall be placed on all
 software copies, and a complete copy of this notice shall be
 included in all copies of the associated documentation.

 --- This software and any associated documentation is provided "as is"

 AUTHOR MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS OR IMPLIED,
 INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A PARTICULAR
 PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR ASSOCIATED
 DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, TRADEMARKS
 OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.

 AUTHOR shall not be liable under any circumstances for any direct,
 indirect, special, incidental, or consequential damages with respect
 to any claim by USER or any third party on account of or arising from
 the use, or inability to use, this software or its associated
 documentation, even if AUTHOR has been advised of the possibility of
 those damages.
----------------------------------------------------------------------
