Syntactic approach to the deadlock detection problem

A method for solving the deadlock detection problem in operating systems with single unit resources is introduced by using the formalism of the automata and languages theory. The waiting relations between processes are represented in a wait-string. The study of the properties of wait-strings which contain deadlocked processes allows a solution to be obtained for the deadlock detection problem in the form of a finite automation (FA). The designed FA, which accepts the wait-strings with deadlock, acts as a deadlock detection algorithm. Its performance is proved. The design method of the FA is itself a detection algorithm based on the same principles. Therefore its formal proof is also valid, and can be used when strong memory requirements are imposed.<>