[pl-seminar] Last talk of the year

[Steve Jackson <sjackso@xxxxxxxxxxx>]

Nick Kidd will be giving a VMCAI practice talk on Thursday, 18  
December.  It will be held at 4 PM in 3310 CS.  Details below.
Title: Finding Concurrency-Related Bugs using Random Isolation


Abstract:
A recent bug survey of Apache and Firefox by Lu et al. showed that one  
third of
all non-deadlock concurrency bugs involved more than one shared memory  
location.
In this talk, I will present the methods used in Empire, a tool to  
detect
concurrency-related bugs, namely atomic-set serializability violations  
in Java
programs. The correctness criterion is based on atomic sets of memory  
locations,
which share a consistency property, and units of work, which preserve
consistency when executed sequentially.  Empire checks that, for each  
atomic
set, its units of work are serializable. This notion subsumes data races
(single-location atomic sets), serializability (all locations in one  
atomic
set), and is one of the first tools to be able to statically detect
multi-location consistency errors.


To obtain a sound, finite model of locking behavior for use in Empire,  
we
devised a new abstraction principle, random isolation, which allows  
strong
updates to be performed on the abstract counterpart of each randomly- 
isolated
object. This permits Empire to track the status of a Java lock, even for
programs that use an unbounded number of locks. The advantage of random
isolation is that properties proved about a randomly-isolated object  
can be
generalized to all objects allocated at the same site.

This is joint work with Prof. Reps, and Mandanva Vaziri and Julian  
Dolby from
IBM Research.

The is a practice talk for VMCAI 2009.