Distributed controller synthesis for deadlock avoidance

TL;DR

This paper addresses the challenge of synthesizing distributed controllers to prevent deadlocks in systems with locks, proposing restrictions that make the problem decidable and analyzing its computational complexity.

Contribution

It introduces two restrictions—limited lock usage per process and nested lock usage—that render the deadlock avoidance synthesis problem decidable and characterizes their computational complexity.

Findings

Distributed control synthesis is undecidable without restrictions.

Restricting each process to two locks makes the problem $ ext{Sigma}_2^P$-complete.

Nested lock usage leads to NEXPTIME-complete complexity.

Abstract

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 $\Sigma_2^P$-complete, 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.