Open Jack-Clark opened 2 years ago
From a quick look, the CFG you have sketched looks valid. I don't have time to dig properly before going for holiday. @vili-1 it would be great if you could do a review of the Amber before @Jack-Clark files an issue to Mesa. And also the issue of a block that's structurally reachable but is named as if it were wholly unreachable would be worth getting to the bottom of. Thanks!
It seems this bug could be the same as the one filed here. I've added a comment with the reduced example as the original example provided is ~180 lines of spirv whereas the reduced example is about ~30 lines (w/o new lines).
@Jack-Clark, in our model we have the set StructurallyReachableBlock
which is a sub-type of Block
, where Block is the set of all blocks, totally-unreachable inclusive). So, using Block$X
naming doesn't necessarily mean that it is a totally unreachable block. I guess you are referring to block 13 in the graph below as a "totally-reachable". As you see all blocks here are reachable, i.e., StructurallyReachableBlock == Block
. What is that differentiates block 13 from others in your understanding?
The graph is valid, by the way.
Now, about the error you get running amber, I do get an error, too. I have to dig into this a bit.
[mvk-error] VK_ERROR_DEVICE_LOST: Command buffer 0x7fe1ddb04fe0 "" execution failed (code 12): GPU Command Buffer execution stopped due to Stack Overflow Exception. Please check the [MTLComputePipelineDescriptor maxCallStackDepth] setting. (00000011:kIOAccelCommandBufferCallbackErrorStackOverflow)
jack1.amber: Vulkan::Calling vkWaitForFences Fail
Summary of Failures:
jack1.amber
Summary: 0 pass, 1 fail
I'm attaching the xml so let's refer to the naming used in it for further discussion on this issue.
@vili-1 I am familiar with the terms structurally reachable and wholly unreachable as defined in the structured control flow doc, but I'm not sure what totally reachable and totally unreachable mean - are they equivalent? Also bear in mind I'm not familiar with the Alloy model or Alloy itself.
My expectation was that all structurally reachable blocks would be of type StructurallyReachableBlock
or one of its subtypes (if it has any) and that any other blocks that are not a subtype of StructurallyReachableBlock
would be wholly unreachable. From your answer it sounds like this is not the case. This is what caused my confusion regarding block 13 as it had type Block
rather than StructurallyReachableBlock
, yet it was structurally reachable.
Ah, yes - you are right - "wholly (un)reachable" is the correct term.
In the xml that I attached today, all blocks are of type StructurallyReachableBlock
. Maybe the confusion is because we changed the names in the model: what is now StructurallyReachableBlock
/Block
was before Block
/BLOCK
. If there's still confusion please don't hesitate to ask.
@Jack-Clark can you please send me the amber file that you are getting the error from. Just realised that the one you posted above is not a proper fleshed one (hence the Stack Overflow Exception I got).
I used my original fleshing program to flesh this example. Executing the amber is always successful in my Mac.
@vili-1 I can try to dig out the original amber file if you still want to take a look? I think what may have happened is that I had regenerated all of the XML files, but not removed the old amber files from the directory, so there will be a mix of old and new amber files. This won't affect correctness, but is a little confusing on the naming front. I'll be sure to only have amber files with the new naming in future folders.
No worries @Jack-Clark, I fleshed it using my original program, so no need to send it.
I get no error with SwiftShader either.
@vili-1 thanks for confirming. I get an error with MESA only. Both the SwiftShader and Nvidia drivers successfully execute this example when I tested.
Running the following command using branch 22.0.1 and master (commit cde1be0b) of Mesa:
gives:
This is potentially related to this bug. A patch was eventually merged for that bug so this is still valid. I think the discussion of the bug highlights the value in the formal modelling of the control flow rules.
I've compiled and validated the reduced asm from the following amber code:
I've removed many blocks from the original CFG, so it would be good if someone (@afd @vili-1 @johnwickerson) could double check this before I submit it as a bug.
There is something in the original CFG file that caught my eye, but doesn't affect the bug, however could indicate an error in some part of our code. There is a block B0 which is labelled as wholly unreachable (i.e. uses
Block$X
naming), but looks structurally reachable to me because of the pathSRB6->LH0->B0
. Am I missing something? I've drawn out the CFG below. NoteSRBX = StructurallyReachableBlock$X and BX = Block$X
.Here is the skeleton asm: