A unifying theory of control dependence and its application to arbitrary program structuresTools Danicic, Sebastian; Barraclough, Richard; Harman, Mark; Howroyd, John; Kiss, Akos and Laurence, Michael. 2011. A unifying theory of control dependence and its application to arbitrary program structures. Theoretical Computer Science, 412(49), pp. 68096842. ISSN 03043975 [Article] No full text available
Official URL: http://dx.doi.org/10.1016/j.tcs.2011.08.033
Abstract or DescriptionThere are several similar, but not identical, definitions of control dependence in the literature. These definitions are given in terms of control flow graphs which have had extra restrictions imposed (for example, endreachability). We define two new generalisations of nontermination insensitive and nontermination sensitive control dependence called weak and strong controlclosure. These are defined for all finite directed graphs, not just control flow graphs and are hence allow control dependence to be applied to a wider class of program structures than before. We investigate all previous forms of control dependence in the literature and prove that, for the restricted graphs for which each is defined, vertex sets are closed under each if and only if they are either weakly or strongly controlclosed. Low polynomialtime algorithms for producing minimal weakly and strongly controlclosed sets over generalised control flow graphs are given. This paper is the first to define an underlying semantics for control dependence: we define two relations between graphs called weak and strong projections, and prove that the graph induced by a set of vertices is a weak/strong projection of the original if and only if the set is weakly/strongly controlclosed. Thus, all previous forms of control dependence also satisfy our semantics. Weak and strong projections, therefore, precisely capture the essence of control dependence in our generalisations and all the previous, more restricted forms. More fundamentally, these semantics can be thought of as correctness criteria for future definitions of control dependence.
