Avoiding Deadlocks in Lock-Sharing Systems

We consider distributed synthesis problem where the task is to construct a controller for each process so that the controlled system does not have a deadlock. In our model processes synchronize by taking and releasing locks. A classical dinning philosophers problem is an example of a system of this kind. A strategy for each process has access only to local information, it should decide on a next action of a process knowing solely the previous actions of the process. The problem is undecidable even when every process can use at most four locks. However, when each process can use at most two locks the problem is solvable in the second level of the polynomial hierarchy, and even in PTIME under some additional assumptions. Dining philosophers problem uses two locks per process. We also prove that the problem is decidable when the number of locks per process is not bounded but locks must be used in a nested manner. This is joint work with Hugo Gimbert, Anca Muscholl and Igor Walukiewicz.

Authors

• Corto Mascle

Keywords

No keywords are indexed for this paper.