search

mc-imperial / spirv-control-flow

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

(Un)structured control-flow #41

Open vili-1 opened 2 years ago

vili-1 commented 2 years ago

The graph below is deemed feasible by our Alloy model. However, the divergent branches (at b1) represent unstructured control-flow.

So, to reject this example (as an unstructured one), on top of the predicates about the out degree of the header blocks, we add the below constraints:

/* If non-header block 'b' has multiple successors then (at least) one of the following must hold:

  1. 'b' must be a break block
  2. 'b' must be a continue block

*/

multiple_edges

pred sampleCFG1 {
  some disj b0, b1, b2, b3, b4: Block {
    EntryPoint = b0
    HeaderBlock = none
    LoopHeader = none
    SwitchBlock = none
    jump = (b0 -> (0 -> b1))
    + (b1 -> ((0 -> b2) + (1 -> b3)))
    + (b2 -> (0 -> b4))
    + (b3 -> (0 -> b4) )
    no merge 
    no continue
  }
}
run { sampleCFG1 && allFacts } for 5 Block
vili-1 commented 2 years ago

The rule above is further refined in mc-imperial/spirv-control-flow#36

afd commented 2 years ago

@vili-1 We added this rule to our model, but I am not sure this change made it back to the spec. I'm going to label this with "future work" so that we can revisit it. But let's not discuss it in the paper.