Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

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

Matthew B. DwyerContact Information, John HatcliffContact Information, RobbyContact Information and Venkatesh Prasad RanganathContact Information

(1) Department of Computing and Information Sciences, Kansas State University, 234 Nichols Hall, Manhattan, KS 66506, USA

Abstract  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 lock-acquisition 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 over existing 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.

software model checking - software verifcation - partial order reduction - escape analysis - locking discipline


Contact InformationMatthew B. Dwyer
Email: dwyer@cis.ksu.edu

Contact InformationJohn Hatcliff
Email: hatcliff@cis.ksu.edu

Contact InformationRobby
Email: robby@cis.ksu.edu

Contact InformationVenkatesh Prasad Ranganath
Email: rvprasad@cis.ksu.edu
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this article
Export this article as RIS | Text
 
Remote Address: 38.107.191.115 • Server: MPWEB36
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)