mc-imperial / spirv-control-flow

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

Consider introducing "structured-dominance" to simplify control flow rules #47

Open afd opened 3 years ago

afd commented 3 years ago

Spec version: Version 1.5, Revision 5, Unified January 7, 2021

The SPIR-V spec says:

a selection construct: includes the blocks dominated by a selection header, while excluding blocks dominated by the selection construct’s merge block”

A problem with this definition is illustrated by this example:

image

If we use the definition to determine the blocks in the selection construct headed at SH, we get: {SH, X, Y, LC, LM}. Intuitively, we want {SH, X, Y}.

Other constructs suffer from similar problems.

The spec accounts for this by saying:

Furthermore, these structured control-flow constructs are additionally defined to exclude all outer constructs' continue constructs and exclude all blocks dominated by all outer constructs' merge blocks.

This is problematic because:

Proposal: structured dominance

We could say that:

A structured-dominates B if every path made up of jump, merge and continue edges from the start of the control flow graph that reaches B goes through A.

In other words, structured-dominance is like dominance, but it also counts the edges that identify merge blocks and the edges that identify continue targets.

Here is the above example but with edges that identify merges and continues also shown:

image

If we changed the rule for selection constructs to:

a selection construct: includes the blocks structured-dominated by a selection header, while excluding blocks [structured-dominated / dominated] by the selection construct’s merge block

(not sure whether we want structured-dominated or just dominated in the second occurrence)

then for this example, at least, things would work out nicely: SH dominates LC and LM, but it does not structured-dominate them. In more detail: SH dominates LC because the only (cycle-free) path of jump edges from the CFG entry to LC is: LH->SH->X->LC, so every path of jump edges from the CFG entry to LC goes through SH. Similarly, the only paths from the entry to LM are: LH->SH->Y->LM and LH->SH->X->SM->LM, so SH dominates LM. However, SH does not structured-dominate LC because of the path: LH->LC (a continue target edge); this does not go through SH. Similarly, SH does not structured-dominate LM because of the path LH->LM (a merge target edge); this does not go through SH.

Perhaps if we defined structured-dominance, and changed the rules for the various constructs to use structured-dominance, things would be less ambiguous and achieve the effect that the language designers intuitively wanted.

Note that I do not propose that we use structured-dominance over dominance throughout. I am only proposing to use it when we are trying to capture notions such as the set of blocks contained in a particular construct. In that case I think it’s rather natural because the merge and continue targets help to clarify the boundary of a construct.