University of Cambridge > > Computer Laboratory Automated Reasoning Group Lunches > On the Strength of Owicki-Gries for Resources

On the Strength of Owicki-Gries for Resources

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact William Denman.

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. The extracted closures provide general yardsticks for measuring and comparing accuracy of existing and future analyses for programs with resources.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity