An axiomatic approach to control description and implementation
Ching-Chy Wang · 1983
The development of an axiomatic description of advanced control mechanisms in concurrent high level languages is presented by considering an abstract representation of run-time control states. Through this representation, the concepts involved in the control events can be formalized leading to a better conceptual view of concurrent control structures. Besides the benefits of semantic comprehension, the model can also be used to provide guidelines for the development of deletion strategies for program module instances which lead to efficient storage utilization. Using the notation developed, the strategies can be shown to be secure in that an instance is not deleted if it is needed subsequently in the execution. Certain types of deadlock situations are investigated through a detailed analysis of the control event model, enabling detection at run-time of deadlocks. In order to demonstrate the advantages of this approach of control description, an Ada-like language is adopted as the test language. The language is similar to Ada except that remote is included to provide an additional channel of data accessing among program modules. Security of reclaiming deadlock-related instances is based on the assumption that automatic recovery strategies are not provided. If the assumption is invalid, implementation efficiency can be achieved by reducing the cost of breaking deadlocks. If the cost of restarting a task is constant, the problem of breaking deadlocks with minimum cost reduces to that of finding a minimum cardinality decycling set (cutset) of a directed graph. Although the general problem of finding minimum cardinality cutset is NP-complete, a linear algorithm for its solution on reducible flow graphs is given by Shamir. We define the class of cyclically reducible graphs (CR-graphs) and present a polynomial time algorithm for finding minimum decycling sets of these graphs. Three basic transformations are introduced to characterize the class of CR-graphs. We show that these transformations have the Church-Rosser property. This is, the final graph is independent of the order of applying transformations.