  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 Sigma2P-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.
