The authors present a technique which uses Petri nets to detect static deadlocks in concurrent Ada programs (Ada programs which use the tasking features of the language). This method addresses two kinds of static deadlock: what the authors refer to as inconsistency deadlocks, which result from incorrect entry calls, and circular deadlocks, as exemplified by the well-worn (but well-loved) dining philosophers problem. The authors refer to previous relevant work and claim that their work reduces “to some extent” the space and time complexities of comparable methods.

The authors assume that readers are familiar with Ada, the Ada rendezvous in particular. A familiarity with Petri nets is also a distinct advantage when reading this paper, although the authors do present an overview of Petri net invariants, on which their method depends.

The technique centers on translating Ada source programs into Ada nets, which are Petri net models that represent the flow of control in the original program. The deadlock detection algorithms are applied to the nets. Both algorithms are described in the paper, as are the sub-algorithms upon which they call. Examples illustrate the complete process, from source code via Petri net to deadlock detection. It would have been nice to have the task specifications as well as the bodies in the examples, because the task specification is a vital part of the documentation of Ada tasking programs.

The paper is fairly readable, although in places the meaning is not clear. When the authors say “for example to distinguish package function calls from task entry calls” I am not sure what they mean. This point is important because in well-written Ada programs, tasks, which cannot themselves be library units, will be hidden within packages, and their entries called via procedures (not functions) exported by the packages.

For those concerned with the correctness of Ada tasking programs, this paper will be of interest. Nonetheless, while I agree that deadlock detection tools like this are necessary, it would be a mistake for embedded system programmers to become dependent on them as an alternative to sound design and coding practice. For example, if no task which calls another task is allowed to have entries of its own, the circularity problem is eradicated. Alas, inconsistency is not so easily banished.