BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:On the Strength of Owicki-Gries for Resources - Alexander Malkis (
 IMDEA)
DTSTART:20111101T130000Z
DTEND:20111101T140000Z
UID:TALK34083@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:In multithreaded programs data are often separated into lock-p
 rotected resources. Properties of those resources are typically verified b
 y modular\, Owicki-Gries-like methods. The modularity of the Owicki-Gries 
 method has its price: proving some properties may require manual introduct
 ion of auxiliary variables. What properties can be proven without the burd
 en of introducing auxiliary variables? We answer this question in the abst
 ract interpretation framework. On one hand\, we reveal a lattice structure
  of the method and supply a syntax-based abstract transformer that describ
 es the method exactly. On the other hand\, we bound the loss of precision 
 from above and below by transition-relation-independent weakly relational 
 closures. On infinitely many programs the closures coincide and describe t
 he precision loss exactly\; in general\, the bounds are strict. We prove t
 he absence of a general exact closure-based fixpoint characterization of t
 he accuracy of the Owicki-Gries method\, both in the collecting semantics 
 and in certain trace semantics. The extracted closures provide general yar
 dsticks for measuring and comparing accuracy of existing and future analys
 es for programs with resources.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR