On the Strength of Owicki-Gries for Resources

Alexander Malkis and Laurent Mauborgne.
On the Strength of Owicki-Gries for Resources.
In Honqseok Yang, editor, Asian Symposium on Programming Languages and Systems (APLAS 2011), volume 7078 of Lecture Notes in Computer Science, pages 172--187.
Springer-Verlag, 2011.
download.
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. The extracted closures provide general yardsticks for measuring and comparing accuracy of existing and future analyses for programs with resources.

\bibitem{malkis:mauborgn11}
Alexander Malkis and Laurent Mauborgne.
\newblock On the strength of owicki-gries for resources.
\newblock In Honqseok Yang, editor, {\em 9th Asian Symposium on Programming
  Languages and Systems (APLAS 2011)}, volume 7078 of {\em Lecture Notes in
  Computer Science}, pages 172--187. Springer-Verlag, 2011.

@inproceedings{malkis:mauborgn11,
author = "Alexander Malkis and Laurent Mauborgne",
title = "On the Strength of Owicki-Gries for Resources",
booktitle = "9th Asian Symposium on Programming Languages and Systems (APLAS 2011)",
volume = 7078,
pages = "172--187",
editor = "Honqseok Yang",
series = "Lecture Notes in Computer Science",
year = 2011,
publisher = "Springer-Verlag",
}

Email: Laurent.Mauborgne@imdea.org