The Semantics of Program Dependence

Robert Cartwright, Matthias Felleisen^{∗} Department of Computer Science Rice University Houston, TX 77251-1892

Abstract

Optimizing and parallelizing compilers for procedural languages rely on intermediate graph representations called program dependence graphs (pdgs) to express the essential control and data dependences among atomic program operations. In this paper, we provide a semantic justification for this practice by deriving two different forms of program dependence graph—the output pdg and the def-order pdg— and their semantic definitions from non-strict generalizations of the denotational semantics of the programming language. In the process, we demonstrate that both the output pdg and the deforder pdg (with minor technical modifications) are conventional data flow programs. In addition, we show that the semantics of the def-order pdg dominates the semantics of the output pdg and that both of these semantics dominate—rather than preserve—the semantics of sequential execution.

1 Program Dependence Graphs

Optimizing and parallelizing compilers for procedural languages rely on intermediate graph representations to express the essential control and data dependences of atomic program operations. Some prominent examples in the literature are the control flow graph, the call graph, the def-use chain [1], the data dependence graph [7], and the extended data-flow graph [2]. Recently, Ferrante, Ottenstein, and Warren [3] have proposed a comprehensive graph representation called the program dependence graph (pdg) that subsumes previous graph representations, creating a single structure suitable for scalar optimization [3, 8], vectorization [14], and general parallelization [15]. In addition, Horwitz, Prins, and Reps [4] have used a revised form of the pdg representation as a basis for integrating program revisions. To distinguish these two forms of the pdg, we use the term output pdg to refer to the original pdg [3] and the term def-order pdg to refer to the revised form [4].

A program dependence graph represents “[the] partial ordering on the statements and predicates in the program that must be followed to preserve the semantics of the original program” [3:322]—relaxing the implied total evaluation order of linear program text. Thus, the pdg is a data-flow representation for programs that captures the informal non-sequential semantics that compiler writers assign to programs. The widespread use of the pdg representation as a basis for program compilation and optimization raises many interesting questions about the semantic properties of the analysis process.

• Does the program dependence graph representation have a “natural” interpretation as a data-flow programming language?

• What are the appropriate denotational and operational semantics for this language?

• Does the translation from a textual representation into a dependence graph representation preserve the program semantics?

• Does the semantics of pdgs justify the common optimizing transformations?

• Can a semantic characterization of program dependence provide the insight required to develop better program optimization techniques?

As a first step towards a formal theory of program dependence, Horwitz, Prins, and Reps recently proved that the def-order pdg representation is adequate: programs with the same program dependence graphs have the same meaning. But no attempt has been made to provide a semantic justification for the program optimization process based on dependence analysis.

This paper, in conjunction with a companion paper by Selke [10], tackles the first three questions in the preceding list and presents three results:

∗The work of both authors was partially supported by NSF and DARPA.

0

1. The output pdg and def-order pdg representations [3, 4] for a program—with some minor technical modifications—are conventional data flow programs that can be derived from the denotational semantics of the original program.

2. The derivation also yields a denotational semantics of program dependence graphs that explains the significance of the data flow and control flow information.

3. The semantics of the output pdg is closer to the semantics of sequential execution than is the the semantics of the def-order pdg. More precisely, the semantics of the def-order pdg dominates the semantics of the output pdg, and both dominate the semantics of the original programming language.

The remainder of the paper consists of four sections. The next section defines the syntax and conventional semantics for a simple procedural programming language and describes the output pdg and def-order pdg representations for this language. In Section 3, we analyze the semantics of this language from the perspective of program optimization and introduce two non-strict (“lazy”) generalizations of the semantics that expose more parallelism. The fourth section contains our principal technical results. By semantically interpreting the concepts of control and data dependence, we derive a denotational definition of the control and data demand generated by program expressions. We then perform a staging analysis on the demand semantics, which produces a natural decomposition of the meaning function into two components: (i) a construction algorithm that builds program dependence trees and (ii) a meaning function that interprets these trees. At the end of Section 4, we describe how to build pdgs from program dependence trees. The final section presents directions for future research and some of the potential applications of our semantic characterization of program dependence.

2 The Programming Language W and Program Dependence

The typical programming language for optimizing and parallelizing compilers has a simple core consisting of assignment statements, sequencing constructs, loop constructs, and branching facilities. For the purpose of this discussion, we will focus our attention on a simple statement-oriented programming language W with the following abstract syntax:

s ::= x := e |

s; s |

if b then s else s |

while b do s where s ranges over statements, x ranges over a set of identifiers ide, and b and e range over a set of expressions exp. For the sake of generality, the set of expressions exp is left unspecified, but we assume that expressions may refer to identifiers in ide. The two functions Refs[[ · ]] and Defs[[ ·]] map programs and expressions to the sets of identifiers that occur in expressions and on the lefthand sides of assignment statements, respectively.

A definition of the denotational semantics of W is given in Figure 1. Since the syntactic domain exp is unspecified, the definition is parameterized over the domain val of denotations for expression and the meaning function E for mapping expressions to their denotations. The only restriction that we impose is the assumption that the domain val is flat.^{1}

The semantic domain for W-programs is constructed from the domain of values as the domain of functions mapping stores to stores:

store ⟶ store .

A store is a mathematical representation of the machine’s memory and maps identifiers to values:

ide ⟶ val .

The infix notation σ[x ← v] represents a functional update of the store σ that is strict in all three arguments.^{2} The updated store σ[x ← v] is identical to σ except that σ[x ← v] has the value v for variable x (assuming that σ, x, and v are all defined). Hence, the strict update function ·[· ← ·] : store ⟶ ide ⟶ val ⟶ store is defined by the following rules:

σ[x ← v] = ⊥ if σ = ⊥ ∨ x = ⊥ ∨ v = ⊥

and

σ[x ← v](z) = \{ \begin{matrix}σ(z) & z ≠ x \\ v & z = x \end{matrix}

in all other cases.

A program dependence graph consists of a set of nodes representing atomic computations and a set of edges representing dependences. The atomic computations are assignment statements and predicate expressions. The set of edges contains data dependence edges and control dependence edges. A dependence edge between two nodes indicates that the computation of the target node depends on the computation of the source node.

A program node A that uses a variable v has a data dependence on a definition B of v iff there is a path in Semantic Domains:

1A flat domain D is a partially ordered set ordinary data values augmented by the undefined value bottom (⊥) denoting a divergent computation. The ordering relation ⊑ is the least relation such that every element approximates itself and the undefined value ⊥ approximates every element.

2A function f is strict in an argument x iff it is undefined (⊥)

for all inputs where x is undefined (⊥).

u, v ∈ val  (unspecified)
σ ∈ store = ide ⟶ val

Semantics:

E : exp ⟶ store ⟶ val  (unspecified)
W_{strict} : stmt ⟶ store ⟶ store
W_{strict}[[x := e]] = λσ.σ[x ← E[[e]]σ]
W_{strict}[[s_{1} ; s_{2}]] = λσ.W_{strict}[[s_{2}]](W_{strict}[[s_{1}]]σ)
W_{strict}[[if b then s_{t} else s_{f}]] = λσ.E[[b]]σ ⟶ W_{strict}[[s_{t}]]σ, W_{strict}[[s_{f}]]σ
W_{strict}[[while b do s]] = fix(λwσ.E[[b]]σ ⟶ w(W_{strict}[[s]]σ), σ)

Figure 1: The Denotational Semantics of W

[figure: use-of(i); i := 2; j := 3; i := 1; j < 1; output; T; F]

Figure 2: The pdg for program P the flow chart representation of the program from B to A that does not contain an intervening definition of v. A predicate B controls a node A iff there are paths from B through the program that contain A and paths that do not contain A. B directly controls A if B controls A and there is a path from B to A that does not contain an intervening predicate that controls A. A program node A has a control dependence [3] on a predicate B iff B directly controls A.

There is another form of control dependence called output dependence [3] that must be respected for programs to execute in accord with the conventional sequential semantics. A definition A of a variable v has an output dependence on a preceding definition B of the same variable iff there is a path from A to B that does not contain an intervening definition of v. There is a relaxation of output dependence—more accurately, the transitive closure of output dependence—called deforder dependence [4] that ignores output dependences between definitions where there is no node that depends on both of them. A definition A of a variable v has a def-order dependence on a preceding definition B of the same variable iff there is a path from B to A and both A and B are the sources of data dependence edges to some program node.

The informal semantics underlying the dependence graph representation is an extended data-flow model of computation [3]. An assignment node in the graph computes a new identifier value; a predicate node determines a boolean value for the selection and elimination of other computation nodes. The incoming data dependence edges of a node specify the input values for the node’s computation; the outgoing data edges indicate which nodes depend on the result of the node. Control dependences have the task of ordering, selecting, and eliminating computations.

The crucial property of the data-flow model of computation is the absence of a centralized store and storeoriented operations. There is no notion of overwriting values in locations. Instead, an assignment node directly passes the generated binding to its successor nodes in the graph.

For an illustration of the pdg representation, consider the program

P =^{df} i := 1 ;

if j < 1 then i := 2 else j := 3 ;

use-of(i) .

The translation of P into dependence graph form produces the pdg in Figure 2. There are two data-flow edges, one from each assignment to i to the node demanding the value of i. The predicate node j < 1 controls the second assignment to i through a T-control edge and the assignment to j through an F-control edge. An output or def-order edge—depending on the graph representation—between the two assignment nodes for i specifies the order of evaluation between the two assignments. Both truth-value-labeled edges and def-order edges denote control dependences. The representation of while-loops is similar to those of if-statements, but introduces cyclic dependences and requires a classification of data dependences as loop-dependent or loopindependent [3, 4].

3 Non-Strict Semantics for W

The denotational semantics for W reflects the behavior of a sequential implementation of W. An assignment statement alters the contents of a memory cell. The effect of a sequence of statements is the compound effect of evaluating its components from left to right. The if-statement selects the appropriate branch for further evaluation. A while-loop composes the effects of repeated evaluations of its body statement until its guard evaluates to F.

The sequentiality of program execution is reflected in the denotational semantics of W by the strictness of store update function ·[· ← ·] used in the semantic function W_{strict}. Thus, if a statement s encountered in the sequential execution of the program p diverges for some input store σ, then the function W_{strict}[[p]] applied to σ yields the completely undefined store ⊥_{store} regardless of what statements follow s. For example, the straightline program

Q =^{df} y := 1 ; x := e; x := 2

diverges if the evaluation of the expression e diverges even though the value of e cannot affect the final value of x or y.

From the perspective of program optimization, the semantics of sequential execution is too restrictive. In the preceding program Q, the statement

x := e

is superfluous because it can never contribute to a final answer. Fortunately, it is easy to modify the denotational definition of W so that no assignment is evaluated unless it can affect the final contents of the program store [9]. The trick is to replace the strict update operation ·[· ← ·] by an update operation that is non-strict in the third argument. There are two important forms of non-strict update:

1. The first option, denoted ·[· ⇐ ·], is the standard “lazy” generalization of ·[· ← ·]. It is non-strict in both the first (store) and third (value) arguments. The store produced by the operation σ[x ⇐ v] is defined if either x is defined and either σ or v is defined.^{3} From an operational perspective, the Additional Semantic Domain:

3There is one exception to this rule: the result is undefined if σ is defined only at x and v are undefined.

δ ∈ update = store ⟶ ide ⟶ val ⟶ store

Semantics:

W : update ⟶ stmt ⟶ store ⟶ store

Wδ[[x := e]] = λσ.δ(σ, x, E[[e]]σ)
Wδ[[s_{1} ; s_{2}]] = λσ.Wδ[[s_{2}]](Wδ[[s_{1}]]σ)
Wδ[[if b then s_{t} else s_{f}]] = λσ.E[[b]]σ ⟶ Wδ[[s_{t}]]σ, Wδ[[s_{f}]]σ
Wδ[[while b do s]] = fix(λwσ.E[[b]]σ ⟶ wWδ[[s]]σ, σ)

Figure 3: The Generalized Denotational Semantics of W

computation of the value argument v is deferred until the value of the assigned identifier is demanded from the store. Moreover, the value v is never computed if a subsequent update on the same identifier is performed before the value is needed. Hence,

σ[x ⇐ v](z) = \{ \begin{matrix}⊥ & x = ⊥ \\ σ(z) & z ≠ x ∧ x ≠ ⊥ \\ v & z = x ∧ z ≠ ⊥ \end{matrix}

for all σ, x, v, z.

2. The second option, denoted ·[· ↩ ·], is partially “lazy”. It is non-strict only in the third (value) argument because the operation σ[x ↩ v] forces σ(x) to be evaluated. Hence, updates to different variables cannot interfere with one another, but updates to the same variable can. In particular, σ[x ↩ v] is defined at x only if both σ(x) and v are defined. From an operational perspective, ·[· ↩ ·] treats ⊥ as a “sticky” value: once a variable is bound to ⊥ it will always be bound to ⊥ regardless of subsequent updates. Hence, if x ≠ ⊥

σ[x ↩ v](z) = \{ \begin{matrix}σ(z) & z ≠ x \\ v & z = x ∧ σ(x) ≠ ⊥ \\ ⊥ & z = x ∧ σ(x) = ⊥ \end{matrix} .

We refer to the update operations ·[· ⇐ ·] and ·[· ↩ ·] as the lazy update and the lackadaisical update, respectively. It is easy to verify that the lazy update operation dominates^{4} the lackadaisical operation, and that both dominate the strict update operation defined in the previous section:

·[· ← ·] ⊑ ·[· ↩ ·] ⊑ ·[· ⇐ ·]  (†) .

Given these two lazy update functions, we can formulate two less restrictive semantic definitions for W and precisely describe their relation to the original semantics. To this end, we define a a new semantic function W based on W_{strict} that abstracts W_{strict} with respect to the update function. Figure 3 contains the complete definition of W. From W, we can obtain the original semantic function W_{strict} and the two non-strict variants as simple instantiations:

W_{strict} = W(·[· ← ·])
W_{lack} = W(·[· ↩ ·])
W_{lazy} = W(·[· ⇐ ·]) .

Since W is a continuous function of its update function argument, the approximation relations between update functions (†) imply the following approximation relations between the semantic functions:

W_{strict} ⊑ W_{lack} ⊑ W_{lazy} .

The differences among these three semantics is best illustrated by an example. If the expression e in the program Q is undefined for all stores, then Q has a different meaning in each semantic definition:

W_{strict}[[Q]] = λσ.⊥_{store}
W_{lack}[[Q]] = λσ.σ(y) ≠^{?} ⊥ ⟶ {(y, 1)}
W_{lazy}[[Q]] = λσ.{(x, 2), (y, 1)} .

4A function f : A → B dominates a function g : A → B iff ∀x ∈ A f(x) ⊒ g(x): if the computation of g(x) terminates, the computation of f(x) must terminate and yield the same answer.

In short, while the lazy semantics ignores undefined values produced as the results of irrelevant subcomputations, the lackadaisical semantics only ignores the undefined values corresponding to irrelevant variables. Consequently, we interpret these two non-strict generalizations of the semantics of W as formalizations of two different perspectives on what assumptions an optimizing compiler should make. In the following section, we show how these two perspectives have influenced the design of program dependence representations.

4 A Semantic Approach to Dependence

The motivation behind translating programs into dependence graph representations is the conviction that the functional representation of a computation exposes potential parallelism hidden by the sequential, storeoriented evaluation model associated with the conventional program text [Warren: private communication]. On the other hand, the goal of denotational semantics [9] is to define a functional meaning for programs that explains their operational behavior, yet avoids machinespecific details.

The preceding observation suggests that denotational semantics is closely related to dependence analysis. For this reason, we decided to investigate the hypothesis that program dependence graphs are a form of parallel intermediate code that can be derived from a demandoriented denotational semantics just as compilers and machine code can be derived from conventional denotational semantics [6, 11, 12, 13].

This section presents the results of that inquiry. In the first subsection, we show that a simple reformulation of a denotational definition exposes the data demands of expressions, revealing the data dependences between statements. The following subsection addresses the issue of control dependence. We introduce an explicit parameter for modeling the control predicates along the path from the root of the program to the current statement. The third subsection contains a staging analysis of the data and control demand semantics. The resulting separation of the semantic function produces an algorithm for constructing dependence trees and a meaning function for these trees. The final subsection addresses the issue of how to generate program dependence graphs from our dependence trees.

4.1 Data Dependence

The primary goal of dependence analysis is to eliminate the notion of a centralized store and to illuminate the data flow between subcomputations within a program. To achieve this goal, we must answer two questions:

1. Which subcomputations are required to determine the value of an identifier at any given point in the program?

2. Where is each computed value used in the remainder of the program?

However, the semantic function W_{strict} and its instantiations are poorly suited to answering these questions because they presume a store-oriented model of computation. To eliminate this reliance on a central store, we must transform the semantic function W into a function V that extracts the value of a designated identifier— rather than the entire store—from a program.

A naïve way to write the new semantic function V would be to apply the result of W to an identifier. But this approach would merely hide the central store rather than eliminate it. Since we know the name of the designated identifier before the program is executed but know nothing about the contents of the initial store, the insight gained from research on deriving compilers from denotational semantics [6] suggests that we should rearrange the order of the arguments in W so that the identifier argument precedes the initial store argument. Then we can apply the transformed semantic function to the identifiers that appear in program expressions as part of a static analysis process akin to compilation. Hence, we want to rewrite the semantic function

W : update ⟶ stmt ⟶ store ⟶ (ide ⟶ val)

as a semantic function

V : update ⟶ stmt ⟶ ide ⟶ store ⟶ val

that is mathematically equivalent, i.e.,

Vδsxσ = Wδsσx for all δ, s, x, σ .

The complete definition of V is given in Figure 4. Like W, V can be instantiated using three different update functions to produce three different, but closely related, semantic functions:

V_{strict} = V(·[· ← ·])
V_{lack} = V(·[· ↩ ·])
V_{lazy} = V(·[· ⇐ ·]) .

A closer examination of the non-strict versions of V reveals that we can simplify the definition of their assignment clauses. In both definitions, we can move the equality test on the identifier forward, out of the update operation. For the lazy update, this analysis produces the following assignment clause:

V_{lazy}[[x := e]] = λiσ.σ[x ⇐ E[[e]]σ](i)
= λiσ.i =^{?} x ⟶ E[[e]]σ, σ(i)

(by the definition of · [· ⇐ ·])

= λi.i =^{?} x ⟶ E[[e]], λσ.σ(i) .

V : update ⟶ stmt ⟶ ide ⟶ store ⟶ val

Vδ[[x := e]] = λiσ.δ(σ, x, E[[e]]σ)(i)
V_{lazy}[[x := e]] = V(·[· ⇐ ·])[[x := e]]
= λi.i =^{?} x ⟶ E[[e]], λσ.σ(i)
V_{lack}[[x := e]] = V(·[· ↩ ·])[[x := e]]
= λi.i =^{?} x ⟶ (λσ.σ(i) =^{?} ⊥ ⟶ ⊥, E[[e]]), λσ.σ(i)
Vδ[[s_{1} ; s_{2}]] = λiσ.Vδ[[s_{2}]]i(λj.Vδ[[s_{1}]]jσ)
Vδ[[if b then s_{t} else s_{f}]] = λiσ.E[[b]]σ ⟶ Vδ[[s_{t}]]iσ, Vδ[[s_{f}]]iσ
Vδ[[while b do s]] = fix(λw.λiσ.E[[b]]σ ⟶ wi(λj.Vδ[[s]]jσ), σ(i))

Figure 4: The Generalized Demand Semantics of W

For the lackadaisical update, the same analysis yields a slightly different result:

V_{lack}[[x := e]] =

λi.i =^{?} x ⟶ (λσ.σ(i) =^{?} ⊥ ⟶ ⊥, E[[e]]), λσ.σ(i) .

These two transformations show that it is possible to identify the final assignments for a given identifier by statically analyzing the denotational meaning of the program—provided the update functions are non-strict. But this form of analysis alone is too weak to identify the data dependences in a program. For a given identifier, the semantic functions V_{lazy} and V_{lack} identify the final assignment(s) to the identifier and then wait for the computation of the input store. Without the store, it is not clear how to determine the denotation of the righthand side of the assignment statement.

At this point, we must recall the second question from the beginning of this subsection: how do we determine where a value is needed? Before the semantic function V can produce the final value for some identifier x, we must provide the data values for evaluating the righthand sides of the final assignments for x. Since the syntactic function Refs[[ · ]] determines the finite set of identifiers referenced in an expression, we can restrict the data demand of an expression e to the values of all identifiers in the set Refs[[e]] instead of demanding the entire store. In other words, the right-hand side of a final assignment generates a demand for the values of a finite set of identifiers. The definition of V tells us how to propagate this demand. Since the input store σ to each final assignment is built by the recursive application of the function V, the application of σ to the demanded identifiers reveals the final assignments to these identifiers within the preceding computation. This process can be repeated to identify all of the data dependences in the program. In fact, we could perform a staging analysis (as described for C in Section 4.3) to generate a “structural” form of program dependence graph similar to the pdgs presented in [2]. However, this form of pdg expresses data dependences between expressions and compound statements instead of between expressions and assignments. To analyze data dependence at the level of atomic assignments and predicates, we need to analyze control information as well.

In summary, the transformation of semantic function W into V produces a demand-driven semantics for W that reveals the data dependences between the expressions and statements in a program.

4.2 Control Dependence

The second component of a program dependence analysis is the determination of control dependences between assignments and predicates. In the definition of the semantic function V, the code for handling if and while is motivated by an operational interpretation of W. After evaluating the predicate, the function selects the appropriate branch and determines the value of the demanded identifier computed by that branch. However, from a mathematical perspective, the function determines the values of both branches and selects the relevant one afterwards. The value generated by the non-selected branch is often bottom (⊥_{val}) because the predicates typically enforce conditions that prevent the execution of erroneous or irrelevant computations. This observation suggests that if we could guarantee that nonselected branches always produce the value ⊥, then we could modify V to merge the results of alternative statements by returning the first (and only) result other than bottom.

The obvious choice for the merge operation is the least upper bound operation ⊔, which on a flat domain always returns the proper value when applied to a proper value and bottom. Unfortunately, the ⊔ operation is not defined on the entire domain val, because the least upper bound of two non-bottom values does not exist. Although this situation cannot occur within W-programs, we need to extend the val domain to cast the least upper bound operation into a continuous function on the entire domain. We can overcome this problem by attaching a top element ⊤ to the domain val above all of the other elements. The resulting domain val^{⊤} then forms a complete lattice and the least upper bound operation is a continuous function. An added benefit of this extension is that it creates a framework in which we can define the semantics of program dependence graphs that are not the images of W-programs.

To incorporate val^{⊤} in our revised denotational definition of W, we must also modify the definition of the domain store which depends on val. We will use the domain

store^{⊤} = ide ⟶ val^{⊤}

instead of the domain store.

Given the extended domain of values val^{⊤}, we can now abstract V with respect to an explicit control parameter (κ) that represents the accumulated boolean value of the predicates along the control path from the root of the program to the current statement. This parameter passes information to atomic assignments indicating whether or not they are reachable in a given computation. In the former case, they pass their computed values to all of the sites (assignments and predicates) that demand them. In the latter case, they pass the default value ⊥. When the values from all of the final assignments to an identifier in a program component are merged to produce the demanded answer, only one of the final assignments is reachable. Without this extra control information, we cannot transmit data values directly from definition sites (assignments) to their use sites (assignments and predicates). The control parameter directly corresponds to the control information that is passed along control dependence edges in a pdg.

The abstraction V with respect to the control parameter κ yields a new function C with the type

update ⟶ stmt ⟶ ide ⟶ bool ⟶ store^{⊤}
⟶ val^{⊤} .

A complete definition of C including instantiations for the non-strict updates ·[· ⇐ ·] and ·[· ↩ ·] appears in Figure 5. The clause defining the meaning of assignments is:

Cδ[[x := e]] = λiκσ.κ ⟶ δ(σ, x, E[[e]]σ)(i), ⊥ .

When the update operation δ is instantiated as ·[· ⇐ ·] or ·[· ↩ ·], we can unfold the definition of the update operation to reveal both the control dependences and the data dependences between statements and expressions. The definition of C includes one important feature that does not occur in the definition of V. In particular, the clauses in C defining the meaning of if and while statements interpret these statements as identity transformations (empty statements) if they are irrelevant (no definition of the demanded variable occurs in the text of the statement). This feature changes the meaning of W because it eliminates a possible source of divergence, namely the evaluation of the predicates governing the execution of irrelevant if and while statements. Hence, C satisfies the following two conditions

Vδ[[p]]iσ ⊑ Cδ[[p]]iTσ
⊥ = Cδ[[p]]iF(λj.⊥) .

We could eliminate this difference between V and C at the cost of generating extra control dependences on the predicates of irrelevant if and while statements. In this case, C would satisfy the stronger condition

Vδ[[p]]iσ = Cδ[[p]]iTσ

instead of the inequality relation given above.

4.3 Program Dependence Trees

Now that we have produced a denotational semantics that identifies the essential data and control dependences for computing the value of each identifier, we can perform a staging analysis to extract a code representation for W-programs [6, 11, 12, 13]. A staging analysis transforms a denotational definition and decomposes it into a static meaning function, which constructs an intermediate representation for a program, and an interpreter, which executes the intermediate code. The key step in a staging analysis is to transform the definition of the meaning function to make as many phrases as possible independent of the program input. Then the static meaning function can construct concrete representations for the results of applying these phrases to program text.

In our case, the staging analysis must determine which parameters of the semantic function C depend on the initial store. We can then construct a new semantic function C′ that abstracts the affected parameters with respect to the initial store and passes the initial store as the final argument. From the specification of C’s domain,

stmt ⟶ ide ⟶ bool ⟶ store^{⊤} ⟶ val^{⊤},

Modified Semantic Domains:

u, v ∈ val^{⊤}  (val ∪ {⊤})
σ ∈ store^{⊤} = ide ⟶ val^{⊤}

Semantics: C : update ⟶ stmt ⟶ ide ⟶ bool ⟶ store^{⊤} ⟶ val^{⊤}

Cδ[[x := e]] = λiκσ.κ ⟶ δ(σ, x, E[[e]]σ)(i), ⊥
C_{lazy}[[x := e]] = C(·[· ⇐ ·])[[x := e]]
= λiκσ.i =^{?} x ⟶ (κ ⟶ E[[e]]σ, ⊥), σ(i)
C_{lack}[[x := e]] = C(·[· ↩ ·])[[x := e]]
= λiκσ.i =^{?} x ⟶ (κ ∧ σ(i) ≠ ⊥ ⟶ E[[e]]σ, ⊥), σ(i)
Cδ[[s_{1} ; s_{2}]] = λiκσ.Cδ[[s_{2}]]iκ(λj.Cδ[[s_{1}]]jκσ)
Cδ[[if b then s_{t} else s_{f}]] = λiκσ.i ∉ Defs[[s_{t}]] ∪ Defs[[s_{f}]] ⟶ σ(i),
let κ^{+} = κ ∧ E[[b]]σ; κ^{−} = κ ∧ ¬E[[b]]σ
in \begin{matrix}(i ∉ Defs[[s_{t}]] ⟶ (κ^{+} ⟶ σ(i), ⊥), Cδ[[s_{t}]]i κ^{+} σ) ⊔ \\ (i ∉ Defs[[s_{f}]] ⟶ (κ^{−} ⟶ σ(i), ⊥), Cδ[[s_{f}]]i κ^{−} σ) \end{matrix}

Cδ[[while b do s]] = fix(λw.λi κ σ.
i ∉ Defs[[s]] ⟶ σ(i),
let κ^{+} = κ ∧ E[[b]]σ; κ^{−} = κ ∧ ¬E[[b]]σ
in (w i κ^{+}(λj.Cδ[[s]]jκ^{+}σ)) ⊔ (κ^{−} ⟶ σ(i), ⊥)

Figure 5: Demand and Control Semantics of W

and its semantic clauses, it is clear that at an arbitrary point in the evaluation, both the control parameter and the store parameter depend on the initial store. This analysis suggests that function C′ should have the the type

stmt ⟶ ide ⟶ (store^{⊤} ⟶ bool )
⟶ (store^{⊤} ⟶ store^{⊤})
⟶ store^{⊤} ⟶ val^{⊤},

but this formulation of C′ treats the program text preceding the current statement as a function from store^{⊤} to store^{⊤}. As we observed earlier, the meaning of the current statement does not depend on the entire input store, but only on the values of selected variables. Hence, we can re-apply the same trick that we used to eliminate the central store from W: move the identifier argument from the answer store (produced in this case by the preceding program text) to the beginning of the argument list:

stmt ⟶ ide ⟶ (store^{⊤} ⟶ bool )
⟶ (ide ⟶ store^{⊤} ⟶ val^{⊤})
⟶ store^{⊤} ⟶ val^{⊤}.

In writing new semantic function C′, we must preserve the semantics given by the function C. The initial control parameter T and the initial store of C become parameters that are abstracted over the initial store, and the initial store becomes the last argument:

C′δ[[p]]i(λσ.T)(λiσ.σ(i))σ_{0} = Cδ[[f]]piTσ_{0}.

Given this invariant, it is straightforward to rewrite C’s clauses to match the types of the new semantic domain. The result of the staging analysis appears in Figure 6. This definition shows that it is possible to determine which decisions made during conventional program execution are independent of the initial store and where C′ : update ⟶ stmt ⟶ ide ⟶ (store^{⊤} ⟶ bool) ⟶ (ide ⟶ store^{⊤} ⟶ val^{⊤}) ⟶ store^{⊤} ⟶ val^{⊤}

C′δ[[x := e]] = λiκγσ.κσ ⟶ (δ(σ, x, e))(i), γiσ
C_{lazy}[[x := e]] = C′(·[· ⇐ ·])[[x := e]]
= λiκγ.i =^{?} x ⟶ λσ.(κσ ⟶ E[[e]](λj.γjσ), ⊥), λσ.γiσ
C_{lack}[[x := e]] = C′(·[· ↩ ·])[[x := e]]
= λiκγ.i =^{?} x ⟶ λσ.(κσ ∧ σ(i) ≠^{?} ⊥ ⟶ E[[e]](λj.γjσ), ⊥), λσ.γiσ
C′δ[[s_{1} ; s_{2}]] = λiκγ.C′δ[[s_{2}]]iκ(λj.C′δ[[s_{1}]]jκγ)
C′δ[[if b then s_{t} else s_{f}]] = λiκγ.

i ∉ Defs[[s_{t}]] ∪ Defs[[s_{f}]] ⟶ γi,

let κ^{+} = λσ.κσ ∧ E[[b]](λj.γjσ); κ^{−} = λσ.κσ ∧ ¬E[[b]](λj.γjσ)

in \begin{matrix}(i ∉ Defs[[s_{t}]] ⟶ (λσ.κ^{+}σ ⟶ γiσ, ⊥), (λσ.C′δ[[s_{t}]]iκ^{+}γσ)) ⊔ \\ (i ∉ Defs[[s_{f}]] ⟶ (λσ.κ^{−}σ ⟶ γiσ, ⊥), (λσ.C′δ[[s_{f}]]i κ^{−} γσ)) \end{matrix}

C′δ[[while b do s]] = fix(λw.λiκγ.

i ∉ Defs[[s]] ⟶ γi,

let κ^{+} = λσ.κ ∧ E[[b]](λj.γjσ); κ^{−} = λσ.κ ∧ ¬E[[b]](λj.γjσ)

in (λσ.κ^{−}σ ⟶ γiσ, ⊥) ⊔ (wiκ^{+}(λj.C′δ[[s]]jκ^{+}γ))

Figure 6: Staged Semantics of W

the initial store is really needed. More importantly, the evaluation of a program using the function C′ does not rely on a central store; the only stores involved are local stores for each assignment statement and predicate expression.^{5}

The last step in our staging analysis is the decomposition of C′ into two functions: a static meaning function and an interpreter. If we apply C′ to all the required arguments except the initial store, it returns a function that maps the initial store to a value. But this function has exactly the same type as abstract machine code, which maps initial stores to answers. If we devise a concrete representation for this code, we can decompose C′ into a “compiler” function G that constructs the code and an “interpreter” function P that determines the meaning of code.

Figure 7 defines the concrete code representation and the functions G and P. These definitions rely on standard domain constructions and operators explained in the Appendix. An assignment statement

x := e produces a data-node consisting of the uninterpreted right-hand side expression e, a finite set of dependence trees indexed by the identifiers in e (which computes the inputs to the expression), and a control-node, which computes the value of the control predicate governing the flow of the assignment statement’s output. An if-statement generates a pair of data-nodes, one for each arm of the if-statement. A while-loop produces an infinite sequence [d_{0}, d_{1}, …, d_{k}, …] of data-nodes, where d_{k} computes exactly k iterations of the loop. A control-node is either the atomic code true_{c}, which represents the initial predicate, or a data-node tagged with the value T or F; the expression field in the tagged data-node is the text of the controlling predicate and the tag indicates the boolean value that the predicate must produce to satisfy the control dependence.

The separation of the semantic function C′ into the functions G and P is a simple process. Every time C′ returns a function that maps the initial store to a value, G must construct a concrete representation for the function. For example, when C′(·[· ⇐ ·]) returns the function

λσ.(κσ ⟶ E[[e]](λj.γjσ), ⊥)

in the assignment clause, we see that the parameters of Semantic Domains:

5By making more assumptions about the expression language, we could also eliminate the local stores.

c_{σ} ∈ code-table = ide ⟶ ∘ code  (finite table of code)
data-node = exp ⊗ code-table ⊗ control-node)  (data node: ⟨e, c_{σ}, c_{κ}⟩)
c ∈ code = (data-node ⊗ data-node) ⊕ data-node^{+}  (pairs and sequences of data nodes)
c_{κ} ∈ control-node = true_{c} ⊕ data-node ⊕ data-node  (control node:
true_{c}, ⟨T, c, c_{σ}, c_{k}⟩, ⟨F, c, c_{σ}, c_{k}⟩)

Generating Dependence Trees:

G :  update ⟶ stmt ⟶ ide ⟶ control-node ⟶ code-table ⟶ code
G_{lazy}[[x := e]] = G(·[· ⇐ ·])[[x := e]]
= λiκγ.i =^{?} x ⟶ ⟨e, {(j, γj) | j ∈ Refs[[e]]}, κ⟩, γi
G_{lack}[[x := e]] = G(·[· ↩ ·])[[x := e]]
= λiκγ.i =^{?} x ⟶ ⟨e, {(j, γj) | j ∈ Refs[[e]]} ∪ {(i, γi)}, κ⟩, γi
Gδ[[s_{1} ; s_{2}]] = λiκγ.Gδ[[s_{2}]]iκ(λj.(Gδ[[s_{1}]]jκγ))
Gδ[[if b then s_{t} else s_{e}]] = λiκγ.

i ∉ Defs[[s_{t}]] ∪ Defs[[s_{f}]] ⟶ γi, let κ^{+} = ⟨T, b, {(j, γj) | j ∈ Refs[[b]]}, κ⟩; κ^{−} = ⟨F, b, {(j, γj) | j ∈ Refs[[b]]}, κ⟩

in \begin{matrix}⟨(i ∉ Defs[[s_{t}]] ⟶ ⟨⟨i, \{(i, γi)\}, κ^{+}⟩⟩, Gδ[[s_{t}]]iκ^{+}γ)), \\ (i ∉ Defs[[s_{f}]] ⟶ ⟨⟨i, \{(i, γi)\}, κ^{−}⟩⟩, Gδ[[s_{f}]]iκ^{−}γ))⟩ \end{matrix}
Gδ[[while b do s]] = fix(λw.λiκγ.

i ∉ Defs[[s]] ⟶ γi, let κ^{+} = ⟨T, b, {(j, γj) | j ∈ Refs[[b]]}, κ⟩; κ^{−} = ⟨F, b, {(j, γj) | j ∈ Refs[[b]]}, κ⟩

in ⟨i, {(i, γi)}, κ^{−}⟩⟩ ∘ (wiκ^{+}(λj.Gδ[[s]]jκ^{+}γ))

Interpreting Dependence Trees:

P :  code ⟶ store^{⊤} ⟶ val^{⊤}
P[[[c_{1}, c_{2}, …]]] = λσ.P_{d}[[c_{1}]]σ ⊔ P[[[c_{2}, …]]]σ
P[[⟨c_{1}, c_{2}⟩]] = λσ.P[[c_{1}]]σ ⊔ P[[c_{2}]]σ
P_{d} :  data-node ⟶ store^{⊤} ⟶ val^{⊤}
P_{d}[[⟨c, c_{e}, c_{k}⟩]] = λσ.P_{c}[[c_{k}]]σ ⟶ E[[c]]{(j, P[[c_{j}]]σ) | (j, c_{j}) ∈ c_{e}}, ⊥
P_{c} :  control-node ⟶ store^{⊤} ⟶ bool^{⊤}
P_{c}[[true_{c}]] = λσ.T
P_{c}[[⟨T, c, c_{e}, c_{k}⟩]] = λσ.P_{c}[[c_{k}]]σ ∧ E[[c]]{⟨j, P[[c_{j}]]σ⟩ | (j, c_{j}) ∈ c_{e}}
P_{c}[[⟨F, c, c_{e}, c_{k}⟩]] = λσ.P_{c}[[c_{k}]]σ ∧ ¬E[[c]]{⟨j, P[[c_{j}]]σ⟩ | (j, c_{j}) ∈ c_{e}}

Figure 7: Dependence Tree Semantics of W this definition are the expression e, the control parameter κ, and the intermediate function γ that maps the identifiers in e to the code trees for computing the respective values. Hence, the code representation for this function is the data-node

⟨e, {(j, γj) | j ∈ Refs[[e]]}, κ⟩

since the rest of the function is reconstructible from this information. The other clauses are derived in a similar way.

As mentioned above, the composition of P and G is identical to C′:

P(G(·[· ⇐ ·])[[p]]i(true_{c})(λiσ.σ(i))σ_{0}

= C′(·[· ⇐ ·])[[p]]i(λσ.T)(λiσ.σ(i))σ_{0}.

The finite set formation operation (denoted by braces {·}) in the definition of P_{c} is strict. Consequently, a code expression c is never evaluated until all of its data dependences and control dependences have been satisfied.

The trees that we generate for the lazy semantics and the lackadaisical semantics, respectively, are essentially the infinite unwindings of the corresponding def-order pdgs and output pdgs. The only difference between the lazy code trees and the infinite unwindings of def-order pdgs is the presence of valve nodes in the code trees instead of def-order edges.^{6} Similarly, the only difference between our lackadaisical code trees and the infinite unwindings of output pdgs is the presence of valve nodes in our code trees in addition to the output dependence edges.

Valve nodes are produced by the code generator γ when it discovers the definition (final assignment) of a demanded identifier in while-loop or in only one arm of a if-statement. The valve controls the flow of the value produced by the preceding definition to the demanding site. If the new definition of the identifier is executed then the valve blocks the flow of the value from the preceding definition. As we mentioned above in the discussion of the semantic function C, the valve nodes ensure that only one non-bottom value is transmitted to a consuming node. From a semantic perspective, the def-order and output edges included in conventional pdg representations are insufficient. Neither form of edge passes the precedence information about multiple definitions of the same identifier to the consuming nodes that must make the discrimination. Thus, in a conventional def-order or output pdg, a consuming node may receive several different values for the same identifier, but it cannot determine which one is “correct” without access to global information about the status of the associated output or def-order dependences.

Figure 8 illustrates the difference between our code trees and the unwound def-order pdgs for the simple program P (presented as a conventional pdg in Figure 2). When the use-node for i has received the value from the first assignment to i and the second assignment has yet to provide a value, the use-node cannot tell whether to accept the first value for i as the final one or to wait for a value to be transmitted along the second data-flow edge for i. The decision depends on the evaluation of the def-order or output edge between the first and second assignment to i, which is completely disassociated from the use-node for i. The introduction of valve nodes as in Figure 8 solves this problem. Since the new valve node (*) is under the control of the if-predicate and causes either the second assignment node or the valve node to send the value ⊥_{val}, only one proper value ever reaches the use-node. As a result, the evaluation of the usenode no longer depends on non-associated pieces of the graph.

4.4 Collapsing Trees into Graphs

To collapse a tree into a graph, we partition the nodes of the tree into a finite set of equivalence classes and construct the graph determined by merging all of the nodes in the same equivalence class. The equivalence relation is defined by equating all of the tree nodes that correspond to the same assignment statement or predicate in the program. Valve nodes are equated if they have have the same controlling predicate (in the program text), the same demanded variable, and the same truth label (Tor F) on the edge to the controlling node.

For loop-free programs, the unwinding of the collapsed graph is identical to the original code tree because all of the nodes in an equivalence class in the tree have exactly the same predecessors (subtrees): see Figure 8. For programs with loops, however, the collapsed graph does not contain enough information to reconstruct the original code tree. The problem is that we cannot distinguish loop-carried data dependence edges from loop independent edges. We can overcome this problem by appropriately labeling the edges involving loop nodes, but the details of the tree reconstruction process are complex and lie beyond the scope of this paper. For a simple example, we include our variant for the lazy pdg for the following simple program:

R =^{df} s := 0 ; x := 1 ;

while x ≤ N do

\begin{matrix}s := s + x; \\ x := x + 1 \end{matrix}

The result appears in Figure 9. Edges with a bar represent loop-carried data dependence edges, others are

6There is another minor difference between our code trees and def-order pdgs as defined in [4]. In contrast to our code trees and other pdg representations [3], Horwitz et al include nodes corresponding to dead code in their representation. Their version of the pdg is designed to support program integration where dead code may become live after subsequent integration steps.

[figure: use-of(i); i := i (*); i := 1; j < 1; i := 2; F; T; use-of(i); i := i (*); i := 1; j < 1; i := 2; j < 1; F; T; (a); (b)]

Figure 8: Semantic pdg for Program P

[figure: s := s; s := s; s := 0; x ≤ N; F; s := s + x; |; x := x + 1; |; x := 1; |; |; T; F; T]

Figure 9: Semantic-based Pdg for Program R either control or data dependences.

5 Directions for Future Research

Although the semantic analysis presented in this paper is instructive, it is too narrow to serve as a practical framework for expressing and justifying program optimizations. To satisfy this goal, we must expand the programming language to include the all of the fundamental operations included in real programming languages, namely composite data structures (arrays, pointers and records), procedures, and more general control structures. In conjunction with this effort, we also intend to develop an equational calculus for reasoning about pdgs. Given this machinery, it should be possible to construct an optimization laboratory that enables compiler writers to specify optimizing transformations in concise, formal notation; to generate experimental optimizing compilers from these specifications; and to prove the correctness of the incorporated optimizations.

Acknowledgements. We gratefully acknowledge several discussions with Joe Warren, Thomas Reps, and Susan Horwitz.

References

1. Aho,  A.,  R.  Sethi,  and

J. Ullman. Compilers—Principles, Techniques, and Tools. Addison-Wesley, Reading, Mass., 1985.

2. Ferrante, J. and K. Ottenstein. A program form based on data dependency in predicate regions. In Proc. 10th ACM Symposium on Principles of Programming Languages, 1983, 217–236.

3. Ferrante, J., K. Ottenstein, and J. Warren. The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 9(3), 1987, 319–349.

4. Horwitz, S., J. Prins, and T. Reps. On the adequacy of program dependence graphs representing programs. In Proc. 15th ACM Symposium on Principles of Programming Languages, 1988, 146–157.

5. Horwitz, S., J. Prins, and T. Reps. Integrating non-interfering versions of programs. In Proc. 15th ACM Symposium on Principles of Programming Languages, 1988, 133–145.

6. Jørring, U. and W. L. Scherlis. Compilers and staging transformations. In Proc. 13th ACM Symposium on Principles of Programming Languages, 1986, 86–96.

7. Kuck, D. J., R. H. Kuhn, D. A. Padua, and M. Wolfe. Dependence graphs and compiler optimizations. In Proc. 8th ACM Symposium on Principles of Programming Languages, 1981, 207–218.

8. Ottenstein, K. J. An intermediate program form based on a cyclic data-dependence graph. Technical Report No 81-1, Department of Computer Science, Michigan Tech. University, 1981.

9. Schmidt, D.A. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Newton, Mass., 1986.

10. Selke, R. P. A Rewriting Semantics for Program Dependence Graphs. In Proc. 16th ACM Symposium on Principles of Programming Languages, 1989, 12–24

11. Wand, M. Loops in combinator-based compilers. In Proc. 10th Symposium on Principles of Programming Languages, 1983, 190–196.

12. Wand, M. Semantics-directed machine architecture. In Proc. 9th Symposium on Principles of Programming Languages, 1982, 234–241.

13. Wand, M. Deriving target code as a representation of continuation semantics. ACM Trans. Program. Lang. Syst. 4(3), 1982, 496–517.

14. Warren, J. A hierarchical basis for reordering transformations. In Proc. 11th ACM Symposium on Principles of Programming Languages, 1984, 272– 282.

15. Wolfe, M. J. Optimizing Supercompilers for Supercomputers. Ph. D. dissertation, University of Illinois, 1982.

Appendix

The definitions of the semantic functions G and P rely on the domain constructors ⊗ (product), ⊕ (sum), ^{+} (infinite sequences), and ⟶ ∘ (finite functions) together with the associated functions ⟨·, ·⟩ and ∘ for constructing pairs and infinite sequences, respectively. The domain operators ⊗, ⊕, and ·^{+} are defined by the following equations:

A ⊗ B = {⊥} ∪
{(a, b) | a ∈ A \ {⊥} ∧ b ∈ B \ {⊥}}
A ⊕ B = {(F, a) | a ∈ A \ {⊥}} ∪
{(T, b) | b ∈ B \ {⊥}} ∪ {⊥}
A_{⊥} = {⊥} ∪ {(T, a) | a ∈ A}
A^{+} = A ⊗ (A^{+})_{⊥}

The values T and F are used as “tags” in the construction of composite objects; the objects (T, a) and (F, a) are distinct from ⊥ regardless of the value of a (including a = ⊥). The binary function

⟨·, ·⟩ : A × B ⟶ A ⊗ B

constructs elements of A ⊗ B as follows:

⟨a, b⟩ = \{ \begin{matrix}(a, b) & if a ≠ ⊥ ∧ b ≠ ⊥ \\ ⊥ & otherwise \end{matrix} .

The expression ⟨e_{1}, e_{2}, …, e_{n}⟩ abbreviates

⟨e_{1}, ⟨e2, …⟩⟩

Similarly, the expression [e_{1}, e_{2}, e_{3}, …] abbreviates

⟨e_{1}, (T, ⟨e_{2}, (T, ⟨e_{3}, (T, …)⟩⟩⟩

The infix operator

∘ : A × A^{+} ⟶ A^{+}

is defined by:

a_{0} ∘ [a_{1}, a_{2}, …] = ⟨a_{0}, ⟨T, [a_{1}, a_{2}, …]⟩⟩
= [a_{0}, a_{1}, a_{2}, …].

The domain A ⟶ ∘ B is the set of all finite subsets S of A ⊗ B that correspond to functions: (a, b) ∈ S and (a, b′) ∈ S implies b = b′. We frequently interpret elements of A ⟶ ∘ B as functions in A ⟶ B.