Add support for OpenCL SPIR-V #792

tonghaining · 2025-01-15T16:00:12Z

No description provided.

ThomasHaas · 2025-01-15T16:12:43Z

Oh, this is a big one, but I immediately have two questions:

(1) What is the purpose of ScopedPointerVariable? It seems to me that in the whole processing pipeline and the final encoding, it is always treated like a simple address/memory object. If so, a processing pass that just eliminates them altogether would be a lot better.

(2) Why does FunctionCall need to remember expressions transformers that are used during Inlining? Is this somehow related to the scoped pointers?

tonghaining · 2025-01-15T20:16:26Z

(1) Thanks for pointing this out! Yes ScopedPointerVariable visitors are not necessary. I think I initially added them while working on accessing function parameters but forgot to remove them afterward. I’ve now removed all of them.

(2) It was not relevant to the scoped pointers. We now have new cases where one test has multiple functions.

ThomasHaas · 2025-01-15T20:29:38Z

(2) It was not relevant to the scoped pointers. We now have new cases where one test has multiple functions

I don't understand this point. C-code also has multiple functions, yet we do not need special transformers when inlining.
What is different for SPIRV/OpenCL code? Do you need to translate pointers to thread_local memory objects or something?

tonghaining · 2025-01-16T15:09:42Z

Yes for pointers inside a function call, we sometimes need to translate them into thread-local/workgroup-local memory objects. Does C-code has similar cases?

ThomasHaas · 2025-01-16T15:25:29Z

Ok, I guessed so. But then you are facing a different issue.
In C-code, we first do inlining and then create the threads, so the thread creation pass actually resolves/translates thread-local memory accesses.
In your case, I believe the parser already creates threads during parsing time, i.e., before inlining.

I think there are two canonical solutions to this:
(1) Do not create threads during parsing time. Instead, we could mark a function as "entry point" (in C-code this is just main, for litmus-like code it would be each process) and let the thread creation pass generate the threads. In this case you would actually need to attach GPU-specific scope information already to functions instead of threads.
(2) Let Inlining do its usual job and have an extra pass that resolves/translates thread-local accesses if possible. This translation should not make use of custom expression transformers attached to function calls. If anything, I think the necessary information should be attached to the threads (or even better: be computable from the threads).

natgavrilenko

First part of the review, will continue tomorrow.

dartagnan/src/main/antlr4/SpirvLexer.g4

dartagnan/src/main/antlr4/Spirv.g4

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java

...n/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsAnnotation.java

...an/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsComposite.java

...nan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsConstant.java

...an/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsExtension.java

hernanponcedeleon

I just saw Natalia stated her review too, so some comments might be repeated

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java

dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java

dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java

...an/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsComposite.java

...agnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemory.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Local.java

hernanponcedeleon · 2025-01-16T19:16:04Z

...nan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvOpenCL.java

+    public List<Event> visitSpirvLoad(SpirvLoad e) {
+        String mo = moToOpenCLTag(Tag.Spirv.getMoTag(e.getTags()));
+        Load load = newLoadWithMo(e.getResultRegister(), e.getAddress(), mo);
+        load.setFunction(e.getFunction());


why do spirv events need to propagate the function from the original event?

This should definitely be avoided because it causes inconsistent state: the event thinks it belongs to a function, but it is not inserted into the function yet. Basically this function should never be called directly (maybe we can make it private, not sure though).

For single event they are not useful, but for RMW events which are translated to C11 event sequences, functions are needed for creating dummy registers.

VisitorSpirvVulkan is translated to Vulkan event sequences and those also need to create dummy registers for RMW. Why is this not a problem in that case?

We are also doing it for vulkan https://github.com/hernanponcedeleon/Dat3M/blob/master/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkan.java#L83

hernanponcedeleon · 2025-01-16T19:18:25Z

...nan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvOpenCL.java

+    @Override
+    public List<Event> visitControlBarrier(ControlBarrier e) {
+        Event entryFence = EventFactory.newControlBarrier(e.getName() + "_entry", e.getId());
+        entryFence.addTags(Tag.OpenCL.ENTRY_FENCE, Tag.C11.MO_RELEASE);


I think we discussed about getting rid of this fence tags and treat barriers in OpenCL the same we do for the other languages (IIRC this was only needed for barrier divergence; we can figure out later how to handle that property)

I agree with Hernan that we should treat control barriers in the same way for all models, unless there is a really good reason to do otherwise. But I suggest to merge this commit first and change barriers after that in a separate commit.

If I am not wrong, the Tag.OpenCL.ENTRY_FENCE tag is not used anymore, so we can simply remove it from the Tag class and remove the axiom from the cat file (all this is dead code ATM)

.../src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlow.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Local.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWExtremum.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java

.../src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/Thread.java

...agnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMWExtremumBase.java

...agnan/src/main/java/com/dat3m/dartagnan/program/event/arch/opencl/OpenCLRMWExtremumBase.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/FunctionCall.java

dartagnan/src/main/antlr4/Spirv.g4

dartagnan/src/main/antlr4/SpirvLexer.g4

dartagnan/src/main/antlr4/Spirv.g4

...n/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsAnnotation.java

...an/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsComposite.java

.../src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsControlFlow.java

...an/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsComposite.java

ThomasHaas · 2025-02-14T14:59:17Z

[...] there will be a weird loop with two backward jumps, and I wonder how it is unrolled.

We normalize such loops first:

Only the last backward jump remains (if it is unconditional, otherwise we introduce a new one).
Every other backward jump is transformed to a forward jump that jumps to the last backward jump.

...n/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsConversion.java

hernanponcedeleon · 2025-02-18T07:49:40Z

@tonghaining please rebase and fix the conflicts

...rc/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ProgramBuilder.java

...an/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsComposite.java

...nan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/helpers/HelperTags.java

...an/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/utils/ThreadCreator.java

...nan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsFunction.java

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsType.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java

...nan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvOpenCL.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java

...nan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvOpenCL.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/ThreadGrid.java

dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/ClangSpirvAssertionsTest.java

...src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsFunctionTest.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/ThreadGrid.java

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java

hernanponcedeleon

First pass up to VisitorExtensionOpenClStd

hernanponcedeleon · 2025-02-24T14:24:17Z

...an/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsComposite.java

+            if (!(element instanceof ConstructExpr)) {
+                throw new ParsingException(String.format("Element is not a ConstructExpr at index: %d for: %s", index, id));
+            }


Isn't this the same check as line 29?

Yes, line 29 removed.

hernanponcedeleon · 2025-02-24T19:40:15Z

...nan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvOpenCL.java

+    @Override
+    public List<Event> visitControlBarrier(ControlBarrier e) {
+        Event entryFence = EventFactory.newControlBarrier(e.getName() + "_entry", e.getId());
+        entryFence.addTags(Tag.OpenCL.ENTRY_FENCE, Tag.C11.MO_RELEASE);


If I am not wrong, the Tag.OpenCL.ENTRY_FENCE tag is not used anymore, so we can simply remove it from the Tag class and remove the axiom from the cat file (all this is dead code ATM)

hernanponcedeleon · 2025-02-24T19:45:25Z

...nan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsFunction.java

+    final Map<String, Function> forwardFunctions = new HashMap<>();
+    final Map<String, Set<FunctionCall>> forwardCalls = new HashMap<>();


Why are those 2 not private?

Updated to private.

hernanponcedeleon · 2025-02-24T19:47:52Z

...nan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsFunction.java

+        if (type instanceof ArrayType aType) {
+            Type elementType = HelperTypes.getMemberType(id, aType, List.of(0));
+            return 1 + getFirstElementDepth(id, elementType);
+        } else if (type instanceof AggregateType agType) {
+            Type elementType = HelperTypes.getMemberType(id, agType, List.of(0));
+            return 1 + getFirstElementDepth(id, elementType);
+        }


Can we merge the two bodies or would the type checker complain about getMemberType?

hernanponcedeleon · 2025-02-24T20:03:23Z

...nan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsFunction.java

+        return 0;
+    }
+
+    private void createExternalVariable(String id, Type type) {


I cannot really follow what is going on with createExternalVariable, addExternalValue, createPointedExternalValue, addExternalParameterLocalEvent and addParameterRegisters. Why do we need all this?

They are used to create external variables which entry function pointers may point to (which are not declared by OpVariable as our earlier tests).
I update their name as:

createExternalVariable -> createParameterVariable
addExternalValue -> addParameterVariable
createPointedExternalValue -> createExternalVariable
addExternalParameterLocalEvent -> addEntryParameterLocalEvent

Would it be better as this?

hernanponcedeleon · 2025-02-24T20:22:46Z

...rc/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ProgramBuilder.java

@@ -191,8 +210,9 @@ public String getPointerStorageClass(String id) {

    public Register addRegister(String id, String typeId) {
        Type type = getType(typeId);
-        if (type instanceof ScopedPointerType) {
-            throw new ParsingException("Register cannot be a pointer");
+        // TODO: Remove this check when tuple registers are supported


Tuple registers are supported, it is just that we do not create single memory events for them.

Comment updated

hernanponcedeleon · 2025-02-25T08:48:25Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java

+    public void updateEntry(Event event){
+        if (entry == null) {
+            append(event);
+        } else {
+            Event originalEntry = entry;
+            entry = event;
+            entry.setFunction(this);
+            event.setSuccessor(originalEntry);
+            originalEntry.setPredecessor(event);
+        }
+    }
+


This should probably be symmetric to updateExit() as it is the case in #803

hernanponcedeleon · 2025-02-25T08:55:27Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java

+                if (loopBegin.getPredecessor() == null) {
+                    Event newEntry = copies.get(0);
+                    loopBegin.getFunction().updateEntry(newEntry);
+                    newEntry.insertAfter(copies.subList(1, copies.size()));
+                } else {


Why do we need this special handling?

Due to the lack of insertBefore I think. I think its best to merge #803 and use the new functions rather than working around the limitations.

Yeah it causes issue when loop from the first event.

hernanponcedeleon · 2025-02-25T09:09:53Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java

+                final Thread thread = createSPVThreadFromFunction(entryFunction, tid, grid, transformers);
+                program.addThread(thread);
+            }
+            // Remove unused memory objects of the entry function


By "unused" you mean that a given object X was repladed by e.g., WX and from now one the program will use WX?

Given object X in the entry function, it will be replaceds by X0 in thread0, X1 in thread1.., and the entry function objects will not be used anymore.

hernanponcedeleon · 2025-02-25T09:10:32Z

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java

-import com.dat3m.dartagnan.program.Function;
-import com.dat3m.dartagnan.program.Program;
-import com.dat3m.dartagnan.program.Register;
+import com.dat3m.dartagnan.program.processing.transofrmers.MemoryTransformer;


typo in transformer

Thanks! updated

hernanponcedeleon · 2025-02-25T09:28:43Z

...nan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvOpenCL.java

+    public List<Event> visitSpirvLoad(SpirvLoad e) {
+        String mo = moToOpenCLTag(Tag.Spirv.getMoTag(e.getTags()));
+        Load load = newLoadWithMo(e.getResultRegister(), e.getAddress(), mo);
+        load.setFunction(e.getFunction());


VisitorSpirvVulkan is translated to Vulkan event sequences and those also need to create dummy registers for RMW. Why is this not a problem in that case?

Signed-off-by: Haining Tong <[email protected]>

natgavrilenko reviewed Jan 16, 2025

View reviewed changes

hernanponcedeleon reviewed Jan 16, 2025

View reviewed changes

natgavrilenko reviewed Jan 17, 2025

View reviewed changes

tonghaining force-pushed the opencl branch 2 times, most recently from 55e9306 to f813b99 Compare January 27, 2025 10:48

tonghaining force-pushed the opencl branch 2 times, most recently from adec207 to cd3219c Compare January 30, 2025 16:54

ThomasHaas reviewed Feb 3, 2025

View reviewed changes

ThomasHaas reviewed Feb 5, 2025

View reviewed changes

tonghaining force-pushed the opencl branch 2 times, most recently from 5ddbf02 to 6b10bf4 Compare February 12, 2025 10:28

ThomasHaas reviewed Feb 13, 2025

View reviewed changes

hernanponcedeleon mentioned this pull request Feb 14, 2025

Unrolling control barriers #797

Merged

natgavrilenko reviewed Feb 14, 2025

View reviewed changes

dartagnan/src/main/antlr4/Spirv.g4 Outdated Show resolved Hide resolved

dartagnan/src/main/antlr4/Spirv.g4 Outdated Show resolved Hide resolved

dartagnan/src/main/antlr4/SpirvLexer.g4 Outdated Show resolved Hide resolved

dartagnan/src/main/antlr4/Spirv.g4 Outdated Show resolved Hide resolved

natgavrilenko reviewed Feb 14, 2025

View reviewed changes

...n/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsConversion.java Outdated Show resolved Hide resolved

...n/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsConversion.java Outdated Show resolved Hide resolved

natgavrilenko reviewed Feb 18, 2025

View reviewed changes

tonghaining force-pushed the opencl branch 2 times, most recently from 3163cb4 to 2c93434 Compare February 19, 2025 09:41

natgavrilenko reviewed Feb 19, 2025

View reviewed changes

...nan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/helpers/HelperTags.java Outdated Show resolved Hide resolved

...an/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/utils/ThreadCreator.java Outdated Show resolved Hide resolved

natgavrilenko reviewed Feb 19, 2025

View reviewed changes

...nan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsFunction.java Outdated Show resolved Hide resolved

natgavrilenko reviewed Feb 19, 2025

View reviewed changes

ThomasHaas reviewed Feb 19, 2025

View reviewed changes

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java Outdated Show resolved Hide resolved

tonghaining force-pushed the opencl branch 2 times, most recently from 6e0eb25 to 232d7d5 Compare February 20, 2025 10:49

natgavrilenko reviewed Feb 21, 2025

View reviewed changes

...nan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvOpenCL.java Show resolved Hide resolved

natgavrilenko reviewed Feb 21, 2025

View reviewed changes

dartagnan/src/main/java/com/dat3m/dartagnan/program/ThreadGrid.java Outdated Show resolved Hide resolved

natgavrilenko reviewed Feb 21, 2025

View reviewed changes

dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/ClangSpirvAssertionsTest.java Outdated Show resolved Hide resolved

natgavrilenko reviewed Feb 21, 2025

View reviewed changes

...src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsFunctionTest.java Outdated Show resolved Hide resolved

tonghaining force-pushed the opencl branch from a59419a to fd60182 Compare February 22, 2025 11:39

natgavrilenko reviewed Feb 24, 2025

View reviewed changes

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java Outdated Show resolved Hide resolved

natgavrilenko reviewed Feb 24, 2025

View reviewed changes

tonghaining force-pushed the opencl branch from fd60182 to a1b80c5 Compare February 24, 2025 16:19

hernanponcedeleon reviewed Feb 24, 2025

View reviewed changes

hernanponcedeleon reviewed Feb 25, 2025

View reviewed changes

tonghaining force-pushed the opencl branch from 6d4f7d2 to 77a2a8f Compare February 25, 2025 11:57

add support for OpenCL SPIR-V

90034ec

Signed-off-by: Haining Tong <[email protected]>

tonghaining force-pushed the opencl branch from 77a2a8f to 90034ec Compare February 25, 2025 12:37

		final Map<String, Function> forwardFunctions = new HashMap<>();
		final Map<String, Set<FunctionCall>> forwardCalls = new HashMap<>();

Add support for OpenCL SPIR-V #792

Are you sure you want to change the base?

Add support for OpenCL SPIR-V #792

Conversation

tonghaining commented Jan 15, 2025

ThomasHaas commented Jan 15, 2025

tonghaining commented Jan 15, 2025

ThomasHaas commented Jan 15, 2025

tonghaining commented Jan 16, 2025

ThomasHaas commented Jan 16, 2025

natgavrilenko left a comment

Choose a reason for hiding this comment

hernanponcedeleon left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ThomasHaas commented Feb 14, 2025

hernanponcedeleon commented Feb 18, 2025

hernanponcedeleon left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment