Add comments on sibling and parent properties in dominator trees
git-svn-id: https://llvm.org/svn/llvm-project/llvm/trunk@306913 91177308-0d34-0410-b5e6-96231b3b80d8
Daniel Berlin
3 years ago

316 | 316 | |

317 | 317 | return true; |

318 | 318 | } |

319 | // The below routines verify the correctness of the dominator tree relative to | |

320 | // the CFG it's coming from. A tree is a dominator tree iff it has two | |

321 | // properties, called the parent property and the sibling property. Tarjan | |

322 | // and Lengauer prove (but don't explicitly name) the properties as part of | |

323 | // the proofs in their 1972 paper, but the proofs are mostly part of proving | |

324 | // things about semidominators and idoms, and some of them are simply asserted | |

325 | // based on even earlier papers (see, e.g., lemma 2). Some papers refer to | |

326 | // these properties as "valid" and "co-valid". See, e.g., "Dominators, | |

327 | // directed bipolar orders, and independent spanning trees" by Loukas | |

328 | // Georgiadis and Robert E. Tarjan, as well as "Dominator Tree Verification | |

329 | // and Vertex-Disjoint Paths " by the same authors. | |

330 | ||

331 | // A very simple and direct explanation of these properties can be found in | |

332 | // "An Experimental Study of Dynamic Dominators", found at | |

333 | // https://arxiv.org/abs/1604.02711 | |

334 | ||

335 | // The easiest way to think of the parent property is that it's a requirement | |

336 | // of being a dominator. Let's just take immediate dominators. For PARENT to | |

337 | // be an immediate dominator of CHILD, all paths must go through PARAENT | |

338 | // before they hit CHILD. This implies that if you were to cut PARENT out of | |

339 | // the CFG, there should be no paths to CHILD that are reachable. If there | |

340 | // were, then you now have a path from PARENT to CHILD that goes around PARENT | |

341 | // and still reaches the target node, which by definition, means PARENT can't | |

342 | // be a dominator (let alone an immediate one). | |

343 | ||

344 | // The sibling property is similar. It says that for each pair of sibling | |

345 | // nodes in the dominator tree (LEFT and RIGHT) , they must not dominate each | |

346 | // other. If sibling LEFT dominated sibling RIGHT, it means there are no | |

347 | // paths in the CFG from sibling LEFT to sibling RIGHT that do not go through | |

348 | // LEFT, and thus, LEFT is really an ancestor (in the dominator tree) of | |

349 | // RIGHT, not a sibling. | |

350 | ||

351 | // It is possible to verify the parent and sibling properties in | |

352 | // linear time, but the algorithms are complex. Instead, we do it in a | |

353 | // straightforward N^2 and N^3 way below, using direct path reachability. | |

354 | ||

319 | 355 | |

320 | 356 | // Checks if the tree has the parent property: if for all edges from V to W in |

321 | 357 | // the input graph, such that V is reachable, the parent of W in the tree is |