1. Introduction
2. A Hierarchy of Constants
2.1 A Taxonomy of Constants
2.1.1 Flow Graphs
2.1.2 May- and Must-Constants
2.1.3 Weakened Constant Detection Problems
2.1.4 Classes of Integer Constants
2.2 Known Results
2.3 New Undecidability Results
2.4 New Intractability Results
2.5 Summary
3. Deciding Constants by Effective Weakest Preconditions..
3.1 Presburger and Polynomial Constants
3.2 Presburger-Constant Detection at a Glance
3.3 A Generic Algorithm
3.4 Detection of Presburger Constants
3.5 A Primer on Computable Ideal Theory
3.6 More About Z[x1,...,xn]
3.6.1 Z[X1,...,Xn] as a Complete Lattice
3.6.2 Zeros
3.6.3 Substitution
3.6.4 Projection
3.7 Detection of Polynomial Constants
3.8 Conclusion
4. Limits of Parallel Flow Analysis
4.1 A Motivating Example
4.2 Parallel Programs
4.3 Interprocedural Copy-Constant Detection
4.3.1 Two-Counter Machines
4.3.2 Constructing a Program
4.3.3 Correctness of the Reduction
4.4 Intraprocedural Copy-Constant Detection
4.5 Copy-Constant Detection in Loop-Free Programs
4.6 Beyond Fork/Join Parallelism
4.7 Owicki/Gries-Style Program Proofs
4.8 Correctness of the Reduction in Section 4.3
4.8.1 Enriching the Program
4.8.2 The Proof Outlines
4.8.3 Interference Freedom
4.9 Correctness of the Reduction in Section 4.4
4.9.1 Enriching the Program
4.9.2 An Auxiliary Predicate
4.9.3 Proof Outline for 7r0
4.9.4 Proof Outline for 7ri(r)
4.9.5 Proof Outline for Main
4.9.6 Interference Freedom
4.10 Conclusion
5. Parallel Flow Graphs
5.1 Parallel Flow Graphs
5.2 Operational Semantics
5.3 Atomic Runs
5.4 The Run Sets of Ultimate Interest
5.5 The Constraint Systems
5.5.1 Same-Level Runs
5.5.2 Inverse Same-Level Runs
5.5.3 Two Assumptions and a Simple Analysis
5.5.4 Reaching Runs
5.5.5 Terminating Runs
5.5.6 Bridging Runs
5.5.7 The General Case
5.6 Discussion
6. Non-atomic Execution
6.1 Modeling Non-atomic Execution by Virtual Variables ...
6.2 A Motivating Example
6.3 The Domain of Non-atomic Run Sets
6.3.1 Base Statements
6.3.2 Sequential Composition
6.3.3 Interleaving Operator
6.3.4 Pre-operator
6.3.5 Post-operator
6.4 Conclusion
……
7. Dependence Traces
8. Detecting Copy Constants and Eliminating Faint Code
9. Complexity in the Non-atomic Scenario
10. Conclusion
A. A Primer on Constraint-Based Program Analysis
References
鄂公网安备 42010302001612号 