Transcript Bandera Overview: ICSE00 talk

A Demonstration of Basic Aspects of the
Bandera Tool Set
SAnToS Laboratory, Kansas State University, USA
Faculty
Students and Post-docs
Matthew Dwyer
John Hatcliff
Radu Iosif
Hongjun Zheng
Shawn Laubach
Corina Pasareanu
Robby
Roby Joehanes
Venkatesh Ranganath
Oksana Tkachuk
http://www.cis.ksu.edu/santos/bandera
Notes

Demo examples are chosen to be simple and
to illustrate tool components
 For more examples with interesting
specifications, see…
– Bandera tutorial…
– STTT paper
• complete presentation of BoundedBuffer example
• Doug Lea’s Readers/Writers
• Publish/Subscribe framework from java.util
Outline

Concept of a session
– configuring Bandera for a run

Simple deadlock example
– illustrates session, code display,
counterexample navigation, and slicing

Pipeline example
– illustrates creating a temporal specification,
slicing, and abstraction
Configuring Bandera
A run of Bandera is configured by a session specification

A session specifies...
– which Java files to take as input
– which property to check
– which tool components (e.g., slicer, abstraction) to
invoke
– which backend model-checker to use
– …other options

A session file holds several related sessions
– sessions in session file can be executed in batch
mode or individually selected in the BUI.
Simple Deadlock Example
Process 1
Process 2
acquisition
acquisition
Lock 1
Lock 2
blocked
acquisition
blocked
acquisition
Simple Deadlock Example
public class Deadlock {
static Lock lock1;
static Lock lock2;
static int state;
public static
void main(String[] args) {
lock1 = new Lock();
lock2 = new Lock();
Process1 p1
= new Process1();
Process2 p2
= new Process2();
p1.start();
p2.start();
}
class Lock {}
class Process1 extends Thread {
public void run() {
Deadlock.state++;
synchronized (Deadlock.lock1) {
synchronized (Deadlock.lock2) {
Deadlock.state++;
}}}}
class Process2 extends Thread {
public void run() {
Deadlock.state++;
synchronized (Deadlock.lock2) {
synchronized (Deadlock.lock1) {
Deadlock.state++;
}}}}
Deadlock Example Artifacts
Point.basl
Property Tool
Point.java
Abstracted Java
Abstraction
Analyses Engine
BIRC
Translators
BIR
SPIN
.trail
dSPIN
Java
Jimple
Parser
SMV
Slicer
Error Trace Display
Sliced Java
Simulator
JPF
Simple Deadlock Example
/**
* @observable
*
LOCATION[p1startlabel] p1start();
*/
public static void main(String[] args) {
lock1 = new Lock();
lock2 = new Lock();
Process1 p1 = new Process1();
Process2 p2 = new Process2();
p1startlabel:
p1.start();
p2.start();
}
Bandera predicate (used
as proposition in temporal
logic specification)
Simple Deadlock Example
Bandera predicate (used
as proposition in temporal
logic specification)
/**
* @observable
*
EXP x1isTwo(this): (x1 == 2);
*/
class Process1 extends Thread {
Integer variables that
int x1, y1;
interact with
public void run() {
Deadlock.state
DeadlockAbs.state++;
synchronized (DeadlockAbs.lock1) {
synchronized (DeadlockAbs.lock2) {
x1 = DeadlockAbs.state++;
y1 = DeadlockAbs.state++ + x1;
}
}
}
}
Tool Status

Available for download with user manual,
example repository, BIR backend developers
guide
 Major additions over next 3 months to allow
treatment of almost all of Java
– minor releases throughout fall

Complete rewrite of code-base is underway
and new version will be incorporated into
IBM’s Eclipse open source IDE.
– target for release: March 2003