Transcript 1.9 - CIS Forge

Extending JML for
Modular Specification and
Verification of
Multi-Threaded Programs
Edwin Rodríguez (KSU)
John Hatcliff (KSU)
Matthew B. Dwyer (UNL)
Gary T. Leavens (ISU)
Cormac Flanagan (UCSC)
Robby (KSU)
Support
US Army Research Office (ARO)
US National Science Foundation (NSF)
US Department of Defense
Advanced Research Projects Agency (DARPA)
Lockheed Martin
The Problem
Hoare-Style Specification
+?
= Specification for Multi-Threaded Code
Approach
Hoare-Style Specification
+ Atomicity
= Specification for Multi-Threaded Code
Contribution: language design
Outline







Overview
Problem in Detail
Atomicity and Independence
Additions to JML
Evaluation
Related Work
Conclusions
Multi-Threading



Available easily in Java, C#, …
Used in most larger systems
Increasingly used in:





Embedded systems
Mission-critical systems
Safety-critical systems
Hard to test and debug
Can’t apply sequential reasoning directly
Two Worlds of Specification and
Verification Tools

Tools for multi-threaded programs



Event ordering, temporal properties
No interference through heap
Tools for sequential programs


Assume serial execution
Invalid for multi-threaded programs
Long Range Goal


Merge these worlds
Create specification language


Work with multiple tools
Useful and practical
Approach: extend JML
Java Modeling Language (JML)

Specifies functional behavior of Java






Interface (names, types)
Pre- and postconditions, invariants, etc.
Many other features
Cooperative, international effort
(see jmlspecs.org)
Wide range of tools
Focused on sequential subset of Java
Problems for
Hoare-style Reasoning


Interference within method bodies
Interference around method calls
Internal Interference
Thread 1
dq.drainTo(c);
Thread 2
requires dq.isEmpty();
dq.add(e);
!dq.isEmpty()
c.add(e);
ensures c.isEmpty();
External Interference
Thread 1
dq = new DelayQueue();
b = dq.isEmpty();
Thread 2
requires true;
return true;
dq.add(e);
ensures \result == true;
!dq.isEmpty()
assert b;
Why Hoare Logic Needs
Non-Interference

Hoare logic:
Pre- and postconditions
//@ assume o != null && mPre;
o.m();
//@ assert mPost;
 No concept of intermediate states


Non-interference:

Atomic region only has
before and after states
Specifying Non-Interference
Needs:
 Locking
 Data confinement
 Serializability
Ignore:
 Extra-program control (e.g., scheduling)
Needs:
Specifying Locking
Allow specification of:
 Locks a method acquires & releases
 Locks that protect part of an object
 That an objects is a lock
 Set of locks held by a thread
 When an object is lock protected
Needs:
Specifying Data Confinement
Allow specification of:
 Aliasing and ownership patterns
 Thread locality of objects
 Frame axioms
Needs:
Specifying Serializability
Specify when a method is:
 Atomic
 Independent
Background for Approach:
Lipton’s (1975) Reduction Theory




Transitions ≈ Java bytecodes
Commuting: can be reordered with
transition of other threads
Transition α is a right mover if,
for all transitions of other threads, β,
α,β leads to same state as β,α
E.g., lock acquire,
read or write protected by lock
Right Movers
s1
s1
acq
E1
s2
s2’
t=x
acq
s3
s3
E1
t=x
s4
s4
Left Movers, Both Movers
E2
s4
s4
x = t+1
s5
s5’
x = t+1
rel
s6
s6’
E3
E2
s7
s7’
rel
E3
Actions protected by locks are both movers.
s8
s8
Atomic Region

Has form
R* N? L*
where
R = right mover
N = neither left nor right mover
L = left mover

Example:
acq; t=x; x=t+1; rel
R
R
L
L
Independence


A both mover is independent.
Independent region has form
I*
where
I is independent

Independent regions are:


Atomic, and
Composable
Outline







Overview
Problem in Detail
Atomicity and Independence
Additions to JML
Evaluation
Related Work
Conclusions
Locking Notations
Already in JML
monitors_for id <- lock1, …, lockn ;
 Type-level declaration
 Meaning: to access id thread must lock
each non-null lock in lock1, …, lockn .
\lockset()
 Expression
 Meaning: locks held by current thread.
Heap Restriction Notations
Already in JML (Universes)
rep
 Type modifier
 Meaning: object referenced is a
wholly-owned part of the representation;
no external references.
readonly
 Type modifier
 Meaning: cannot change object through
the reference
DelayQueue Example (1)
package java.util.concurrent;
import java.util.concurrent.locks.*; /*… */
public class DelayQueue<E extends Delayed>
/* … */
{
private /*@ spec_public rep @*/
transient final ReentrantLock lock
= new ReentrantLock();
private /*@ spec_public rep @*/ final
PriorityQueue<E> q = new PriorityQueue<E>();
//@ monitors_for q <- lock;
Additions to JML:
Locks Clause
locks lock1, …, lockn ;
 Method specification clause
 Meaning: may only lock the given locks.
 Default: this, if method is synchronized
Additions to JML:
Specifying Atomicity
atomic
 Method modifier
 Meaning: when precondition is met,
implementation must be serializable.
DelayQueue Example (2)
/*@ requires o != null;
@ locks lock;
@ ensures this.q.contains(o);
@*/
public /*@ atomic @*/
boolean offer(E o) {
lock.lock();
try { E first = q.peek(); /* … */ }
finally { lock.unlock(); }
}
Additions to JML:
Predicates for Thread Safety
\lock_protected(o)
 Meaning: o is protected by locks,
all of them held by current thread.
\thread_local(o)
 Meaning: o is owned by current thread.
\thread_safe(o) <==>
\lock_protected(o) || \thread_local(o).
DelayQueue Example (3)
/*@ requires \thread_safe(c)
@
&& c != null && c != this;
@ locks lock;
@ ensures (\forall int i;
@
1 <= i && i <= q.size;
@
c.contains(q.queue[i]));
@*/
public /*@ atomic @*/ int
drainTo(Collection<? super E> c);
Additions to JML:
Predicate for Independence
\independent
 Predicate in method postconditions
 Meaning: the method’s execution was
independent.
DelayQueue Example (4)
/*@ ensures \independent
@ && \result == Integer.MAX_VALUE;
@*/
public /*@ atomic @*/
int remainingCapacity() {
return Integer.MAX_VALUE;
}
Locks clause and \independent
locks lock1, lock2;
means
ensures \old(\lockset().has(lock1)
&& \lockset().has(lock2))
==> \independent;
So drainTo and offer are independent,
if thread holds lock.
Blocking Behavior and
Commit Atomicity
when predicate;
 Method specification clause
 Meaning: method blocks until predicate.
 Checking:
at statement labeled commit,
the predicate must hold
(Freund & Qadeer, 2004).
ArrayBlockingQueue Example (1)
package java.util.concurrent;
import java.util.concurrent.locks.*;
import java.util.*;
public class ArrayBlockingQueue<E>
/* … */
{
private /*@ spec_public rep @*/ final
ReentrantLock lock;
ArrayBlockingQueue Example (2)
private /*@ spec_public non_null rep @*/
final E[] items;
private /*@ spec_public @*/ transient int takeIndex;
private /*@ spec_public @*/ transient int putIndex;
private /*@ spec_public @*/ int count;
/*@ private invariant
@
0 <= takeIndex && takeIndex < items.length
@ && 0 <= putIndex && putIndex < items.length
@ && count == (putIndex - takeIndex)
@
% items.length;
@*/
ArrayBlockingQueue Example (3)
take() Specification
/*@ locks this.lock;
@ when count != 0;
@ assignable items[takeIndex],
@
takeIndex, count;
@ ensures \result
@
== \old(items[takeIndex])
@ && takeIndex == \old(takeIndex) + 1
@ && count == \old(count) -1;
@*/
public /*@ atomic @*/ E take()
throws InterruptedException
ArrayBlockingQueue Example (3)
take() Implementation
{ lock.lockInterruptibly();
try {
try {
while (count == 0) { notEmpty.await(); }
} catch (InterruptedException ie) {
notEmpty.signal(); throw ie;
}
/*@ commit: @*/ E x = extract();
return x;
} finally { lock.unlock(); }
}
Additions to JML:
Notations for Lock Types


JML considers subtypes of
java.util.concurrent.locks.Lock
to be lock types.
Objects of type Lock are lock objects.
locked_if predicate;
 Clause in body of classes and interfaces
 Meaning: object locked when predicate.
Reentrant Lock Example
package java.util.concurrent;
import java.util.concurrent.locks.Lock;
public class ReentrantLock
implements Lock, java.io.Serializable {
//@ locked_if isLocked();
/* ... */
}
Specification Case Studies




Bounded Buffer, Dining Philosophers
from Hartley (1998)
LinkedQueue, Readers-Writers
from Lea (2000)
java.util.Vector
Eight classes from java.util.concurrent
Statistics from
Specification Case Studies
200
methods
150
100
50
0
total
atomic
\indep.
locks
\thread
when
Verification Case Study

Bogor (Robby, et al., 2003)




Extensible model checking framework
JML functional spec. checking (2004)
Atomicity checking (2004)
Integration of JML functionality
and atomicity checking is new.


Postcondition and frame checking
only if method execution was serial.
Report atomic methods that aren’t serial.
Methods Samples for
Verification Case Study

Used subset of classes from
specification case study




BoundedBuffer, Dining Philosophers
LinkedQueue, Readers and Writers
CopyOnWriteArrayList,
LinkedBlockingQueue
Strong specifications

Heap properties, frames, freshness,
reachability, values of memory locations
Statistics from Verification
Case Study with Bogor
50
methods
40
30
20
10
0
total
checkable
checkable
atomicity
functionality
Verification Case Study

Can’t verify atomicity for
22 out of 42 methods

11 commit atomicity.


Could be checked (Flanagan 2004).
Rest challenging.

“Normal” code not so hard?
Related Work
Jacobs, Leino, Schulte (2004)
 Spec# similar to JML overall.
 New acquire and release statements.
 Acquire gets exclusive access.
 Proof of soundness.
 But limited to programs written to
follow discipline.
Related Work




Ábrahám, et al., 2002
Proof system for multi-threaded Java.
Whole-program Owicki-Gries style
annotations, so not modular.
Only deals with monitor synchronization
Future Work



Working out details (e.g., pure methods)
Formalization of the extensions.
Implementation in other JML tools.





Parsing and type checking support.
Runtime assertion checking as in Atomizer
JMLEclipse support
ESC/Java2
Other extensions

Synchronization patterns (temporal logic)
Conclusions

Extended JML to support:




Supports modular reasoning about:



Locking
Data confinement
Serializability
Functionality (data) and
Concurrency
Validated by cases studies