Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs

• Published in: Formal methods in system design 2004-09, Vol.25 (2/3), p.199-240
• Main Authors: Dwyer, Matthew B., Hatcliff, John, Ranganath, Venkatesh Prasad
• Format: Article
• Language: English
• ISSN: 0925-9856
• DOI: 10.1023/B:FORM.0000040028.49845.67

Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of system states explored (and thus the time and memory required) for verification. As model checking techniques are scaled up to software systems, it is important to develop and assess partial-order reduction strategies that are effective for addressing the complex structures found in software and for reducing the tremendous cost of model checking software systems. In this paper, we consider a number of reduction strategies for model checking concurrent object-oriented software. We investigate a range of techniques that have been proposed in the literature, improve on those in several ways, and develop five novel reduction techniques that advance the state of the art in partial-order reduction for concurrent object-oriented systems. These reduction strategies are based on (a) detecting heap objects that are thread-local (i.e., can be accessed by a single thread) and (b) exploiting information about patterns of lockacquisition and release in a program (building on previous work). We present empirical results that demonstrate upwards of a hundred fold reduction in both space and time overexisting approaches to model checking concurrent Java programs. In addition to validating their effectiveness, we prove that the reductions preserve LTL_X properties and describe an implementation architecture that allows them to be easily incorporated into existing explicit-state software model checkers.