Transcript power point presentation - UCSB Computer Science

Developing Verifiable Concurrent
Software
Tevfik Bultan
Department of Computer Science
University of California, Santa Barbara
[email protected]
http://www.cs.ucsb.edu/~bultan
Joint Work with My Students
• Design for verification
– Aysu Betin-Can (PhD 2005)
• Verification of Service Interactions
– Xiang Fu (PhD 2004)
• Action Language Verifier
– Tuba Yavuz-Kahveci (PhD 2004)
– Constantinos Bartzis (PhD 2004)
• Interface Grammars
– Graham Hughes (PhD candidate)
Verification Tools, Concurrency Problems
Action
Language
Verifier
Synchronizability
Analysis
enables
uses
Verification of
Synchronization in
Concurrent
Programs
Design for
Verification
enables
uses
Analyzing
Web Service
Interactions
Read-Write Lock in Action Language
S : Cartesian product of
variable domains defines
the set of states
module main()
integer nr;
boolean busy;
restrict: nr>=0;
initial: nr=0 and !busy;
I : Predicates defining
the initial states
module ReaderWriter()
enumerated state {idle, reading, writing};
initial: state=idle;
R : Atomic actions of
a single process
r_enter: state=idle and !busy and nr’=nr+1 and state’=reading;
r_exit:
state=reading and nr’=nr-1 and state’=idle;
w_enter: state=idle and !busy and nr=0 busy’ and state’=writing;
w_exit:
state=writing and !busy’ and state’=idle;
R : Transition relation of a
ReaderWriter: r_enter | r_exit | w_enter | w_exit;
process, defined as
endmodule
asynchronous
main: ReaderWriter() | ReaderWriter() | ReaderWriter();
composition of its
atomic actions
spec: invariant(busy => nr=0)
spec: invariant(busy => eventually(!busy))
endmodule
R : Transition relation of main, defined as asynchronous
composition of three processes
A Java Read-Write Lock Implementation
Where are the guarded
commands?
How do we translate
this to Action Language?
class ReadWriteLock {
private Object lockObj;
private int totalReadLocksGiven;
private boolean writeLockIssued;
private int threadsWaitingForWriteLock;
public ReadWriteLock() {
lockObj = new Object();
writeLockIssued = false;
}
public void getReadLock() {
synchronized (lockObj) {
while ((writeLockIssued) || (threadsWaitingForWriteLock != 0)) {
try {
lockObj.wait();
} catch (InterruptedException e) {
}
}
totalReadLocksGiven++;
}
}
public void getWriteLock() {
synchronized (lockObj) {
threadsWaitingForWriteLock++;
Action
Language
Verifier
while ((totalReadLocksGiven != 0) || (writeLockIssued)) {
try {
lockObj.wait();
} catch (InterruptedException e) {
//
}
}
threadsWaitingForWriteLock--;
writeLockIssued = true;
}
}
public void done() {
synchronized (lockObj) {
Verification of
Synchronization in
Java
Programs
//check for errors
if ((totalReadLocksGiven == 0) && (!writeLockIssued)) {
Design for Verification
• Abstraction and modularity are key both for successful designs and
scalable verification techniques
• The question is:
– How can modularity and abstraction at the design level be better
integrated with the verification techniques which depend on these
principles?
• Our approach:
– Structure software in ways that facilitate verification
– Document the design decisions that can be useful for verification
– Improve the applicability and scalability of verification using this
information
A Design for Verification Approach
We have been investigating a design for verification approach based on
the following principles:
1. Use of design patterns that facilitate automated verification
2. Use of stateful, behavioral interfaces which isolate the behavior and
enable modular verification
3. An assume-guarantee style modular verification strategy that
separates verification of the behavior from the verification of the
conformance to the interface specifications
4. A general model checking technique for interface verification
5. Domain specific and specialized verification techniques for behavior
verification
• Avoids usage of error-prone Java synchronization primitives:
synchronize, wait, notify
• Separates controller behavior from the threads that use the controller:
Supports a modular verification approach which exploits this modularity
for scalable verification
Modular Design / Modular Verification
Thread Modular Interface Verification
Thread 1
Thread 2
Thread n
Thread n
Thread 2
Thread 1
Concurrent Program
Interface
Machine
Interface
Machine
Interface
Machine
Interface
Controller
Shared
Data
Controller Behavior
Modular
Behavior
Verification
Verification Framework
Controller
Behavior
Machine
Controller
Classes
Behavior
Verification
Action
Language
Verifier
Counting
Abstraction
Concurrent
Program
Controller
Interface
Machine
Thread
Thread
Thread
Classes
Interface
Verification
Java
Path Finder
Thread
Isolation
Thread
Class
Outline
Action
Language
Verifier
Synchronizability
Analysis
enables
uses
Verification of
Synchronization in
Concurrent
Programs
Design for
Verification
enables
uses
Analyzing
Web Service
Interactions
Web Services
Interaction
WSCDL
Composition
WSBPEL
Service
WSDL
Message
SOAP
Type
XML Schema
Data
XML
Web Service Standards
Implementation Platforms
Loosely coupled, interaction through standardized interfaces
Standardized data transmission via XML
Asynchronous messaging
Platform independent (.NET, J2EE)
Microsoft .Net, Sun J2EE
•
•
•
•
A Model for Composite Web Services
• A composite web service consists of
– a finite set of peers and a finite set of messages
• We assume that the messages among the peers are exchanged using
reliable and asynchronous messaging
– FIFO and unbounded message queues
• A conversation is the global sequence of messages exchanged
among the peers participating to a composite service
• Model checking problem: Given an LTL property, does the
conversation set satisfy the property?
Synchronizability Analysis
• We know that analyzing conversations of composite web services is
difficult due to asynchronous communication
– Can we identify the composite web services where asynchronous
communication does not create a problem?
• A composite web service is synchronizable, if its conversation set does
not change when asynchronous communication is replaced with
synchronous communication
• If a composite web service is synchronizable we can check properties
about its conversations using synchronous communication semantics
• We built a tool called Web Service Analysis Tool (WSAT), which checks
sufficient conditions for synchronizability
– Requires each peer participating to the composite service to be
specified as a state machine
Checking Service Implementations
• Web service implementations are
written using programming languages
such as Java, C#, etc.
Synchronizability
Analysis
• Synchronizability analysis works on
state machine models
• How do we generate the state machines
from the Java code?
Checking
Service
Implementations
Design for Verification Approach
Use the same principles:
1. Use of design patterns that facilitate automated verification
2. Use of stateful, behavioral interfaces which isolate the behavior and
enable modular verification
3. An assume-guarantee style modular verification strategy that
separates verification of the behavior from the verification of the
conformance to the interface specifications
4. A general model checking technique for interface verification
5. Domain specific and specialized verification techniques for behavior
verification
Modular Design / Modular Verification
Peer Modular Interface Verification
Peer 1
Peer 2
Peer n
Peer n
interface
Peer 2
interface
interface
Peer 1
Composite Service
Interface
Machine
Interface
Machine
Interface
Machine
Conversation Behavior
Modular
Conversation
Verification
Verification Framework
Thread
Peer
Thread
WSAT
State
Machines
Promela
Translation
Synchronizability
Analysis
Composite
Service
Peer
State
Machine
Conversation
Verification
Interface
Verification
Spin
Java
Path Finder
Peer
Code
Promela
Conclusions
• Once the behavior is isolated (using concurrency controller or peer
controller patterns) behavior verification was quite efficient
– Use of domain specific behavior verification techniques has been
very effective
– Model checking research resulted in numerous verification
techniques and tools which can be customized for specific classes
of software systems
• Interface verification (which is less specialized) was very hard
– It is necessary to find effective behavioral interface specification
and verification techniques
– Check out our recent work on interface grammars!
Conclusions
• We were able to use our design for verification approach based on
design patterns and behavioral interfaces in different domains
• Automated verification techniques can scale to realistic software
systems using a design for verification approach
THE END