Author: Cosimo Laneve
Paper Information
Title: | A lightweight deadlock analysis for programs with threads and reentrant locks |
Authors: | Cosimo Laneve |
Proceedings: | FM FMComplete |
Editors: | Jan Peleska, Klaus Havelund and Bill Roscoe |
Keywords: | Object-oriented programs, Deadlock, threads, synchronizations, lams, type system |
Abstract: | ABSTRACT. Deadlock analysis of object-oriented programs that dynamically create threads and objects is complex because these programs may have infinitely many states. We define a simple calculus featuring recursion, threads and synchronizations that guarantee exclusive access to objects. We detect deadlocks by associating an abstract model to programs -- the lam model -- where it is decidable whether a problematic object dependency (e.g.~a circularity) between threads will be ever manifested. The analysis is lightweight because the deadlock detection problem is fully reduced to the corresponding one in lams (without using other models). The technique is intended to be an effective tool for the deadlock analysis of mainstream programming languages by defining ad-hoc extraction processes. |
Pages: | 16 |
Talk: | Jul 17 15:00 (Session 121B) |
Paper: |