Paper Info
Title
On the strength of owicki-gries for resources
Abstract
In multithreaded programs data are often separated into lock- protected resources. Properties of those resources are typically verified by modular, Owicki-Gries-like methods. The modularity of the Owicki-Gries method has its price: proving some properties may require manual introduction of auxiliary variables. What properties can be proven without the burden of introducing auxiliary variables? We answer this question in the abstract interpretation framework. On one hand, we reveal a lattice structure of the method and supply a syntax-based abstract transformer that describes 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 the precision loss exactly; in general, the bounds are strict. We prove the absence of a general exact closure-based fixpoint characterization of the accuracy of the Owicki-Gries method, both in the collecting semantics and in certain trace semantics.
Year
DOI
Venue
2011
10.1007/978-3-642-25318-8_15
APLAS
Keywords
Field
DocType
multithreaded programs data,collecting semantics,owicki-gries-like method,owicki-gries method,general exact closure-based fixpoint,auxiliary variable,syntax-based abstract transformer,precision loss,certain trace semantics,abstract interpretation framework
Closure (computer programming),Programming language,Computer science,Abstract interpretation,Lock (computer science),Critical section,Theoretical computer science,Fixed point,Modular design,Semantics,Modularity
Conference
Citations 
PageRank 
References 
2
0.36
12
Authors
2
Name
Order
Citations
PageRank
Alexander Malkis1494.65
Laurent Mauborgne264828.43