StEAM, (State Exploring Assembly Model checker) is a model checker for native concurrent C++ programs.It extends a virtual machine - called ICVM - to perform model checking directly on the assembly level. This document gives you the basic information needed to install and use StEAM. The example programs included in the installation package are supposed to show the current capabilities of StEAM. However, we encourage you to try to verify your own programs. This manual will also explain the steps needed to prepare a piece of software for verification with StEAM. For detailed information about the internals of the model checker, we refer to Technical Reference of StEAM.
The installation instructions assume that StEAM will be installed on a Linux system using gcc. StEAM is based on the Internet Virtual Machine (IVM). The IVM package comes with source code for the compiler and the virtual machine (vm) itself. In the course of the StEAM project only the vm needed to be enhanced, while the compiler was left unchanged. The task of building igcc - the compiler of IVM, will hence be assigned to the user. The rest of the model checker, including the modified virtual machine can either be obtained as a binary package for Linux or as a source package. The source package can be compiled for use on Linux and Cygwin (a Linux-like environment for Windows).
The original source package of IVM can be downloaded from the http://bugfinder.sourceforge.net. The package was found to compile with older versions of gcc (e.g. 2.95.4). However, later versions such as 3.4.4 require considerable changes to the makefile in order to build igcc.
We have debuged a few minor bugs in igcc and rewritten some Makefiles to be able to make binary packages for igcc. At a present, you can find Debian and RPM Packages at http:/bugfinder.sourceforge.net. Feel free to test the packeges, considering they are in beta status at a time.
After unpacking source package, you will find 4 subdirectories: binutils, gcc, lib and include. First check if you have right gcc version on your machine. Output should be something like this:
gcc -v
Reading specs from /usr/lib/gcc-lib/i386-linux/2.95.4/specs
gcc version 2.95.4 20011002 (Debian prerelease)
Everything fine, active is gcc-2.95. If you have more as one gcc version installed, some other version could be active. Please set correct symbolic links:
ln -sf /usr/bin/gcc-2.95 /usr/bin/gcc
ln -sf /usr/bin/g++-2.95 /usr/bin/g++
Now you have to install binutils:
cd binutils
make
make install
After that, you have to install the igcc compiler itself:
cd ../gcc
make
make install
If everything went fine, you shold be able to compile something. In gcc directory is also the file test.c. There are no libraries installed yet, but you can test by typing
igcc -S test.c
You should be able to edit and view the machine language file test.s.
Igcc is a cross-compiler, which means it compiles on your machine binary code for steam virtual machine. To do so he need some libraries. Standard libraries are included in lib directory, otherwise you couldn't compile igcc at all. The last step we need to do is to make static libraries:
cd ../lib
make
make install
Done! Your igcc compiler is ready to use. If something went wrong, reffer to INSTALL and README sections in directories mentioned above, or mail us.
There is not much to say here - you have to install first ivm-binutils and then ivm igcc package. Packages are build on i686, but shoul run on any Intel or AMD. You have some other processor - you can still compile the sources, configure file is able to check which processor you have.
After unpacking source package, you will find 3 subdirectories: docs, models and src. To compile StEAM, you'll need 3 libraries source packages: libX11, libICE and libxml2 from your favorite linux distribution. Makefile assume that they are in /usr/lib/, or you have to modify Makefile to set a proper path. After installing libraries, we can compile StEAM.
You should be able to compile StEAM with gcc or some other compiler, but it has not be tested enough. We had success with gcc 2.95, 3.3 and 3.4. We suggest gcc-3.4 with libc++6. First check if you have right gcc version on your machine. Output should be something like this:
gcc -v
...
gcc version 3.4.4 20050314 (prerelease) (Debian 3.4.3-13)
Everything fine, active is gcc-3.4. If you have more as one gcc version installed, some other version could be active. Please set correct symbolic links:
ln -sf /usr/bin/gcc-3.4 /usr/bin/gcc
ln -sf /usr/bin/g++-3.4 /usr/bin/g++
Now you have to install StEAM:
cd src
make
make install
If everything was fine, you should be able to start steam:
steam
Usage: steam <[-optargi]> <progname> [<prog. arguments>]
steam -h or --help for detailed information and examples.
Reffer to section A First Example to learn how to use StEAM.
After installing igcc packages and downloading steam package for your linux distribution, install it. Packages are i686-build and compiled with gcc-3.4. For other processors recompile from source could be nessesery.
If you followed the instructions in section Installation, you should now be able to check one of the example programs. If you obtained source package, you have in $STEAM_VERSION/models small collections of test programs. Otherwise, obtain newest models archive from http://bugfinder.sourceforge.net/. After unpacking, change to models directory.
You can see here a few subdirectories. Go to the directory philosophers, which has C++ implementation of well known dining philosophers problem:
cd philosophers
There are two versions, with and without deadlock. Deadlock is intended error, to show function of StEAM. If you look at the content of Philosopher_err.cc (e.g. with less Philospher_err.cc), you will notice, that it basically does locks and unlocks two global variables which were passed to the constructor function. The file philosophers.c contains the main() method which generates and starts the threads.Let's see it now:
cd deadlock
ls
Philosopher_err.cc
Philosopher_err.h
philosophers.c
We have programed a mfgen, the tool that produces a Makefile automaticly. To include all present file in Makefile to be compiled, and compile it after, do
mfgen -f *
make
make will first apply annotations to the .c and .cc source files. After this, the example program is compiled and linked with ig++ - the compiler of IVM. Do another directory listing and you will see the following:
Makefile
Philosopher_err.cc
Philosopher_err.cc_ext.c
Philosopher_err.h
Philosopher_err_ex.o
philosophers.ivm
philosophers_ex.o
philosophers.c
philosophers.c_ext.c
The source files containing an ext.c ext.cc in their name were produced by the source annotation tool extcml. The file philosophers.ivm is the IVM-object file compiled from the annotated source files. Start the model checker on the example program by typing:
steam philosophers.ivm 2
This will start the model checker with the default parameters on the compiled program philosophers.ivm parameterized with '2'. In the case of the dining philosophers, this means that 2 instances of the thread class Philosopher are created. The typed command will produce the output of some standard information from the model checker, followed by the report of a detected deadlock, an error trail and some statistics - such as the number of generated states, memory requirements etc. Each line of the error trail tells us the executed thread, the source file and line number of the executed instruction. Here, Thread 1 refers to the main program, while Thread 2 and Thread 3 correspond to the first and second instance of Philosopher. However, the error trail may seem a bit lengthy for such a small program. Now type:
steam -a bfs philosophers.ivm 2
This tells the model checker to use breadth-first (BFS) search (instead of depth-first, which is the default search algorithm). The error trail produced by BFS will be significantly shorter than the first one. You may want to compare the source files with the information given in the trail to track down the deadlock. Alternatively, you can add the parameter --source-trail to the command line. This prints the error trail as actual source lines - rather than just as line numbers. Apparently, a deadlock occurs if both Philosophers lock their first variable and wait for the respective other variable to be released.
StEAM is invoked by a call:
steam <[-optargi]> <progname> [<prog. arguments>]
The options are declared so:
<progname> is the name of the program to be checked.<prog. arguments> are the parameters passed to the program to be checked<[-optargi]> are optional model checker parameters.
steam -h
In the current version, StEAM supports depth-first search (default), breadth-first search (-a bfs),depth-first iterative deepening (-a idfs) and the heuristic search algorithms best-first (-a best) and (-a astar). The latter two additionally require that a heuristic is given (see
Heuristics).
Also note, that IDFS is only effective in combination with bitstate-hashing (see below).
For detailed information about each heuristic, we refer to Technical Reference. The heuristic to use is specified by the parameter -c or --heuristic <hname>, where<hname> is from one of the follwing groups.
These heuristics are specifically tailored to accelerate the search for deadlocks, but will in general not be helpful for finding other errors, such as assertion violations. StEAM currently supports the deadlock heuristics: mb, lnb, pl1, pl2, pb1 and pb2. For example:
steam -a best --heuristic lnb philosophers.ivm 30
Uses best-first search and the lock and block heuristic to model check the dining philosophers with 30 instances of the Philosopher class. The best parameter may have been omitted in this case, because StEAM uses best-first as the default algorithm when a heuristic is given. You may compare the results of the directed search with these of undirected search (type steam philosophers.ivm 30 or steam -a bfs philosophers.ivm 30).
Rather than searching for a specific kind of error, structural heuristics exploit properties of concurrent systems and the underlying programming language, such as the degree of thread interleaving and the number of global variable accesses. The currently supported structural heuristics are aa, int and rw.
When the option -e or --externalization is given, StEAM keeps the states external on a hard disc, not in RAM. This option should be used in when the model does not fit in RAM any more. To improve speed, you can use RAM cache --state-cache-size <x>, where x represents max. amount of states to be keeped in RAM.
The parameter -l or --lock-global-compaction activates lock-global compaction, which allows thread-switches only after either a global variable was changed or a resource was locked. In experiments, this reduction method has shown to considerably reduce the memory requirements of a model checking run. However, it is yet not formally proven that lock-global-compaction preserves completeness.
By default, StEAM only hashes the cpu-registers of a program state -p part. Other options are:
The option -p full instructs StEAM to hash the entire program state.
Given the option -p inc, the entire state description is hashed in an incremental fashion, which is usually faster than -p full alone. Note, that -p inc implies full hashing.
When option -p bit is given, closed states are not completely stored but mapped to a position in a bit-vector. Bitstate hashing should always be used with full hashing, as this minimizes the chance that StEAM will miss states.
Passing then option --memory-guard activates StEAMs internal memory management. This is helpful to e.g. find memory leaks in the model checker (but not in the checked program).
Given the option -i or --illegal, StEAM will explicitly look for illegal memory accesses (segmentation faults). As this may significantly slow down the exploration, it is not a default option.
The option -s or --simulation tells StEAM to simulate (execute) the program instead exploring its state space.
You can set the maximum amount of memory in megabytes (--memory-limit <mb>), maximum amount of generated states (--state-limit <n>) and the maximum runtime in seconds (--time-limit <s>) required by the model checking run. When one these limits is exceeded, the model checker prints its final statistics and terminates.
When option --source-trail is given, the error trail is printed as actual source lines, rather than as line numbers. StEAM currently uses external Unix-commands to print single lines from source files. As a drawback, the printing of the trail cannot be interrupted using ctrl-c, as this terminates the external program rather than the model checker. This problem should be fixed in future versions.
The option --no-trail suppresses the printing of the error trail - this is useful while doing experiments where the actual trail is of no interest.
In this section, we give a small tutorial, how your own code can be verified with StEAM.
The desire to verify software may in principle arise from two reasons. Either we already have some faulty implementation of a system and want to use model checking to detect the error; or we are just starting with our implementation and want to use model checking to avoid the generation of errors while our software is being developed. In this tutorial, we want to concentrate on the latter case. Using assembly model checking in the implementation phase yields several advantages. On the one hand, it may reduce or even replace the efforts spent on verifying properties of a formal description of the program. Skipping the formal modeling will not only save a considerable amount of development time, also there is no need for the developer to learn the underlying description language (e.g. Promela). Furthermore, assembly model checking is able to find implementation errors which were not present in the software's specification.
The concurrency in StEAM can also be used twofold. Either, the investigated software itself describes a concurrent system. In this case, we define the processes in the software in terms of threads in StEAM. Or, the software itself is not concurrent. In the latter case, we can use threads to simulate the environment of our system.
As an example, lets us assume we want to develop the control software of snack vendor machine. As its basic functionalities, the machine should accept that coins are inserted to raise the credit and buttons are pressed to buy a certain snack.
This code shows the bare bones of the software formed by two minimal functions - insertCoin() and pressButton().
/************************************************
* vendor.c
*
* The bare bones of a snack vendor machine
*
* written by Tilman Mehler
************************************************/
#include "vendor.h"
#include "icvm_verify.h"
#include "Inserter.h"
#include "Presser.h"
#include "Checker.h"
int credit=0;
int coin_values[3] = {10, 50, 100};
int price[3] = {50, 100, 200};
int sold=0;
int got=0;
void main() {
BEGINATOMIC;
(new Inserter())->start();
(new Presser())->start();
(new Checker())->start();
ENDATOMIC;
}
void insertCoin(int amount) {
if(credit+amount<=MAX_CREDIT) {
credit+=amount;
got+=amount;
}
}
void pressButton(int n) {
if(price[n]<=credit) {
credit-=price[n];
sold+=price[n];
}
}
When a coin is being inserted, the credit is raised by the appropriate value. When a button is pressed, the machine first checks if there is sufficient credit to buy the snack. If this is the case, the price of the snack is subtracted from the credit. Two counters - got and sold - keep track of how much money was received and the total value of the snacks sold.
A first property we would like to check is that the total value of sold snacks is always less or equal to the amount of money received, i.e. we want to check for the invariant: (got>=sold). Currently, StEAM supports the detection of deadlocks and local assertions. However, we are also able to check for invariants by introducing an observer thread. The source code of this observer is shown in
This code
/**************************************
*
* Checker.h
*
* Declarations for the Checker-class
**************************************/
#ifndef CHECKER_H
#define CHECKER_H
#include "IVMThread.h"
class Checker:public IVMThread
{
public:
Checker();
virtual void start();
virtual void run();
virtual void die();
};
#endif
/**************************************
*
* Checker.cc
*
* Definitions fot the Checker-class,
* which makes an invariant-check
**************************************/
#include "Checker.h"
#include "icvm_verify.h"
extern int credit;
extern int got;
extern int sold;
Checker::Checker() {}
void Checker::start() {
run();
}
void Checker::run() {
VASSERT(got>=sold);
}
void Checker::die() {}
As can be seen, a thread class in StEAM must be derived from the abstract class IVMThread and must implement the methods start() run() and die(). The start()-method makes preparations for the generated instance and must finally call the run()-method. The call to the run() method tells StEAM to insert the new thread into the running system. The run()-method itself must contain the actual loop of the thread. The die()-method is reserved for future versions of StEAM and currently has no effect - it must be implemented, but currently the body can be left empty. The statement VASSERT(bool e) is used to define local assertions. If the program reaches the control point of the statement and the expression e evaluates to FALSE, StEAM returns the path that leads to this state and reports an error.
Note that we do not have to put our assertion into an infinite loop. We can rely on searching only for those error states, where the observer thread is first executed when the assertion does not hold. Thus, we avoid the generation of equivalent paths to the same error state. Furthermore, we need to simulate the environment of our system - in this case, the users of the machine. One way to achieve this, is to introduce two derived thread classes - one that inserts coins and one that presses buttons. The header and source files for these are shown
here. Both classes use the statement RANGE(varname n, int min, int max), which causes a value between min and max to be non-deterministiclly chosen as the value of the integer variable n.
/**************************************
* Inserter.h
*
* Declaratiins fot the coin-inserter
* Thread-class
**************************************/
#ifndef INSERTER_H
#define INSERTER_H
#include "IVMThread.h"
class Inserter:public IVMThread
{
public:
Inserter();
virtual void start();
virtual void run();
virtual void die();
};
#endif
/**************************************
* Inserter.cc
*
* Definitions fot the coin-inserter
* Thread-class
**************************************/
#include "vendor.h"
#include "Inserter.h"
#include "icvm_verify.h"
extern int coin_values[3];
Inserter::Inserter() {}
void Inserter::start() {
run();
}
void Inserter::run() {
int i=0;
while(1) {
RANGE(i, 0, 3);
insertCoin(coin_values[i]);
}
}
void Inserter::die() {}
Although, in its current form, the source code can already be compiled to an IVM-executable, StEAM will not be able interpret the program correctly. First, the .c and .cc files need to be annotated with additional information. Fortunately, this remains mostly transparent to the user. The StEAM package comes with the tool mfgen. The latter takes as its parameter a set of source files and generates a Makefile which can be used to build the model-checkable file. In the directory where the sources for our vendor machine are located, simply type:
mfgen -f *
followed by
make
This will create the binary file vendor.
Now, start the model checker by typing:
steam -a bfs vendor
After a (hopefully short) time, the model checker will print the error trail and report an assertion violation. Note that we have used breadth-first-search (BFS) to detect the error but the default algorithm is depth-first (DFS). In most cases, DFS find errors faster than BFS, but the BFS is guaranteed to return the shortest trail.
Take some time for interpreting the error trail before you read on ...
It should be obvious, what happened: The button was pressed immediately after the credit was increased, but before the coin value was added to got. We can fix the error by declaring the two variable increases as an atomic block in vendor.c, i.e.:
BEGINATOMIC;
credit+=amount;
got+=amount;
ENDATOMIC;
When you recompile the program (make) - and restart the checker, the error will no longer occur.
The special-purpose statements in StEAM are used to define properties and to guide the search. In general, a special-purpose statements is allowed at any place in the code, where a normal C/C++ statement would be valid. In Section
Verifying your own Programs we already used some of these statements for verifying the vendor machine. Now, we summarize statements, that are currently supported by StEAM.
BEGINATOMIC
ENDATOMIC. A BEGINATOMIC statement within an atomic block has no effect.
ENDATOMIC
This statement marks the end of an atomic region. An ENDATOMIC outside an atomic region has no effect.
RANGE (<varname>, int min, int max)
This statement defines a nondeterministic choice over a discrete range of numeric variable values. The parameter <varname> must denote a variable name that is valid in the current scope. The parameters min and max describe the upper and lower border of the value range. Internally, the presence of a RANGE-statement corresponds to expanding a state to have max-min+1 successors. A RANGE-statement must not appear within an atomic region. Also, the statement currently only works for int variables.
VASSERT (bool e)
This statement defines a local property. When, during program execution, VASSERT(e) is encountered, StEAM checks if the corresponding system state satisfies expression e. If e is violated, the model checker provides the user with the trail leading to the error and terminates.
VLOCK (void * r)
A thread can request exclusive access to a resource by a VLOCK. This statement takes as its parameter a pointer to an arbitrary base type or structure. If the resource is already locked, the thread must interrupt its execution until the lock is released. If a locked resource is requested within an atomic region, the state of the executing thread is reset to the beginning of the region.
VUNLOCK (void * r)
Unlocks a resource making it accessible for other threads. The executing thread must be the holder of the lock. Otherwise this is reported as an access violation, and the error trail is returned.
The model checker StEAM is an attempt to realize software model checking without abstraction and the need to manually construct models in specialized languages, such as Promela. In the current form, the tool is already able to find errors in small programs. The large search space induced by real programs remains the main challenge of software model checking, which may inhibit the finding of an error. Therefore, one of the main issues of future development lies in finding good heuristics. As shown in previous work, an appropriate heuristic is able to find errors fast, even if the underlying search space is huge. In version 0.2 from StEAM a externalisation functionability was added, in order to make larger problems solved, though on a cost of speed.
Also we will improve the memory-efficiency of StEAM by optimizing its state representation. Future versions of StEAM will also support memory-efficient techniques such as bitstate hashing. In the long term our vision is to create a user-friendly application, which facilitates software- development and maintainance without the need for in-depth knowledge about model checking technology.
Main focus of the team is making StEAM accept programs which was compiled with gcc, so it would not have to use igcc any more. A plugin for eclipse environment should make checking with steam easier, and give a posibility to work with graphical interface.
Internet C/C++ Virtual Machine - Internet C++/Internet Virtual Machine is a high-speed, open-source alternative to Java and .NET. Applications written in standard languages, such as C and C++. OpenGL 1.2 support brings portable high-speed 3D graphics and games.
A. Groce and W. Visser
Model Checking Java Programs using Structural Heuristics.
In International Symposium on Software Testing and
Analysis (ISSTA), pages 12-21, 2002.
T. Mehler and P. Leven.
Introduction to StEAM - an assembly-level software model checker.
Technical report, University of Freiburg, 2003.