eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-06-28
125:1
125:20
10.4230/LIPIcs.ICALP.2022.125
article
Distributed Controller Synthesis for Deadlock Avoidance
Gimbert, Hugo
1
Mascle, Corto
2
Muscholl, Anca
2
Walukiewicz, Igor
1
Université de Bordeaux, CNRS, France
Université de Bordeaux, France
We consider the distributed control synthesis problem for systems with locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction this problem is undecidable even for three processes each using a fixed number of locks. We propose two restrictions that make distributed control decidable. The first one is to allow each process to use at most two locks. The problem then becomes complete for the second level of the polynomial time hierarchy, and even in Ptime under some additional assumptions. The dining philosophers problem satisfies these assumptions. The second restriction is a nested usage of locks. In this case the synthesis problem is Nexptime-complete. The drinking philosophers problem falls in this case.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol229-icalp2022/LIPIcs.ICALP.2022.125/LIPIcs.ICALP.2022.125.pdf
Distributed Synthesis
Concurrency
Lock Synchronisation
Deadlock Avoidance