Deadlock checking by data race detection

2Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.

Abstract

Deadlocks are a common problem in programs with lock-based concurrency and are hard to avoid or even to detect. One way for deadlock prevention is to statically analyse the program code to spot sources of potential deadlocks. We reduce the problem of deadlock checking to data race checking, another prominent concurrency-related error for which good (static) checking tools exist. The transformation uses a type and effect-based static analysis, which analyses the data flow in connection with lock handling to find out control-points which are potentially part of a deadlock. These control-points are instrumented appropriately with additional shared variables, i.e., race variables injected for the purpose of the race analysis. To avoid overly many false positives for deadlock cycles of length longer than two, the instrumentation is refined by adding "gate locks". The type and effect system, and the transformation are formally given. We prove our analysis sound using a simple, concurrent calculus with re-entrant locks.

Cite

CITATION STYLE

APA

Pun, K. I., Steffen, M., & Stolz, V. (2014). Deadlock checking by data race detection. Journal of Logical and Algebraic Methods in Programming, 83(5–6), 400–426. https://doi.org/10.1016/j.jlamp.2014.07.003

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free