aLive: The Livelock Freedom Checker for Asynchronous Reactive Systems

aLive is a livelock freedom checker for Promela models. In a Promela model, a certain set of statements may have "progress" labels indicating that the executions of these statements are regarded as making progress during the execution of the model. If the model is a reactive system, i.e., it is supposed to run forever and serve the requests from its users, then at least one of these progress statements must be repeated infinitely often. If it happens that none of these statements will ever be repeated, then we have a livelock situation. If the model does not have any livelocked execution, then it is said to be livelock free.

aLive is written in Visual C++. Like IBOC, it uses "lp_solve" as its ILP solving engine. Currently, it has no graphic user interface and runs only on Windows.

The Theory Behind
Usage & Screenshots
Maintenance Status
Release
Future Development

The Theory Behind

We sketch the idea of livelock freedom checking here. For more details, we refer readers to the paper [LSW06].

Like the buffer boundedness test as implemented in IBOC, our livelock freedom checking method is an iterative procedure that involves counterexample-driven abstraction refinement. At the beginnig of the checking, we abstract from arbitrary Promela code, message orders, cycle dependencies, etc. This is completely the same as for the buffer boundedness test. The resulting system is a set of control flow cycles with their message passing effects described as integer vectors. Each component in such an integer vector, called effect vector, corresponds to one type of messages exchanged in the model. On the effect vectors of the collected cycle, we give a necessary condition for the existence of a livelocked execution: there exists a non-negative linear combination of cycle effects such that no cycles containing progress statements are in the combination. Such a combination can be repeated forever during which no progress statements get ever executed. This condition is encoded into an Integer Linear Programming (ILP) problem. If the ILP problem has no solutions, then the model is free of livelock. Otherwise, we can construct a counterexample from a particular ILP solution. A counterexample can be real or spurious. Therefore, we employ cycle dependency discovery methods to detect spurious counterexamples, and use the discovered dependency to refine the abstraction. The livelock freedom test described above is incomplete and may return "UNKNOWN" for some models.

Usage & Screenshots

For a Promela model, one has to use the following SPIN commands to generate two files from the model: a "*.cfsm" file containing a textual reprensentation of the state machine behavior of each proctype; and a "*.sym" file containing the list of identifiers/symbols used in the model.

spin -a MODEL_FILE
gcc -c pan pan.c
pan -d > MODEL_FILE.cfsm
spin -d > MODEL_FILE.sym

Maintenance Status

aLive is continously maintained and extended with new functions and techniques.

Release

There is no public release of aLive right now.

Future Development

We aim to build an open software model verification tool set based on the ILP solving techniques that we develop within the IMCOS project. This would bring better code reuseability and extendability for the implementation of other property checking methods. We will first integrate the buffer boundedness test and the livelock freedom test into the tool set.

Furthermore, we will work on improving the code quality and the user interface of aLive.