mc-imperial / spirv-control-flow

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

SwiftShader: Infinite Loop #8

Open Jack-Clark opened 2 years ago

Jack-Clark commented 2 years ago

Executing amber -t spv1.3 -v 1.1 reduced-infinite-loop.amber hangs presumably due to an infinite loop. I can reproduce this on master (commit d15c42482).

Here is the reduced amber code:

#!amber

SHADER compute compute_shader SPIRV-ASM

; Follow the path:
; <8> -> edge_2 -> <9> -> <15> -> 12
;
; 3 CFG nodes have OpBranchConditional or OpSwitch as their terminators (denoted <n>): 8, 9 and 15.
;
; To follow this path, we need to make these decisions each time we reach 8, 9 or 15.
; This path was generated with the seed 408688807413651389 and has length 4.
;
; We equip the shader with 3+1 storage buffers:
; - An input storage buffer with the directions for each node 8, 9 or 15
; - An output storage buffer that records the blocks that are executed

; SPIR-V
; Version: 1.3
; Generator: Khronos Glslang Reference Front End; 8
; Bound: 15
; Schema: 0

               OpCapability Shader
               OpMemoryModel Logical GLSL450
               OpEntryPoint GLCompute %7 "main"
               OpExecutionMode %7 LocalSize 1 1 1

               OpDecorate %size_1_struct_type BufferBlock
               OpMemberDecorate %size_1_struct_type 0 Offset 0
               OpDecorate %size_1_array_type ArrayStride 4

               OpDecorate %output_struct_type BufferBlock
               OpMemberDecorate %output_struct_type 0 Offset 0
               OpDecorate %output_array_type ArrayStride 4

               OpDecorate %directions_8_variable DescriptorSet 0
               OpDecorate %directions_8_variable Binding 0

               OpDecorate %directions_9_variable DescriptorSet 0
               OpDecorate %directions_9_variable Binding 1

               OpDecorate %output_variable DescriptorSet 0
               OpDecorate %output_variable Binding 3

          %1 = OpTypeVoid
          %2 = OpTypeFunction %1
          %3 = OpTypeBool
          %4 = OpTypeInt 32 0
          %5 = OpConstantTrue %3
          %6 = OpConstant %4 0

               %constant_0 = OpConstant %4 0
               %constant_1 = OpConstant %4 1
               %constant_2 = OpConstant %4 2
               %constant_8 = OpConstant %4 8

               %size_1_array_type = OpTypeArray %4 %constant_1
               %size_1_struct_type = OpTypeStruct %size_1_array_type
               %size_1_pointer_type = OpTypePointer Uniform %size_1_struct_type
               %directions_8_variable = OpVariable %size_1_pointer_type Uniform
               %directions_9_variable = OpVariable %size_1_pointer_type Uniform

               %output_array_type = OpTypeArray %4 %constant_2
               %output_struct_type = OpTypeStruct %output_array_type
               %output_pointer_type = OpTypePointer Uniform %output_struct_type
               %output_variable = OpVariable %output_pointer_type Uniform

               ; Pointer type for declaring local variables of int type
               %local_int_ptr = OpTypePointer Function %4

               ; Pointer type for integer data in a storage buffer
               %storage_buffer_int_ptr = OpTypePointer Uniform %4

          %7 = OpFunction %1 None %2

          %8 = OpLabel ; validCFG/SelectionHeader$1
               %output_index = OpVariable %local_int_ptr Function %constant_0
               %directions_8_index = OpVariable %local_int_ptr Function %constant_0
               %directions_9_index = OpVariable %local_int_ptr Function %constant_0

   %temp_8_0 = OpLoad %4 %output_index
   %temp_8_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_8_0
               OpStore %temp_8_1 %constant_8
   %temp_8_2 = OpIAdd %4 %temp_8_0 %constant_1
               OpStore %output_index %temp_8_2
   %temp_8_3 = OpLoad %4 %directions_8_index
   %temp_8_4 = OpAccessChain %storage_buffer_int_ptr %directions_8_variable %constant_0 %temp_8_3
   %temp_8_5 = OpLoad %4 %temp_8_4
   %temp_8_7 = OpIAdd %4 %temp_8_3 %constant_1
               OpStore %directions_8_index %temp_8_7
               OpSelectionMerge %9 None
               OpSwitch %temp_8_5 %10 1 %11 2 %9

         %10 = OpLabel ; validCFG/Block$0
               OpReturn

         %11 = OpLabel ; validCFG/StructurallyReachableBlock$4
               OpReturn

          %9 = OpLabel ; validCFG/LoopHeader$0
   %temp_9_3 = OpLoad %4 %directions_9_index
   %temp_9_4 = OpAccessChain %storage_buffer_int_ptr %directions_9_variable %constant_0 %temp_9_3
   %temp_9_5 = OpLoad %4 %temp_9_4
   %temp_9_6 = OpIEqual %3 %temp_9_5 %constant_1
   %temp_9_7 = OpIAdd %4 %temp_9_3 %constant_1
               OpStore %directions_9_index %temp_9_7
               OpLoopMerge %12 %13 None
               OpBranchConditional %temp_9_6 %14 %15

         %15 = OpLabel ; validCFG/SelectionHeader$0
               OpSelectionMerge %16 None
               OpBranchConditional %5 %12 %17

         %17 = OpLabel ; validCFG/StructurallyReachableBlock$3
               OpBranchConditional %5 %12 %13

         %16 = OpLabel ; validCFG/StructurallyReachableBlock$2
               OpBranch %14

         %12 = OpLabel ; validCFG/StructurallyReachableBlock$1
               OpReturn

         %13 = OpLabel ; validCFG/StructurallyReachableBlock$0
               OpBranch %9

         %14 = OpLabel ; validCFG/StructurallyReachableBlock$5
               OpReturn

               OpFunctionEnd

 END

 BUFFER directions_8 DATA_TYPE uint32 STD430 DATA 2 END
 BUFFER directions_9 DATA_TYPE uint32 STD430 DATA 0 END

 BUFFER output DATA_TYPE uint32 STD430 SIZE 4 FILL 0

 PIPELINE compute pipeline
   ATTACH compute_shader

   BIND BUFFER directions_8 AS storage DESCRIPTOR_SET 0 BINDING 0
   BIND BUFFER directions_9 AS storage DESCRIPTOR_SET 0 BINDING 1

   BIND BUFFER output AS storage DESCRIPTOR_SET 0 BINDING 3
 END

 RUN pipeline 1 1 1

 EXPECT directions_8 IDX 0 EQ 2
 EXPECT directions_9 IDX 0 EQ 0
 EXPECT output IDX 0 EQ 8 9

I can't get rid of the input load and output store in SH0 or the input load in LH0.

@vili-1 validCFG/Block$0 looks structurally reachable to me. Do you think this is related to the issue mentioned previously?

vili-1 commented 2 years ago

@Jack-Clark, below I've attached the graph: all blocks are structurally reachable.

Executing the fleshed, I get this:

jajck2.amber: Line 162: Verifier failed: 0 == 9, at index 1

Summary of Failures:
   jajck2.amber

Summary: 0 pass, 1 fail

In the last line of the amber file, I would have expected to see something like EXPECT output IDX 0 EQ 8 9 15 12 (the last node in the path should be terminal) - can you check this?

jajck2

vili-1 commented 2 years ago

The error is very strange: it says that instead of 9 it should be 0 in the last line. And if you replace the last line with: EXPECT output IDX 0 EQ 8 0 0 (instead of EXPECT output IDX 0 EQ 8 9 14) then no error is returned!! Will keep thinking on it..

In any case, I haven't experienced hangs as you have.

#!amber

SHADER compute compute_shader SPIRV-ASM

; SPIR-V
; Version: 1.3
; Generator: Khronos Glslang Reference Front End; 8
; Bound: 15
; Schema: 0

; Follow the path:
; <8> -> <9> -> 14
;
; 2 CFG nodes have OpBranchConditional or OpSwitch as their terminators (denoted <n>): 8 and 9.
;
; To follow this path, we need to make these decisions each time we reach 8 or 9.
;
; We equip the shader with 2+1 storage buffers:
; - An input storage buffer with the directions for each node 8 or 9
; - An output storage buffer that records the blocks that are executed

               OpCapability Shader
               OpMemoryModel Logical GLSL450
               OpEntryPoint GLCompute %7 "main"
               OpExecutionMode %7 LocalSize 1 1 1

               ; Below, we declare various types and variables for storage buffers.
               ; These decorations tell SPIR-V that the types and variables relate to storage buffers

               OpDecorate %size_1_struct_type BufferBlock
               OpMemberDecorate %size_1_struct_type 0 Offset 0
               OpDecorate %size_1_array_type ArrayStride 4

               OpDecorate %output_struct_type BufferBlock
               OpMemberDecorate %output_struct_type 0 Offset 0
               OpDecorate %output_array_type ArrayStride 4

               OpDecorate %directions_8_variable DescriptorSet 0
               OpDecorate %directions_8_variable Binding 0

               OpDecorate %directions_9_variable DescriptorSet 0
               OpDecorate %directions_9_variable Binding 1

               OpDecorate %output_variable DescriptorSet 0
               OpDecorate %output_variable Binding 2

          %1 = OpTypeVoid
          %2 = OpTypeFunction %1
          %3 = OpTypeBool
          %4 = OpTypeInt 32 0
          %5 = OpConstantTrue %3
          %6 = OpConstant %4 0

               %constant_0 = OpConstant %4 0
               %constant_1 = OpConstant %4 1
               %constant_3 = OpConstant %4 3
               %constant_8 = OpConstant %4 8
               %constant_9 = OpConstant %4 9
               %constant_10 = OpConstant %4 10
               %constant_11 = OpConstant %4 11
               %constant_12 = OpConstant %4 12
               %constant_13 = OpConstant %4 13
               %constant_14 = OpConstant %4 14
               %constant_15 = OpConstant %4 15
               %constant_16 = OpConstant %4 16
               %constant_17 = OpConstant %4 17

               ; Declaration of storage buffers for the 2 directions and the output

               %size_1_array_type = OpTypeArray %4 %constant_1
               %size_1_struct_type = OpTypeStruct %size_1_array_type
               %size_1_pointer_type = OpTypePointer Uniform %size_1_struct_type
               %directions_8_variable = OpVariable %size_1_pointer_type Uniform
               %directions_9_variable = OpVariable %size_1_pointer_type Uniform

               %output_array_type = OpTypeArray %4 %constant_3
               %output_struct_type = OpTypeStruct %output_array_type
               %output_pointer_type = OpTypePointer Uniform %output_struct_type
               %output_variable = OpVariable %output_pointer_type Uniform

               ; Pointer type for declaring local variables of int type
               %local_int_ptr = OpTypePointer Function %4

               ; Pointer type for integer data in a storage buffer
               %storage_buffer_int_ptr = OpTypePointer Uniform %4

          %7 = OpFunction %1 None %2

          %8 = OpLabel ; validCFG/SelectionHeader$1
               %output_index = OpVariable %local_int_ptr Function %constant_0
               %directions_8_index = OpVariable %local_int_ptr Function %constant_0
               %directions_9_index = OpVariable %local_int_ptr Function %constant_0

   %temp_8_0 = OpLoad %4 %output_index
   %temp_8_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_8_0
               OpStore %temp_8_1 %constant_8
   %temp_8_2 = OpIAdd %4 %temp_8_0 %constant_1
               OpStore %output_index %temp_8_2
   %temp_8_3 = OpLoad %4 %directions_8_index
   %temp_8_4 = OpAccessChain %storage_buffer_int_ptr %directions_8_variable %constant_0 %temp_8_3
   %temp_8_5 = OpLoad %4 %temp_8_4
   %temp_8_7 = OpIAdd %4 %temp_8_3 %constant_1
               OpStore %directions_8_index %temp_8_7
               OpSelectionMerge %9 None
               OpSwitch %temp_8_5 %10 1 %11 2 %9

         %10 = OpLabel ; validCFG/StructurallyReachableBlock$5
               OpReturn

         %11 = OpLabel ; validCFG/StructurallyReachableBlock$4
               OpReturn

          %9 = OpLabel ; validCFG/LoopHeader$0
   %temp_9_0 = OpLoad %4 %output_index
   %temp_9_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_9_0
               OpStore %temp_9_1 %constant_9
   %temp_9_2 = OpIAdd %4 %temp_9_0 %constant_1
               OpStore %output_index %temp_9_2
   %temp_9_3 = OpLoad %4 %directions_9_index
   %temp_9_4 = OpAccessChain %storage_buffer_int_ptr %directions_9_variable %constant_0 %temp_9_3
   %temp_9_5 = OpLoad %4 %temp_9_4
   %temp_9_6 = OpIEqual %3 %temp_9_5 %constant_1
   %temp_9_7 = OpIAdd %4 %temp_9_3 %constant_1
               OpStore %directions_9_index %temp_9_7
               OpLoopMerge %12 %13 None
               OpBranchConditional %temp_9_6 %14 %15

         %15 = OpLabel ; validCFG/SelectionHeader$0
               OpSelectionMerge %16 None
               OpBranchConditional %5 %12 %17

         %17 = OpLabel ; validCFG/StructurallyReachableBlock$3
               OpBranchConditional %5 %12 %13

         %16 = OpLabel ; validCFG/StructurallyReachableBlock$2
               OpBranch %14

         %12 = OpLabel ; validCFG/StructurallyReachableBlock$1
               OpReturn

         %13 = OpLabel ; validCFG/StructurallyReachableBlock$0
               OpBranch %9

         %14 = OpLabel ; validCFG/StructurallyReachableBlock$6
  %temp_14_0 = OpLoad %4 %output_index
  %temp_14_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_14_0
               OpStore %temp_14_1 %constant_14
  %temp_14_2 = OpIAdd %4 %temp_14_0 %constant_1
               OpStore %output_index %temp_14_2
               OpReturn

               OpFunctionEnd

 END

 BUFFER directions_8 DATA_TYPE uint32 STD430 DATA 2 END
 BUFFER directions_9 DATA_TYPE uint32 STD430 DATA 1 END

 BUFFER output DATA_TYPE uint32 STD430 SIZE 3 FILL 0

 PIPELINE compute pipeline
   ATTACH compute_shader

   BIND BUFFER directions_8 AS storage DESCRIPTOR_SET 0 BINDING 0
   BIND BUFFER directions_9 AS storage DESCRIPTOR_SET 0 BINDING 1

   BIND BUFFER output AS storage DESCRIPTOR_SET 0 BINDING 2
 END

 RUN pipeline 1 1 1

 EXPECT directions_8 IDX 0 EQ 2
 EXPECT directions_9 IDX 0 EQ 1
 EXPECT output IDX 0 EQ 8 9 14
vili-1 commented 2 years ago

Well, @Jack-Clark, what I discovered is that: if the node in the fleshing path happens to be a switch case and merge block of the swich simultaneously and furthermore the switch is the first node of the path, then we get the error. I proved this by changing the merge block to 11, then 8->11 would trigger the error. Also in #7 where the switch 14 can't be the first node of the path, no error is triggered when switch->switch.merge is in the path. @afd, I'm afraid there is something that hasn't been considered in our program to cover this case. Can you take a look when you have the time?

PS. This holds for #9, too.

Jack-Clark commented 2 years ago

@vili-1 thanks for digging into this.

In the last line of the amber file, I would have expected to see something like EXPECT output IDX 0 EQ 8 9 15 12 (the last node in the path should be terminal) - can you check this?

I reduced the amber code to remove the output related code in some of the blocks to make a simpler bug report, so I have also removed the corresponding block ids in the EXPECT statement. I can post the full amber code if you want?

The error is very strange: it says that instead of 9 it should be 0 in the last line. And if you replace the last line with: EXPECT output IDX 0 EQ 8 0 0 (instead of EXPECT output IDX 0 EQ 8 9 14) then no error is returned!! Will keep thinking on it. In any case, I haven't experienced hangs as you have.

One thing I have noticed is that the flesher will not add output related instructions to the blocks that are not on the path, so it could be the case that the path is actually 8->10 or 8->11 but this would still be recorded as 8 0 in the output buffer (to detect this you can try changing the initialisation of the output array to have a different value). These different paths could be taken due to the compiler making some assumption about being able to avoid going into the loop starting at 9. The hanging issue may be related to the SwiftShader driver specifically, but it is interesting that you have had some issues on moltenVK.

Well, @Jack-Clark, what I discovered is that: if the node in the fleshing path happens to be a switch case and merge block of the swich simultaneously and furthermore the switch is the first node of the path, then we get the error...@afd, I'm afraid there is something that hasn't been considered in our program to cover this case. Can you take a look when you have the time?

Just to be clear, are you concerned that this pattern might make the CFG invalid? Otherwise, is it not the case that the bugs are errors in the driver implementation? I'll report the output mismatch (#10) to SwiftShader because it is not related to the pattern. For the segfault (#9), do you know if the driver is allowed to segfault if the spirv is invalid?

vili-1 commented 2 years ago

I loaded the SwiftShader in my Mac and now I get no error; just the two warnings below. Very interesting!

../src/Vulkan/libVulkan.cpp:2821 WARNING: pFeatures->pNext sType = 1000082000
../src/Vulkan/libVulkan.cpp:2821 WARNING: pFeatures->pNext sType = 1000225002
vili-1 commented 2 years ago

@Jack-Clark I took another look at this issue and I realised that there is no issue with MoltenVK - I was mislead by some issue about the environmental variables used to swap between drivers not passed correctly to the python shell. But I do get the hanging issue with SwiftShader LLVM10.0, and this happens only for paths with prefix 8->9