A data flow analysis algorithm for computing dominators

Nan Jiang

September 5, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This entry formalises the fast iterative algorithm for computing dominators due to Cooper, Harvey and Kennedy. It gives a specification of computing dominators on a control flow graph where each node refers to its reverse post order number. A semilattice of reversed-ordered list which represents dominators is built and a Kildall-style algorithm on the semilattice is defined for computing dominators. Finally the soundness and completeness of the algorithm are proved w.r.t. the specification.

License

BSD License

Topics

Session Dominance_CHK

Depends on

Cite

× 
@article{Dominance_CHK-AFP,
  author  = {Nan Jiang},
  title   = {A data flow analysis algorithm for computing dominators},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2021},
  note    = {\url{https://isa-afp.org/entries/Dominance_CHK.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: