A Graph-Theoretic Characterization of the PVchunk Class of Synchronizing Primitives

Many of the process synchronization problems studied in the literature are of the form of a conjunction of finitely many conditions of the type “process pᵢ blocks process pⱼ”. Such problems may be expressed as directed graphs whose nodes represent the processes and where there is an edge from node i to node j if and only if process pᵢ blocks process pⱼ. We characterize the class of graphs which correspond to the system of synchronizing primitives of Vantilborgh and van Lamsweerde in terms of a normal form representation and present an efficient algorithm for determining whether an arbitrary graph is in this class.