Deadlock Checking by a Behavioral Effect System for Lock Handling
- 講者Volker Stolz 博士 (Post Doctor of the University of Oslo, Norway)
邀請人：陳郁方老師 - 時間2011-07-13 (Wed.) 11:00 ~ 12:00
- 地點本所新館一樓106演講廳
摘要
Deadlocks are a common error in programs with lock-based concurrency and are hard to avoid or even to detect. One way for dead- lock prevention is to statically analyze the program code to spot sources of potential deadlocks. Often static approaches try to con rm 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.
In contrast, we do not enforce or infer an explicit order on locks. Instead we use a behavioral type and e ect system that, in a rst stage, checks the behavior of each thread or process against the declared behavior, which captures potential interaction of the thread with the locks. In a second step on a global level, the state space of the behavior is explored to detect potential deadlocks. We de ne a notion of deadlock-sensitive simulation to prove the soundness of the abstraction inherent in the behavioral de- scription. Soundness of the e ect system is proven by subject reduction, formulated such that it captures deadlock-sensitive simulation.
To render the state-space nite, we show two further abstractions of the behavior sound, namely restricting the upper bound on re-entrant lock counters, and similarly by abstracting the (in general context-free) behavioral e ect into a coarser, tail-recursive description. We prove our analysis sound using a simple, concurrent calculus with re-entrant locks.