Abstract:
We present an algorithm to detect deadlocks in concurrent message-passing programs. Even though deadlock is inherently noncompositional and its absence is not preserved b...Show MoreMetadata
Abstract:
We present an algorithm to detect deadlocks in concurrent message-passing programs. Even though deadlock is inherently noncompositional and its absence is not preserved by standard abstractions, our framework employs both abstraction and compositional reasoning to alleviate the state space explosion problem. We iteratively construct increasingly more precise abstractions on the basis of spurious counterexamples to either detect a deadlock or prove that no deadlock exists. Our approach is inspired by the counterexample-guided abstraction refinement paradigm. However, our notion of abstraction as well as our schemes for verification and abstraction refinement differs in key respects from existing abstraction refinement frameworks. Our algorithm is also compositional in that abstraction, counterexample validation, and refinement are all carried out component-wise and do not require the construction of the complete state space of the concrete system under consideration. Finally, our approach is completely automated and provides diagnostic feedback in case a deadlock is detected. We have implemented our technique in the MAGIC verification tool and present encouraging results (up to 20 times speed-up in time and 4 times less memory consumption) with concurrent message-passing C programs. We also report a bug in the real-time operating system MicroC/OS version 2.70.
Published in: Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE '04.
Date of Conference: 23-25 June 2004
Date Added to IEEE Xplore: 05 July 2005
Print ISBN:0-7803-8509-8