Verification of Concurrent and
Reactive Systems
Systems composed of elements (threads/processes) that
can operate concurrently and communicate with each other
1. Each component can be viewed as a reactive system,
i.e., a system that continuously interacts with its environment. (telephone switch, disk control system, etc.)
2. State machines in objects may be implemented as
parallel programs, and many of the ways in which these parallel components
interleave their operations are not obvious to the programmer
3. Traditional software testing techniques are of limited
help because test coverage is bound to be a minute fraction of the total number
of possible behaviors; furthermore, scenarios leading to errors may be very
difficult (or impossible) to reproduce
4. In parallel programming, the hardest bug is one that
is not reproducible and treating a concurrent program as a “black box” is
almost useless because the (correct) external behavior may be different on each
test
5. Because of nondeterministic scheduling (from lower
level schedulers) many different (correct) orderings of external behavior may
result
6. We need a tool to model the interaction of concurrent
components and verify their correct behavior by exploring all possible states
of interleaving of threads (tasks, processes, etc.)
7. Must build test harness that is closed to the
environment (otherwise, the number of states may be infinite)
8. Some current systems
a. Promela/Spin Model-checker (well-established)
b. Java Pathfinder (JPF)
c. Verisoft (not supported)
d. Zing for C# (from Microsoft Resarch)
Typical
Parallel Program Environment
Modeling Decisions
1. Why build a model?
a. Design a new system (construct a model)
b. Reverse Engineering (extract a model)
2. Technical Challenges in Model Verification
a. formulation of specifications
b. state explosion
c. model construction
3. Number of States vs. "real code"
a. sizes (buffers, arrays, etc.)
b. number of threads
c. loops
d. atomic step (once validated)
e. "closed environment"
4. Important Properties
a. ordering of events/values
b. proper initiation
c. proper synchronization (safety)
d. proper termination
e. proper content
f. proper response
Promela/Spin Modeling
Gerard Holzman-Bell
Labs
http://cm.bell-labs.com/cm/cs/what/spin/Man/promela.html
1. C-like language
a. Active processes to model real-world processes
b. Channels to synchronize processes (nice model for
ports)
c. Assertions to specify conditions that must hold at a
particular statement
d. Condition-scheduling to easily specify process
continuation
e. Atomic sequences for safety and state reduction
2. Automatic exhaustive state-space exploration
a. Trace-back from error states for manual (graphical)
playback
b. Checks assertions, detects deadlocks, and validates
temporal logic specifications
3. Used successfully in a wide variety of real-world
applications from telephone switches to hardware circuits to space exploration
vehicles
4. Concerns: size of model and state-space explosion
5. Advantages
a. Validating complex parallel programs automatically
b. Successfully used in wide variety of applications
6. Disadvantages
a. Must recode model into real implementation language
7. Example – Sojourner
8. Tools
a. Spin
b. ispin
/*NASA's Pathfinder landed on Mars releasing a small rover named */
/*Sojourner to roam the surface. A software design fault caused */
/*the craft to lose contact with earth at unpredictable moments. */
/*The flaw was a conflict between a mutual exclusion rule and a */
/* priority rule used in the real-time task scheduling algorithm:*/
/* a priority inversion. If the designers of the parallel real- */
/*time program had modeled the design with the following abstract*/
/* model in Promela, they would have solved the problem before */
/* writing the code. */
/* This code is from Gerard Holzmann's paper entitled */
/*"Designing Executable Abstractions" */
mtype = {free, busy, idle, waiting, running};
show mtype h_state = idle;
show mtype l_state = idle;
show mtype mutex = free;
active proctype high_priority()
{
end: do
::h_state = waiting;
atomic{mutex == free -> mutex = busy};
h_state = running;
/*produce data*/
atomic{h_state = idle;
mutex = free}
od
}
active proctype low priority()
provided(h_state == idle)
{
end: do
::l_state = waiting;
atomic{mutex== free -> mutex = free};
l_state = running;
/* consumer data */
atomic{l_state = idle;
mutex = free}
od
}
Java PathFinder
Klaus Havelund-NASA
http://ic-www.arc.nasa.gov/ic/projects/amphion/docs/vandy.html
1. Programs as Models
a. Build architecture of concurrent Java program with
threads, objects, etc.
b. Insert assertions which are automatically checked
during execution
2. Compiled into special JVM for model-check
3. Concerns - size of model and state-space search
4. Advantages
a. Model-check the architecture of the reactive program
b. "atomic" statement to reduce state-space
explosion
c. Just remove assertions and fill-in specific details
d. Solid understanding of the underlying parallel model
5. Disadvantages
a. Large state space
b. Need to iteratively test different sections of the
model
6. Example: Deadlock
VeriSoft
Patrice Godefroid-Bell
Labs
http://www.bell-labs.com/project/verisoft
1. A tool for systematically exploring the state space of
systems composed of several concurrent processes executing arbitrary C code
2. State space is a directed graph that represents the
combined behavior of all the components of the system (recorded only at VeriSoft synchronization points)
3. Semaphores and message exchange
4. When an error is detected during state-space
exploration, a scenario leading to the error state is saved in a file for later
manual playback
a. Assertion violation, deadlock, livelock,
and divergences detected
5. Supports special operations to simulate nondeterminism
a. VS_Toss(random)
6. Verisoft has been successfully applied to testing, debugging,
and reverse-engineering of telephone switches
7. Need to build test harness which enables VeriSoft to explore all states which result from the test
harness
8. Automatically generate, execute and evaluate thousands
of tests per minute, with complete control over nondeterminism,
thus quickly revealing behaviors which are virtually impossible to detect using
conventional testing techniques
9. Concerns
a. Not used very often
10.
Advantages
a. Real C Code
b. Reduced state space because assertions only checked at
visible operations
11.
Disadvantages
a. Must provide Unix processes in operational environment
b. Threads are still unimplemented
c. Only model-checked at synchronization points
d. Cannot use temporal logics
12.
Example: Dining
Philosophers
#include <verisoft.h>
/****************************************************************************
* phil.c : dining philosophers with 1 deadlock *
****************************************************************************/
#include <stdio.h>
#include <sys/types.h>
#include <sys/ipc.h>
#include <sys/sem.h>
#define N 5
philosopher(i,semid)
int i, semid;
{
while (1)
{
printf("philosopher %d thinks\n",i);
semwait(semid,i,1);
semwait(semid,((i+1)%N),1);
printf("philosopher
%d eats\n",i);
semsignal(semid,i,1);
semsignal(semid,((i+1)%N),1);
}
}
main()
{
int semid, i, pid, status;
semid = semget(IPC_PRIVATE,N,0600);
for(i=0;i<N;i++)
semsetval(semid,i,1);
for(i=0;i<(N-1);i++)
{
if((pid=fork()) == 0)
{
philosopher(i,semid);
}
};
philosopher(i,semid);
}