Dependence analysis

In compiler theory, dependence analysis produces execution-order constraints between statements/instructions. Broadly speaking, a statement S2 depends on S1 if S1 must be executed before S2. Broadly, there are two classes of dependencies--control dependencies and data dependencies.

Dependence analysis determines whether it is safe to reorder or parallelize statements.

Control dependencies

Control dependency is a situation in which a program instruction executes if the previous instruction evaluates in a way that allows its execution.

A statement S2 is control dependent on S1 (written ${\displaystyle S1\ \delta ^{c}\ S2}$) if and only if S2's execution is conditionally guarded by S1. S2 is control dependent on S1 if and only if ${\displaystyle S1\in PDF(S2)}$ where ${\displaystyle PDF(S)}$ is the post dominance frontier of statement ${\displaystyle S}$. The following is an example of such a control dependence:

S1       if x > 2 goto L1
S2       y := 3   
S3   L1: z := y + 1

Here, S2 only runs if the predicate in S1 is false.

Data dependencies

A data dependence arises from two statements which access or modify the same resource.

Flow(True) dependence

A statement S2 is flow dependent on S1 (written ${\displaystyle S1\ \delta ^{f}\ S2}$) if and only if S1 modifies a resource that S2 reads and S1 precedes S2 in execution. The following is an example of a flow dependence (RAW: Read After Write):

S1       x := 10
S2       y := x + c

Antidependence

A statement S2 is antidependent on S1 (written ${\displaystyle S1\ \delta ^{a}\ S2}$) if and only if S2 modifies a resource that S1 reads and S1 precedes S2 in execution. The following is an example of an antidependence (WAR: Write After Read):

S1       x := y + c
S2       y := 10

Here, S2 sets the value of y but S1 reads a prior value of y.

Output dependence

A statement S2 is output dependent on S1 (written ${\displaystyle S1\ \delta ^{o}\ S2}$) if and only if S1 and S2 modify the same resource and S1 precedes S2 in execution. The following is an example of an output dependence (WAW: Write After Write):

S1       x := 10
S2       x := 20

Here, S2 and S1 both set the variable x.

Input dependence

A statement S2 is input dependent on S1 (written ${\displaystyle S1\ \delta ^{i}\ S2}$) if and only if S1 and S2 read the same resource and S1 precedes S2 in execution. The following is an example of an input dependence (RAR: Read-After-Read):

S1       y := x + 3
S2       z := x + 5

Here, S2 and S1 both access the variable x. This dependence does not prohibit reordering.

Loop dependencies

The problem of computing dependencies within loops, which is a significant and nontrivial problem, is tackled by loop dependence analysis, which extends the dependence framework given here.

See also

• Program analysis (computer science)
• Automatic parallelization
• Automatic vectorization
• Loop dependence analysis
• Frameworks supporting the polyhedral model
• Hazard (computer architecture)
• Program slicing
• Dead code elimination

Further reading

• Cooper, Keith D.; Torczon, Linda. (2005). Engineering a Compiler. Morgan Kaufmann. ISBN 1-55860-698-X.
• Kennedy, Ken; Allen, Randy. (2001). Optimizing Compilers for Modern Architectures: A Dependence-based Approach. Morgan Kaufmann. ISBN 1-55860-286-0.
• Muchnick, Steven S. (1997). Advanced Compiler Design and Implementation. Morgan Kaufmann. ISBN 1-55860-320-4.

• v
• t
• e

Program analysis

Key concepts

• Control-flow graph
• Correctness
• Hyperproperties
• Invariants
• Path explosion
• Polyvariance
• Rice's theorem
• Runtime verification
• Safety and liveness
• Undefined behavior

Semantics

Types	Axiomatic Denotational Categorical semantics Operational Big-step Small-step
Models	Lambda calculus Petri net Process calculus Rewriting system State machine Turing machine

Analyses

Static	Abstract interpretation Alias Control flow kCFA Data-flow Dependence Effect system Escape Model checking Pointer Shape Symbolic execution Termination Type systems Typestate
Dynamic	Data-flow Taint tracking Concolic execution Fuzzing Invariant inference Program slicing Testing

Formal methods

Concepts	Curry–Howard correspondence Loop invariant Refinement Side effect Soundness and completeness Specification Languages Verification
Logics	Hoare Incorrectness Linear Separation Temporal
Data structures	BDD E-graph Hashcons Union-find
Tools	Constraint solvers CHC SAT SMT Lightweight Alloy TLA+ Proof assistants ACL2 Agda Coq F* HOL Light HOL4 Idris Isabelle Isabelle/HOL Lean LEGO Mizar NuPRL PVS Twelf

• Category
• Outline
• Glossary