Deadlock Checking by a Behavioral Effect System for Lock Handling
|Title||Deadlock Checking by a Behavioral Effect System for Lock Handling|
|Publication Type||Journal Article|
|Year of Publication||2012|
|Authors||K. I. Pun, M. Steffen, and V. Stolz|
|Journal||Journal of Logic and Algebraic Programming|
|Keywords||Abstraction, Behavioral type and effect systems, Concurrency, Deadlock prevention, Simulation relation, static analysis|
Deadlocks are a common error in programs with lock-based concurrency and are hard to avoid or even to detect. One way for deadlock prevention is to statically analyze the program code to spot sources of potential deadlocks. Often static approaches try to confirm that the lock-taking adheres to a given order, or, better, to infer that such an order exists. Such an order precludes situations of cyclic waiting for each other’s resources, which constitute a deadlock.