mc-imperial / spirv-control-flow

Formal modelling of SPIR-V control flow using Alloy
Apache License 2.0
2 stars 0 forks source link

Back-Edges #44

Open vili-1 opened 2 years ago

vili-1 commented 2 years ago

SPIR-V Specs equalises back-edges and retreating edges. It says: “ Back Edge: A branch is a back edge if there is a depth-first search starting at the entry block of the CFG where the branch branches to one of its ancestors. A back-edge block is a block containing such a branch instruction.”

The consensus in the graph theory however is that:

While for every flow graph, every back edge is a retreating, the reverse is, however, not true [1]. And this is crucial because for a flow graph to be reducible, all its retreating edges must be also back edges.

[1] Aho, A. V., Lam, M. S., Sethi, R.,, Ullman, J. D. (2006). Compilers: Principles, Techniques, and Tools 

vili-1 commented 2 years ago

Thinking a bit more about this: as SPIR-V has no control blocks with multiple entries or exits, such as goto, labelled breaks or equivalent statements, then we get always structured control flow graphs. Structured control flow graphs ensure that the CFGs are reducible, in other words, the set of retreating edges is identical to the set of back edges. So, defining backedge as edge whose head is an ancestor of tail (as in SPIR-V specs) is safe. Computationally however, defining backedge as "head dominates tail" is cheaper.