FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A lightweight deadlock analysis for programs with threads and reentrant locks

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: