Previous article

Next article

---

A Static Analysis to Detect Re-Entrancy in Object Oriented Programs Manuel Fähndrich, Diego Garbervetsky, and Wolfram Schulte

REFEREED ARTICLE PDF Version

Abstract

We are interested in object-oriented programming methodologies that enable static verification of object-invariants. Reasoning soundly and effectively about the consistency of objects is still one of the main stumbling blocks to pushing object-oriented program verification into the mainstream. More precisely, any sound methodology must be able to guarantee that the invariant of the receiver object holds at all method call sites. Establishing this proof obligation is tedious, and instead programmers would like to reason informally as follows: methods should be able to assume that the object invariant holds on entry, as long as all constructors establish it, and all methods guarantee that the receiver invariant holds on exit.

This reasoning is only correct under certain conditions. In this paper we present sufficient conditions that make reasoning as above sound and show how these conditions can be checked separately, allowing us to divide the verification problem into two well-defined parts: 1) reasoning about object consistency of the receiver within a single method, and 2) reasoning about the absence of inconsistent re-entrant calls. In particular, when reasoning about the object consistency of the receiver within a method, our approach does not require proving invariants on other objects whose methods are called.

We present a novel whole program analysis to determine the absence of inconsistent re-entrant calls. It warns developers when re-entrant calls are made on objects whose invariants may not hold. The analysis augments a points-to analysis to compute potential call chains in order to detect re-entrant calls.

Note: Due to the typographical sophistication of this article, no HTML version is available. Please use the PDF version.

About the authors

		Manuel Fähndrich is a senior researcher at Microsoft, Redmond, where he pursues his interests in program analysis, static verification, and programming language design. Prior to that, Manuel received his Ph.D. in Computer Science from the University of California at Berkeley. He can be reached at maf@microsoft.com.
		Diego Garbervetsky Ph.D. in Computer Science and full-time Associate Professor in the CS. Department of University of Buenos Aires (Argentina). His research field is Embedded Systems, Formal Verification and Program Analysis focused on prediction of dynamic memory utilization. He can be reached at diegog@dc.uba.ar.
		Wolfram Schulte Since 2006Wolfram Schulte has been a research area manager at Microsoft Research in Redmond, Washington, USA. Wolfram’s research concerns the practical application of formal techniques in programming language design and implementation, in static and dynamic verification. Before joining Microsoft Research in 1999, Wolfram worked at the University of Ulm (1993-1999), at sd&m, a German software company (1992-1993), and at the Technical University Berlin (1987-1992). He can be reached at schulte@microsoft.com.