OpSwitch: Target must be alternating scalar integer literals

[vili-1]

I got the example below generated by Alloy (as a valid one) but the validator complains about the following constraint:

/**
  *  "...if Target T1 branches to Target T2, or if Target T1 branches to the Default
  *   and the Default branches to Target T2, then T1 must immediately precede T2
  *   in the list of the OpSwitch Target operands"
  */

Working this out, I was looking whether there is somewhere in the specs stated somehow any constraint about the number of parallel edges (incident to the same pair)? @afd what does the following mean exactly (from the OpSwitch)?

"Target must be alternating scalar integer literals.."

cfg_2.zip

[afd]

@vili-1 Let me answer your questions in two parts.

First: "Target must be alternating scalar integer literals and the of a label" means that the "Target" part of the instruction must look something like:

1 %12 3 %4 6 %9

i.e., an integer literal (1 in my example), followed by a label id (%12 in my example), then another integer (3 here), then another label (%4 here), etc.

This reflects what a switch statement is like in C, or in GLSL. You do:

switch(some_expr) {
  case literal_1:
     // code fragment 1
  case literal_2:
     // code fragment 2
   etc.
}

Here literal_1, literal_2, etc., correspond to the integer literals in "Target", while the ids of labels correspond to the code fragments.

Second: There is no limit to how many "parallel" edges there can be between two blocks.

At a first look I thought your example was invalid due to violating this part of the spec:

"if Target T1 branches to Target T2, or if Target T1 branches to the Default and the Default branches to Target T2, then T1 must immediately precede T2 in the list of the OpSwitch Target operands"

But on closer inspection I am not so sure! I will think about it further.

[afd]

Here's a simpler example that the validator thinks is invalid:

[afd]

And here are the files:

cfg_2b.zip

[afd]

The offending instruction is:

OpSwitch %6 %11 19 %12 7 %11

The validator does not like the fact that 7 %11 comes after 19 %12. I think this is because %11 branches to %12.

Indeed, I think this is disallowed by: "if Target T1 branches to Target T2, or if Target T1 branches to the Default and the Default branches to Target T2, then T1 must immediately precede T2 in the list of the OpSwitch Target operands"

My thinking is: the targets are %12 and %11, and we have that %11 branches to %12, but there is an occurence of %11 does not immediately precede %12 in the list of targets.

It is a little ambiguous, though - the spec doesn't say anything about what the rules are if a target label appears many times in the sequence.

What do you think, @vili-1 ?

[vili-1]

About the offending instruction

OpSwitch %6 %11 19 %12 7 %11

one of the edges 9->11 does immediately precede the edge 9->12 which means that the rule, as it is stated, should absolutely be satisfied for this example. It seems like the validator uses some greedy search algorithm and if an edge 9->11 (out of many) is found to succeed 9->12 then it 'believes' that doesn't precede..

[afd]

In this example the first occurrence of %11 is not a "Target": it is the "Default".

From OpSwitch the format of the instruction is:

OpSwitch Selector Default [Literal Label]*

In the above example the selector is %6, the Default is %11, and then we have 9 %12 and 7 %11 as the targets. So by this reading, %11 does not precede %12 in the list of targets.

So I'd argue that the example is invalid.

However, your analysis made me think of a couple of problems with the spec. Please see 1.asm and 2.asm in the attached archive:

examples.zip

In 1.asm we have:

               OpSwitch %7 %20 1 %10 2 %10 3 %11

and we have that %10 branches to %11. Now, %10 appears twice in the targets list, and clearly the first occurrence of %10 does not precede %11.

I think the language in the spec should be tightened up to take account of the fact that duplicate targets are allowed (it's very common to have many case targets targeting the same block of code in a switch statement in a high level language, so this is a real thing).

In 2.asm, we have:

               OpSwitch %7 %20 1 %10 3 %11 2 %10

Again, %10 branches to %11.

Here, I think the spec is ambiguous: one occurrence of %10 immediately precedes an occurrence of %11, but then there's another occurrence of %10 that does not.

I think the spec should be re-written like this:

"if Target T1 branches to Target T2, or if Target T1 branches to the Default and the Default branches to Target T2, then every occurrence of T1 must immediately precede an occurrence of T1 or T2 in the list of the OpSwitch Target operands"

This would allow duplicate targets: if the target sequence (ignoring literals and just focusing on labels) is "T1 T1 T1 T1 T2" (and assuming that T1 branches to T2) then this is OK, because the first three T1s each prcede a T1, and the final T1 precedes a T2. And it would disallow "T1 T2 T1", because the second occurrence of T1 does not precede a T2.

What do you think? Shall we open a spec issue for this?

[vili-1]

For the example cfg_2b, you are right - the example is invalid - I found a bug in the model's rule: it was considering the default as target.

For the two last examples, I totally agree with your thoughts and with the redefinition of the rule.

[afd]

Cool - would you be happy to create a SPIR-V specification issue, explaining the problems with the current wording and proposing some new wording? We can discuss it with the working group via the Khronos issue that you create, and then if they're amenable to the change we can do a merge request to have the spec updated.

You would make the issue in Khronos GitLab - do let me know if you need any help.

[vili-1]

Absolutely, I will.

[vili-1]

The attached example is from the CTS - I’m running again the updated Alloy model against all CTS: isn’t this case invalid with respect to the rule in question?

https://github.com/KhronosGroup/VK-GL-CTS/blob/master/external/vulkancts/data/vulkan/amber/spirv_assembly/instruction/compute/switch/switch-case-to-merge-block.amber

[vili-1]

@afd related to 2.asm (your example) above, I've added another edge (5->11 in green): then the new proposed rule can be further generalised as:

"if Target T1 branches to Target T2, or if Target T1 branches to the Default and the Default branches to Target T2, then T1 (or the substring - i.e., the consecutive run - of occurrences of T1 in case of multiple occurrences of T1 ) must immediately precede T2 (or the substring of occurrences of T2 in case of multiple occurrences of T2) in the list of the OpSwitch Target operands"

What do you think?

[vili-1]

The attached example is from the CTS - I’m running again the updated Alloy model against all CTS: isn’t this case invalid with respect to the rule in question?

https://github.com/KhronosGroup/VK-GL-CTS/blob/master/external/vulkancts/data/vulkan/amber/spirv_assembly/instruction/compute/switch/switch-case-to-merge-block.amber

---

This example is a bit special because %mergeLabel is the merge block for the switch, and each of %val1Label, %val2Label and %val3Label's case constructs branch to %mergeLabel.

Now, when the spec defines a case construct, it does say that a case construct is only defined for targets that are different from the merge block for the switch:

a case construct: the blocks dominated by an OpSwitch Target or Default (this construct is only defined for those OpSwitch Target or Default that are not equal to the OpSwitch’s corresponding merge block)

So perhaps there is an implicit intention that the rule:

if Target T1 branches to Target T2, or if Target T1 branches to the Default and the Default branches to Target T2, then T1 must immediately precede T2 in the list of the OpSwitch Target operands

only applies when T2 is not the merge block.

But this is certainly not at all clear from the spec if it is indeed what was intended.

I'll open a new Khronos issue to raise this point.

[vili-1]

This case from CTS is also not accepted by our model due to the fact that one occurrence b1->b3 does not immediately precede b1->b4. I'm going to introduce the concept of substring in our model as mentioned above.

Same story with this

[vili-1]

The final version of the rule for tightening up to take account of the fact that duplicate targets are allowed, is:

  *
  *  (a) if 'T1' and 'T2' appear as labels of targets in the **OpSwitch**
  *      instruction and the case construct defined by 'T1' branches to
  *      the case construct defined by 'T2' then the last target with label 'T1' 
  *      must immediately precede the first target with label 'T2' in the list of 
  *      *OpSwitch* 'Target' operands
  *
  *  (b) if 'T1' and 'T2' appear as labels of targets in the **OpSwitch**
  *      instruction and the case construct defined by 'T1' branches to the
  *      'Default' case construct of the **OpSwitch** which in turn
  *      branches to the case construct defined by 'T2', then either:
  *
  *      (i)   the block that defines the 'Default' case construct must
  *            appear as a target label in the **OpSwitch** instruction, or
  *      (ii)  the last target with label 'T1' must immediately precede the
  *            first target with label 'T2' in the list of **OpSwitch**
  *           'Target' operands
  *
  *  (c) for any label 'T', all targets with label 'T' must appear consecutively 
  *      in the list of *OpSwitch* 'Target' operands
  *