-
Notifications
You must be signed in to change notification settings - Fork 30
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Spir-V frontend #703
Spir-V frontend #703
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Overall comment, whenever you get assumptions (e.g., coming from the specification), document these things because they are no trivial for someone that needs to read the code and might not be an expert on spirv
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java
Outdated
Show resolved
Hide resolved
dartagnan/src/test/java/com/dat3m/dartagnan/spirv/gpuverify/SpirvChecksTest.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ControlBarrier.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/expression/misc/ConstructExpr.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/program/Register.java
Outdated
Show resolved
Hide resolved
} else if (succ instanceof ControlBarrier barrier) { | ||
final Branch succBranch = computeBranchDecomposition(barrier.getSuccessor(), event2BranchMap, branches); | ||
branch.children.add(succBranch); | ||
succBranch.parents.add(branch); | ||
return branch; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I thought of an alternative idea. Usually if we do not terminate, we still jump to the end of the thread.
The new ControlBarriers
changes this fact which requires some updates here and there.
However, we could generate usual branching code like this:
E1: ControlBarrier(<id>)
E2: bool barrierNotExecuted = ExecutionStatus(E1) // Notice this returns TRUE if not executed
E3: if (barrierNotExecuted) goto END_OF_THREAD; ### EARLYTERMINATION
I.e., rather than giving control barriers special branching semantics, we just give them special execution semantics and then use standard branching on the execution semantics via a ExecutionStatus
event.
This code could get fully generated at parsing time with the difference that the if-condition becomes an AbortIf(barrierNotExecuted)
with Tag.EARLYTERMINATION
.
As a consequence no code needs to get modified except the execution encoding of CBs and the stuckness encoding.
EDIT: I believe Tag.EARLYTERMINATION
is misleading: we use it to mean both "nontermination" (spinloops, bound events, and soon control barriers(?)) and "irregular/exceptional termination" (assertion failure in C code).
We should probably split the tag into Tag.NONTERMINATION
and Tag.IRREGULAR_TERMINATION
.
EDIT 2: @hernanponcedeleon FYI, I implemented the above split in the executionModel
branch.
dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/ScopedPointer.java
Show resolved
Hide resolved
...nan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkan.java
Show resolved
Hide resolved
b0cf707
to
029ef16
Compare
Signed-off-by: Hernan Ponce de Leon <[email protected]>
…onfig Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Natalia Gavrilenko <[email protected]>
Co-authored-by: Natalia Gavrilenko <[email protected]>
Co-authored-by: Natalia Gavrilenko <[email protected]>
Co-authored-by: Natalia Gavrilenko <[email protected]>
Co-authored-by: Natalia Gavrilenko <[email protected]>
Co-authored-by: Natalia Gavrilenko <[email protected]>
Co-authored-by: Natalia Gavrilenko <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: haining <[email protected]> Co-authored-by: Thomas Haas <[email protected]>
No description provided.