From de2e6f04ddec014d7a903702d7403868d905cf7f Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Fri, 6 Oct 2023 15:03:18 +0200 Subject: [PATCH 01/21] Improve PTX grammar Signed-off-by: Hernan Ponce de Leon --- dartagnan/src/main/antlr4/LitmusPTX.g4 | 49 +++----- .../program/visitors/VisitorLitmusPTX.java | 110 +++++------------- 2 files changed, 43 insertions(+), 116 deletions(-) diff --git a/dartagnan/src/main/antlr4/LitmusPTX.g4 b/dartagnan/src/main/antlr4/LitmusPTX.g4 index 2692b39be6..54dabd0b3b 100644 --- a/dartagnan/src/main/antlr4/LitmusPTX.g4 +++ b/dartagnan/src/main/antlr4/LitmusPTX.g4 @@ -94,20 +94,11 @@ instruction ; storeInstruction - : storeConstant - | storeRegister - ; - -storeConstant - : store Period mo (Period scope)? location Comma constant - ; - -storeRegister - : store Period mo (Period scope)? location Comma register + : store Period mo (Period scope)? location Comma value ; loadInstruction - : localConstant + : localValue | localAdd | localSub | localMul @@ -115,24 +106,24 @@ loadInstruction | loadLocation ; -localConstant - : load Period mo (Period scope)? register Comma constant +localValue + : load Period mo (Period scope)? register Comma value ; localAdd - : Add register Comma register Comma constant + : Add register Comma value Comma value ; localSub - : Sub register Comma register Comma constant + : Sub register Comma value Comma value ; localMul - : Mul register Comma register Comma constant + : Mul register Comma value Comma value ; localDiv - : Div register Comma register Comma constant + : Div register Comma value Comma value ; loadLocation @@ -164,17 +155,12 @@ barrier ; atomInstruction - : atomConstant - | atomRegister + : atomOp | atomCAS ; -atomConstant - : atom Period mo Period scope Period operation register Comma location Comma constant - ; - -atomRegister - : atom Period mo Period scope Period operation register Comma location Comma register +atomOp + : atom Period mo Period scope Period operation register Comma location Comma value ; atomCAS @@ -182,20 +168,11 @@ atomCAS ; redInstruction - : redConstant - | redRegister - ; - -redConstant - : red Period mo Period scope Period operation location Comma constant - ; - -redRegister - : red Period mo Period scope Period operation location Comma register + : red Period mo Period scope Period operation location Comma value ; branchCond - : cond register Comma register Comma Label + : cond value Comma value Comma Label ; jump diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java index 40a1c1cf84..3643cd7ece 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java @@ -138,9 +138,9 @@ public Object visitInstructionRow(LitmusPTXParser.InstructionRowContext ctx) { } @Override - public Object visitStoreConstant(LitmusPTXParser.StoreConstantContext ctx) { + public Object visitStoreInstruction(LitmusPTXParser.StoreInstructionContext ctx) { MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText()); - IConst constant = (IConst) ctx.constant().accept(this); + Expression constant = (Expression) ctx.value().accept(this); String mo = ctx.mo().content; Store store = EventFactory.newStoreWithMo(object, constant, mo); switch (mo) { @@ -157,64 +157,45 @@ public Object visitStoreConstant(LitmusPTXParser.StoreConstantContext ctx) { } @Override - public Object visitStoreRegister(LitmusPTXParser.StoreRegisterContext ctx) { - MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText()); + public Object visitLocalValue(LitmusPTXParser.LocalValueContext ctx) { Register register = (Register) ctx.register().accept(this); - String mo = ctx.mo().content; - Store store = EventFactory.newStoreWithMo(object, register, mo); - switch (mo) { - case Tag.PTX.WEAK -> { - if (ctx.scope() != null) { - throw new ParsingException("Weak store instruction doesn't need scope: " + ctx.scope().content); - } - } - case Tag.PTX.REL, Tag.PTX.RLX -> store.addTags(ctx.scope().content); - default -> throw new ParsingException("Store instruction doesn't support mo: " + mo); - } - store.addTags(ctx.store().storeProxy); - return programBuilder.addChild(mainThread, store); - } - - @Override - public Object visitLocalConstant(LitmusPTXParser.LocalConstantContext ctx) { - Register register = (Register) ctx.register().accept(this); - IConst constant = (IConst) ctx.constant().accept(this); - return programBuilder.addChild(mainThread, EventFactory.newLocal(register, constant)); + Expression value = (Expression) ctx.value().accept(this); + return programBuilder.addChild(mainThread, EventFactory.newLocal(register, value)); } @Override public Object visitLocalAdd(LitmusPTXParser.LocalAddContext ctx) { - Register rd = (Register) ctx.register().get(0).accept(this); - Register rs = (Register) ctx.register().get(1).accept(this); - IConst constant = (IConst) ctx.constant().accept(this); - Expression exp = expressions.makeADD(rd, constant); + Register rd = (Register) ctx.register().accept(this); + Expression lhs = (Expression) ctx.value(0).accept(this); + Expression rhs = (Expression) ctx.value(1).accept(this); + Expression exp = expressions.makeADD(lhs, rhs); return programBuilder.addChild(mainThread, EventFactory.newLocal(rd, exp)); } @Override public Object visitLocalSub(LitmusPTXParser.LocalSubContext ctx) { - Register rd = (Register) ctx.register().get(0).accept(this); - Register rs = (Register) ctx.register().get(1).accept(this); - IConst constant = (IConst) ctx.constant().accept(this); - Expression exp = expressions.makeSUB(rd, constant); + Register rd = (Register) ctx.register().accept(this); + Expression lhs = (Expression) ctx.value(0).accept(this); + Expression rhs = (Expression) ctx.value(1).accept(this); + Expression exp = expressions.makeSUB(lhs, rhs); return programBuilder.addChild(mainThread, EventFactory.newLocal(rd, exp)); } @Override public Object visitLocalMul(LitmusPTXParser.LocalMulContext ctx) { - Register rd = (Register) ctx.register().get(0).accept(this); - Register rs = (Register) ctx.register().get(1).accept(this); - IConst constant = (IConst) ctx.constant().accept(this); - Expression exp = expressions.makeMUL(rd, constant); + Register rd = (Register) ctx.register().accept(this); + Expression lhs = (Expression) ctx.value(0).accept(this); + Expression rhs = (Expression) ctx.value(1).accept(this); + Expression exp = expressions.makeMUL(lhs, rhs); return programBuilder.addChild(mainThread, EventFactory.newLocal(rd, exp)); } @Override public Object visitLocalDiv(LitmusPTXParser.LocalDivContext ctx) { - Register rd = (Register) ctx.register().get(0).accept(this); - Register rs = (Register) ctx.register().get(1).accept(this); - IConst constant = (IConst) ctx.constant().accept(this); - Expression exp = expressions.makeDIV(rd, constant, true); + Register rd = (Register) ctx.register().accept(this); + Expression lhs = (Expression) ctx.value(0).accept(this); + Expression rhs = (Expression) ctx.value(1).accept(this); + Expression exp = expressions.makeDIV(lhs, rhs, true); return programBuilder.addChild(mainThread, EventFactory.newLocal(rd, exp)); } @@ -238,33 +219,17 @@ public Object visitLoadLocation(LitmusPTXParser.LoadLocationContext ctx) { } @Override - public Object visitAtomConstant(LitmusPTXParser.AtomConstantContext ctx) { + public Object visitAtomOp(LitmusPTXParser.AtomOpContext ctx) { Register register_destination = (Register) ctx.register().accept(this); MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText()); - IConst constant = (IConst) ctx.constant().accept(this); + Expression value = (Expression) ctx.value().accept(this); IOpBin op = ctx.operation().op; String mo = ctx.mo().content; String scope = ctx.scope().content; if (!(mo.equals(Tag.PTX.ACQ) || mo.equals(Tag.PTX.REL) || mo.equals(Tag.PTX.ACQ_REL) || mo.equals(Tag.PTX.RLX))) { throw new ParsingException("Atom instruction doesn't support mo: " + mo); } - PTXAtomOp atom = EventFactory.PTX.newAtomOp(object, register_destination, constant, op, mo, scope); - atom.addTags(ctx.atom().atomProxy); - return programBuilder.addChild(mainThread, atom); - } - - @Override - public Object visitAtomRegister(LitmusPTXParser.AtomRegisterContext ctx) { - Register register_destination = programBuilder.getOrNewRegister(mainThread, ctx.register().get(0).getText(), archType); - MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText()); - Register register_operand = programBuilder.getOrNewRegister(mainThread, ctx.register().get(1).getText(), archType); - IOpBin op = ctx.operation().op; - String mo = ctx.mo().content; - String scope = ctx.scope().content; - if (!(mo.equals(Tag.PTX.ACQ) || mo.equals(Tag.PTX.REL) || mo.equals(Tag.PTX.ACQ_REL) || mo.equals(Tag.PTX.RLX))) { - throw new ParsingException("Atom instruction doesn't support mo: " + mo); - } - PTXAtomOp atom = EventFactory.PTX.newAtomOp(object, register_destination, register_operand, op, mo, scope); + PTXAtomOp atom = EventFactory.PTX.newAtomOp(object, register_destination, value, op, mo, scope); atom.addTags(ctx.atom().atomProxy); return programBuilder.addChild(mainThread, atom); } @@ -286,31 +251,16 @@ public Object visitAtomCAS(LitmusPTXParser.AtomCASContext ctx) { } @Override - public Object visitRedConstant(LitmusPTXParser.RedConstantContext ctx) { - MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText()); - IConst constant = (IConst) ctx.constant().accept(this); - IOpBin op = ctx.operation().op; - String mo = ctx.mo().content; - String scope = ctx.scope().content; - if (!(mo.equals(Tag.PTX.ACQ) || mo.equals(Tag.PTX.REL) || mo.equals(Tag.PTX.ACQ_REL) || mo.equals(Tag.PTX.RLX))) { - throw new ParsingException("Red instruction doesn't support mo: " + mo); - } - PTXRedOp red = EventFactory.PTX.newRedOp(object, constant, op, mo, scope); - red.addTags(ctx.red().redProxy); - return programBuilder.addChild(mainThread, red); - } - - @Override - public Object visitRedRegister(LitmusPTXParser.RedRegisterContext ctx) { + public Object visitRedInstruction(LitmusPTXParser.RedInstructionContext ctx) { MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText()); - Register register_operand = (Register) ctx.register().accept(this); + Expression value = (Expression) ctx.value().accept(this); IOpBin op = ctx.operation().op; String mo = ctx.mo().content; String scope = ctx.scope().content; if (!(mo.equals(Tag.PTX.ACQ) || mo.equals(Tag.PTX.REL) || mo.equals(Tag.PTX.ACQ_REL) || mo.equals(Tag.PTX.RLX))) { throw new ParsingException("Red instruction doesn't support mo: " + mo); } - PTXRedOp red = EventFactory.PTX.newRedOp(object, register_operand, op, mo, scope); + PTXRedOp red = EventFactory.PTX.newRedOp(object, value, op, mo, scope); red.addTags(ctx.red().redProxy); return programBuilder.addChild(mainThread, red); } @@ -356,9 +306,9 @@ public Object visitLabel(LitmusPTXParser.LabelContext ctx) { @Override public Object visitBranchCond(LitmusPTXParser.BranchCondContext ctx) { Label label = programBuilder.getOrCreateLabel(mainThread, ctx.Label().getText()); - Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType); - Register r2 = programBuilder.getOrNewRegister(mainThread, ctx.register(1).getText(), archType); - Expression expr = expressions.makeBinary(r1, ctx.cond().op, r2); + Expression lhs = (Expression) ctx.value(0).accept(this); + Expression rhs = (Expression) ctx.value(1).accept(this); + Expression expr = expressions.makeBinary(lhs, ctx.cond().op, rhs); return programBuilder.addChild(mainThread, EventFactory.newJump(expr, label)); } From 6083775c263d13bf54f770b3d280ebd3939d307b Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Fri, 6 Oct 2023 15:32:26 +0200 Subject: [PATCH 02/21] Add XF_Barrier test Signed-off-by: Hernan Ponce de Leon --- litmus/PTX/Manual/XF-Barrier-RA.litmus | 27 ++++++++++++++++++++++++ litmus/PTX/Manual/XF-Barrier-weak.litmus | 27 ++++++++++++++++++++++++ 2 files changed, 54 insertions(+) create mode 100644 litmus/PTX/Manual/XF-Barrier-RA.litmus create mode 100644 litmus/PTX/Manual/XF-Barrier-weak.litmus diff --git a/litmus/PTX/Manual/XF-Barrier-RA.litmus b/litmus/PTX/Manual/XF-Barrier-RA.litmus new file mode 100644 index 0000000000..24d0fca09a --- /dev/null +++ b/litmus/PTX/Manual/XF-Barrier-RA.litmus @@ -0,0 +1,27 @@ +PTX XF-Barrier-RA +"Adapted from Figure 2 in +Portable Inter-workgroup Barrier Synchronisation for GPUs +https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" +{ +f0=0; +f1=0; +f2=0; +P0:r0=0; +P1:r0=1; +P2:r0=0; +P3:r0=1; +} + P0@cta 0,gpu 0 | P1@cta 0,gpu 0 | P2@cta 1,gpu 0 | P3@cta 1,gpu 0 ; + add r1, r0, 1 | add r1, r0, 1 | fence.sc.cta | fence.sc.cta ; + bge r1, 2, LC01 | bge r1, 2, LC11 | bne r0, 0, LC21 | bne r0, 0, LC31 ; + LC00: | LC10: | st.release.sys f1, 1 | st.release.sys f1, 1 ; + ld.acquire.sys r2, f1 | ld.acquire.sys r2, f2 | LC20: | LC30: ; + bne r2, 0, LC01 | bne r2, 0, LC11 | ld.acquire.sys r2, f1 | ld.acquire.sys r2, f1 ; + goto LC00 | goto LC10 | bne r2, 1, LC21 | bne r2, 1, LC31 ; + LC01: | LC11: | goto LC20 | goto LC30 ; + fence.sc.cta | fence.sc.cta | LC21: | LC31: ; + bge r1, 2, LC02 | bge r1, 2, LC12 | fence.sc.cta | fence.sc.cta ; + st.release.sys f1, 0 | st.release.sys f2, 0 | | ; + LC02: | LC12: | | ; +exists +(P1:r0 == 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/PTX/Manual/XF-Barrier-weak.litmus b/litmus/PTX/Manual/XF-Barrier-weak.litmus new file mode 100644 index 0000000000..83eb862666 --- /dev/null +++ b/litmus/PTX/Manual/XF-Barrier-weak.litmus @@ -0,0 +1,27 @@ +PTX XF-Barrier +"Adapted from Figure 2 in +Portable Inter-workgroup Barrier Synchronisation for GPUs +https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" +{ +f0=0; +f1=0; +f2=0; +P0:r0=0; +P1:r0=1; +P2:r0=0; +P3:r0=1; +} + P0@cta 0,gpu 0 | P1@cta 0,gpu 0 | P2@cta 1,gpu 0 | P3@cta 1,gpu 0 ; + add r1, r0, 1 | add r1, r0, 1 | fence.sc.cta | fence.sc.cta ; + bge r1, 2, LC01 | bge r1, 2, LC11 | bne r0, 0, LC21 | bne r0, 0, LC31 ; + LC00: | LC10: | st.weak f1, 1 | st.weak f1, 1 ; + ld.weak r2, f1 | ld.weak r2, f2 | LC20: | LC30: ; + bne r2, 0, LC01 | bne r2, 0, LC11 | ld.weak r2, f1 | ld.weak r2, f1 ; + goto LC00 | goto LC10 | bne r2, 1, LC21 | bne r2, 1, LC31 ; + LC01: | LC11: | goto LC20 | goto LC30 ; + fence.sc.cta | fence.sc.cta | LC21: | LC31: ; + bge r1, 2, LC02 | bge r1, 2, LC12 | fence.sc.cta | fence.sc.cta ; + st.weak f1, 0 | st.weak f2, 0 | | ; + LC02: | LC12: | | ; +exists +(P1:r0 == 1 /\ P1:r1 == 0) \ No newline at end of file From f2a5be762d3a4dcd5898fe59aef5a8fec60a7d31 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 7 Oct 2023 08:47:15 +0200 Subject: [PATCH 03/21] Improve Vulkan grammar Signed-off-by: Hernan Ponce de Leon --- dartagnan/src/main/antlr4/LitmusVulkan.g4 | 20 ++++++++-------- .../program/visitors/VisitorLitmusVulkan.java | 24 +++++++++---------- 2 files changed, 22 insertions(+), 22 deletions(-) diff --git a/dartagnan/src/main/antlr4/LitmusVulkan.g4 b/dartagnan/src/main/antlr4/LitmusVulkan.g4 index 26b03ad14f..5de395c6a9 100644 --- a/dartagnan/src/main/antlr4/LitmusVulkan.g4 +++ b/dartagnan/src/main/antlr4/LitmusVulkan.g4 @@ -108,12 +108,12 @@ storeInstruction ; loadInstruction - : localConstant + : localValue | loadLocation ; -localConstant - : Load atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList register Comma constant +localValue + : Load atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList register Comma value ; loadLocation @@ -121,16 +121,16 @@ loadLocation ; rmwInstruction - : rmwConstant - | rmwConstantOp + : rmwValue + | rmwOp ; -rmwConstant - : RMW atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList register Comma location Comma constant +rmwValue + : RMW atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList register Comma location Comma value ; -rmwConstantOp - : RMW atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList operation register Comma location Comma constant +rmwOp + : RMW atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList operation register Comma location Comma value ; fenceInstruction @@ -156,7 +156,7 @@ label ; branchCond - : cond register Comma register Comma Label + : cond value Comma value Comma Label ; jump diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java index 26edfe38ca..5cbb16b50e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java @@ -207,10 +207,10 @@ public Object visitStoreInstruction(LitmusVulkanParser.StoreInstructionContext c } @Override - public Object visitLocalConstant(LitmusVulkanParser.LocalConstantContext ctx) { + public Object visitLocalValue(LitmusVulkanParser.LocalValueContext ctx) { Register register = (Register) ctx.register().accept(this); - IConst constant = (IConst) ctx.constant().accept(this); - return programBuilder.addChild(mainThread, EventFactory.newLocal(register, constant)); + Expression value = (Expression) ctx.value().accept(this); + return programBuilder.addChild(mainThread, EventFactory.newLocal(register, value)); } @Override @@ -244,10 +244,10 @@ public Object visitLoadLocation(LitmusVulkanParser.LoadLocationContext ctx) { } @Override - public Object visitRmwConstant(LitmusVulkanParser.RmwConstantContext ctx) { + public Object visitRmwValue(LitmusVulkanParser.RmwValueContext ctx) { Register register = (Register) ctx.register().accept(this); MemoryObject location = programBuilder.getOrNewMemoryObject(ctx.location().getText()); - IConst constant = (IConst) ctx.constant().accept(this); + Expression value = (Expression) ctx.value().accept(this); Boolean atomic = true; // RMW is always atomic String mo = (ctx.mo() != null) ? ctx.mo().content : ""; String avvis = (ctx.avvis() != null) ? ctx.avvis().content : ""; @@ -255,7 +255,7 @@ public Object visitRmwConstant(LitmusVulkanParser.RmwConstantContext ctx) { String storageClass = ctx.storageClass().content; List storageClassSemantics = (List) ctx.storageClassSemanticList().accept(this); List avvisSemantics = (List) ctx.avvisSemanticList().accept(this); - VulkanRMW rmw = EventFactory.Vulkan.newRMW(location, register, constant, mo, scope); + VulkanRMW rmw = EventFactory.Vulkan.newRMW(location, register, value, mo, scope); if (!avvis.isEmpty()) { rmw.addTags(avvis); } @@ -264,10 +264,10 @@ public Object visitRmwConstant(LitmusVulkanParser.RmwConstantContext ctx) { } @Override - public Object visitRmwConstantOp(LitmusVulkanParser.RmwConstantOpContext ctx) { + public Object visitRmwOp(LitmusVulkanParser.RmwOpContext ctx) { Register register = (Register) ctx.register().accept(this); MemoryObject location = programBuilder.getOrNewMemoryObject(ctx.location().getText()); - IConst constant = (IConst) ctx.constant().accept(this); + Expression value = (Expression) ctx.value().accept(this); Boolean atomic = true; // RMW is always atomic String mo = (ctx.mo() != null) ? ctx.mo().content : ""; String avvis = (ctx.avvis() != null) ? ctx.avvis().content : ""; @@ -276,7 +276,7 @@ public Object visitRmwConstantOp(LitmusVulkanParser.RmwConstantOpContext ctx) { IOpBin op = ctx.operation().op; List storageClassSemantics = (List) ctx.storageClassSemanticList().accept(this); List avvisSemantics = (List) ctx.avvisSemanticList().accept(this); - VulkanRMWOp rmw = EventFactory.Vulkan.newRMWOp(location, register, constant, op, mo, scope); + VulkanRMWOp rmw = EventFactory.Vulkan.newRMWOp(location, register, value, op, mo, scope); if (!avvis.isEmpty()) { rmw.addTags(avvis); } @@ -357,9 +357,9 @@ public Object visitLabel(LitmusVulkanParser.LabelContext ctx) { @Override public Object visitBranchCond(LitmusVulkanParser.BranchCondContext ctx) { Label label = programBuilder.getOrCreateLabel(mainThread, ctx.Label().getText()); - Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType); - Register r2 = programBuilder.getOrNewRegister(mainThread, ctx.register(1).getText(), archType); - Expression expr = expressions.makeBinary(r1, ctx.cond().op, r2); + Expression lhs = (Expression) ctx.value(0).accept(this); + Expression rhs = (Expression) ctx.value(1).accept(this); + Expression expr = expressions.makeBinary(lhs, ctx.cond().op, rhs); return programBuilder.addChild(mainThread, EventFactory.newJump(expr, label)); } From 3d699384031a52a9b1d44f034a85c27735fd0b7e Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 7 Oct 2023 08:47:58 +0200 Subject: [PATCH 04/21] Remove unused variable from XF-Barrier Signed-off-by: Hernan Ponce de Leon --- litmus/PTX/Manual/XF-Barrier-RA.litmus | 1 - litmus/PTX/Manual/XF-Barrier-weak.litmus | 1 - 2 files changed, 2 deletions(-) diff --git a/litmus/PTX/Manual/XF-Barrier-RA.litmus b/litmus/PTX/Manual/XF-Barrier-RA.litmus index 24d0fca09a..4d5986e6dd 100644 --- a/litmus/PTX/Manual/XF-Barrier-RA.litmus +++ b/litmus/PTX/Manual/XF-Barrier-RA.litmus @@ -3,7 +3,6 @@ PTX XF-Barrier-RA Portable Inter-workgroup Barrier Synchronisation for GPUs https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" { -f0=0; f1=0; f2=0; P0:r0=0; diff --git a/litmus/PTX/Manual/XF-Barrier-weak.litmus b/litmus/PTX/Manual/XF-Barrier-weak.litmus index 83eb862666..88a84420ab 100644 --- a/litmus/PTX/Manual/XF-Barrier-weak.litmus +++ b/litmus/PTX/Manual/XF-Barrier-weak.litmus @@ -3,7 +3,6 @@ PTX XF-Barrier Portable Inter-workgroup Barrier Synchronisation for GPUs https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" { -f0=0; f1=0; f2=0; P0:r0=0; From ab42d4f1c33878e83d8d3a36ed700c14837c9dc8 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 7 Oct 2023 08:51:03 +0200 Subject: [PATCH 05/21] Use improved grammar in tests Signed-off-by: Hernan Ponce de Leon --- litmus/VULKAN/Manual/MP-mesa-fence-loop.litmus | 2 +- litmus/VULKAN/Manual/MP-mesa-load-acq.litmus | 2 +- litmus/VULKAN/Manual/MP-mesa.litmus | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/litmus/VULKAN/Manual/MP-mesa-fence-loop.litmus b/litmus/VULKAN/Manual/MP-mesa-fence-loop.litmus index a041396a37..baca414a21 100644 --- a/litmus/VULKAN/Manual/MP-mesa-fence-loop.litmus +++ b/litmus/VULKAN/Manual/MP-mesa-fence-loop.litmus @@ -9,7 +9,7 @@ flag=0; LC00: | st.atom.dv.sc0 data, 1 ; ld.atom.dv.sc0 r1, flag | membar.rel.dv.semsc0 ; membar.acq.dv.semsc0 | st.atom.dv.sc0 flag, 1 ; - bne r1, r0, LC01 | ; + bne r1, 0, LC01 | ; goto LC00 | ; LC01: | ; ld.atom.dv.sc0 r2, data | ; diff --git a/litmus/VULKAN/Manual/MP-mesa-load-acq.litmus b/litmus/VULKAN/Manual/MP-mesa-load-acq.litmus index 03f8006f5e..77dc5e748e 100644 --- a/litmus/VULKAN/Manual/MP-mesa-load-acq.litmus +++ b/litmus/VULKAN/Manual/MP-mesa-load-acq.litmus @@ -8,7 +8,7 @@ flag=0; P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 1, qf 0 ; LC00: | st.atom.dv.sc0 data, 1 ; ld.atom.acq.dv.sc0.semsc0 r1, flag | membar.rel.dv.semsc0 ; - bne r1, r0, LC01 | st.atom.dv.sc0 flag, 1 ; + bne r1, 0, LC01 | st.atom.dv.sc0 flag, 1 ; goto LC00 | ; LC01: | ; ld.atom.dv.sc0 r2, data | ; diff --git a/litmus/VULKAN/Manual/MP-mesa.litmus b/litmus/VULKAN/Manual/MP-mesa.litmus index 0ed5b16063..3b303b8b3d 100644 --- a/litmus/VULKAN/Manual/MP-mesa.litmus +++ b/litmus/VULKAN/Manual/MP-mesa.litmus @@ -8,7 +8,7 @@ flag=0; P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 1, qf 0 ; LC00: | st.atom.dv.sc0 data, 1 ; ld.atom.dv.sc0 r1, flag | membar.rel.dv.semsc0 ; - bne r1, r0, LC01 | st.atom.dv.sc0 flag, 1 ; + bne r1, 0, LC01 | st.atom.dv.sc0 flag, 1 ; goto LC00 | ; LC01: | ; membar.acq.dv.semsc0 | ; From c1ef31de3d9ee4e1cd77d16c2cd15c5f9a2a3e35 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 7 Oct 2023 09:14:34 +0200 Subject: [PATCH 06/21] Add, Sub, ... in Vulkan grammar Signed-off-by: Hernan Ponce de Leon --- dartagnan/src/main/antlr4/LitmusVulkan.g4 | 26 ++++++++++++-- .../program/visitors/VisitorLitmusVulkan.java | 36 +++++++++++++++++++ .../VULKAN/Manual/ticketlock-acq2rlx-1.litmus | 4 +-- .../VULKAN/Manual/ticketlock-acq2rlx-2.litmus | 4 +-- .../VULKAN/Manual/ticketlock-diff-wg.litmus | 4 +-- .../VULKAN/Manual/ticketlock-rel2rlx.litmus | 4 +-- .../VULKAN/Manual/ticketlock-same-wg.litmus | 4 +-- 7 files changed, 69 insertions(+), 13 deletions(-) diff --git a/dartagnan/src/main/antlr4/LitmusVulkan.g4 b/dartagnan/src/main/antlr4/LitmusVulkan.g4 index 5de395c6a9..25507017b3 100644 --- a/dartagnan/src/main/antlr4/LitmusVulkan.g4 +++ b/dartagnan/src/main/antlr4/LitmusVulkan.g4 @@ -109,6 +109,10 @@ storeInstruction loadInstruction : localValue + | localAdd + | localSub + | localMul + | localDiv | loadLocation ; @@ -116,6 +120,22 @@ localValue : Load atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList register Comma value ; +localAdd + : Add register Comma value Comma value + ; + +localSub + : Sub register Comma value Comma value + ; + +localMul + : Mul register Comma value Comma value + ; + +localDiv + : Div register Comma value Comma value + ; + loadLocation : Load atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList register Comma location ; @@ -309,9 +329,9 @@ Bgt : 'bgt'; Ble : 'ble'; Bge : 'bge'; -Add : 'plus'; -Sub : 'minus'; -Mult : 'mult'; +Add : 'add'; +Sub : 'sub'; +Mult : 'mul'; Div : 'div'; And : 'and'; Or : 'or'; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java index 5cbb16b50e..ce7c0a4418 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java @@ -213,6 +213,42 @@ public Object visitLocalValue(LitmusVulkanParser.LocalValueContext ctx) { return programBuilder.addChild(mainThread, EventFactory.newLocal(register, value)); } + @Override + public Object visitLocalAdd(LitmusVulkanParser.LocalAddContext ctx) { + Register rd = (Register) ctx.register().accept(this); + Expression lhs = (Expression) ctx.value(0).accept(this); + Expression rhs = (Expression) ctx.value(1).accept(this); + Expression exp = expressions.makeADD(lhs, rhs); + return programBuilder.addChild(mainThread, EventFactory.newLocal(rd, exp)); + } + + @Override + public Object visitLocalSub(LitmusVulkanParser.LocalSubContext ctx) { + Register rd = (Register) ctx.register().accept(this); + Expression lhs = (Expression) ctx.value(0).accept(this); + Expression rhs = (Expression) ctx.value(1).accept(this); + Expression exp = expressions.makeSUB(lhs, rhs); + return programBuilder.addChild(mainThread, EventFactory.newLocal(rd, exp)); + } + + @Override + public Object visitLocalMul(LitmusVulkanParser.LocalMulContext ctx) { + Register rd = (Register) ctx.register().accept(this); + Expression lhs = (Expression) ctx.value(0).accept(this); + Expression rhs = (Expression) ctx.value(1).accept(this); + Expression exp = expressions.makeMUL(lhs, rhs); + return programBuilder.addChild(mainThread, EventFactory.newLocal(rd, exp)); + } + + @Override + public Object visitLocalDiv(LitmusVulkanParser.LocalDivContext ctx) { + Register rd = (Register) ctx.register().accept(this); + Expression lhs = (Expression) ctx.value(0).accept(this); + Expression rhs = (Expression) ctx.value(1).accept(this); + Expression exp = expressions.makeDIV(lhs, rhs, true); + return programBuilder.addChild(mainThread, EventFactory.newLocal(rd, exp)); + } + @Override public Object visitLoadLocation(LitmusVulkanParser.LoadLocationContext ctx) { Register register = (Register) ctx.register().accept(this); diff --git a/litmus/VULKAN/Manual/ticketlock-acq2rlx-1.litmus b/litmus/VULKAN/Manual/ticketlock-acq2rlx-1.litmus index c66f05a3fa..3b357ae285 100644 --- a/litmus/VULKAN/Manual/ticketlock-acq2rlx-1.litmus +++ b/litmus/VULKAN/Manual/ticketlock-acq2rlx-1.litmus @@ -5,7 +5,7 @@ in=0; out=0; x=0; } P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; - rmw.atom.wg.sc0.semsc0.plus r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.plus r1, in, 1 ; + rmw.atom.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; LC00: | LC00: ; ld.atom.acq.wg.sc0.semsc0.semvis r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; beq r1, r2, LC01 | beq r1, r2, LC01 ; @@ -13,6 +13,6 @@ x=0; LC01: | LC01: ; ld.nonpriv.sc0.semsc0 r3, x | ld.nonpriv.sc0.semsc0 r3, x ; st.nonpriv.sc0.semsc0 x, 1 | st.nonpriv.sc0.semsc0 x, 1 ; - rmw.atom.rel.wg.sc0.semsc0.semav.plus r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.plus r4, out, 1 ; + rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; exists (P0:r1 == P0:r2 /\ P1:r1 == P1:r2 /\ P0:r3 == 0 /\ P1:r3 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/ticketlock-acq2rlx-2.litmus b/litmus/VULKAN/Manual/ticketlock-acq2rlx-2.litmus index 767655b5fd..a0b41290cc 100644 --- a/litmus/VULKAN/Manual/ticketlock-acq2rlx-2.litmus +++ b/litmus/VULKAN/Manual/ticketlock-acq2rlx-2.litmus @@ -5,7 +5,7 @@ in=0; out=0; x=0; } P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; - rmw.atom.acq.wg.sc0.semsc0.plus r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.plus r1, in, 1 ; + rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; LC00: | LC00: ; ld.atom.wg.sc0.semsc0 r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; beq r1, r2, LC01 | beq r1, r2, LC01 ; @@ -13,6 +13,6 @@ x=0; LC01: | LC01: ; ld.nonpriv.sc0.semsc0 r3, x | ld.nonpriv.sc0.semsc0 r3, x ; st.nonpriv.sc0.semsc0 x, 1 | st.nonpriv.sc0.semsc0 x, 1 ; - rmw.atom.rel.wg.sc0.semsc0.semav.plus r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.plus r4, out, 1 ; + rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; exists (P0:r1 == P0:r2 /\ P1:r1 == P1:r2 /\ P0:r3 == 0 /\ P1:r3 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/ticketlock-diff-wg.litmus b/litmus/VULKAN/Manual/ticketlock-diff-wg.litmus index 31d921383b..85f9faec37 100644 --- a/litmus/VULKAN/Manual/ticketlock-diff-wg.litmus +++ b/litmus/VULKAN/Manual/ticketlock-diff-wg.litmus @@ -5,7 +5,7 @@ in=0; out=0; x=0; } P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 1, qf 0 ; - rmw.atom.acq.wg.sc0.semsc0.plus r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.plus r1, in, 1 ; + rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; LC00: | LC00: ; ld.atom.acq.wg.sc0.semsc0.semvis r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; beq r1, r2, LC01 | beq r1, r2, LC01 ; @@ -13,6 +13,6 @@ x=0; LC01: | LC01: ; ld.nonpriv.sc0.semsc0 r3, x | ld.nonpriv.sc0.semsc0 r3, x ; st.nonpriv.sc0.semsc0 x, 1 | st.nonpriv.sc0.semsc0 x, 1 ; - rmw.atom.rel.wg.sc0.semsc0.semav.plus r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.plus r4, out, 1 ; + rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; exists (P0:r1 == P0:r2 /\ P1:r1 == P1:r2 /\ P0:r3 == 0 /\ P1:r3 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/ticketlock-rel2rlx.litmus b/litmus/VULKAN/Manual/ticketlock-rel2rlx.litmus index a759e1d3a1..495a384224 100644 --- a/litmus/VULKAN/Manual/ticketlock-rel2rlx.litmus +++ b/litmus/VULKAN/Manual/ticketlock-rel2rlx.litmus @@ -5,7 +5,7 @@ in=0; out=0; x=0; } P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; - rmw.atom.acq.wg.sc0.semsc0.plus r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.plus r1, in, 1 ; + rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; LC00: | LC00: ; ld.atom.acq.wg.sc0.semsc0.semvis r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; beq r1, r2, LC01 | beq r1, r2, LC01 ; @@ -13,6 +13,6 @@ x=0; LC01: | LC01: ; ld.nonpriv.sc0.semsc0 r3, x | ld.nonpriv.sc0.semsc0 r3, x ; st.nonpriv.sc0.semsc0 x, 1 | st.nonpriv.sc0.semsc0 x, 1 ; - rmw.atom.wg.sc0.semsc0.plus r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.plus r4, out, 1 ; + rmw.atom.wg.sc0.semsc0.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; exists (P0:r1 == P0:r2 /\ P1:r1 == P1:r2 /\ P0:r3 == 0 /\ P1:r3 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/ticketlock-same-wg.litmus b/litmus/VULKAN/Manual/ticketlock-same-wg.litmus index 762b424dfd..673cd2b843 100644 --- a/litmus/VULKAN/Manual/ticketlock-same-wg.litmus +++ b/litmus/VULKAN/Manual/ticketlock-same-wg.litmus @@ -5,7 +5,7 @@ in=0; out=0; x=0; } P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 0, qf 0 ; - rmw.atom.acq.wg.sc0.semsc0.plus r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.plus r1, in, 1 ; + rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 | rmw.atom.acq.wg.sc0.semsc0.add r1, in, 1 ; LC00: | LC00: ; ld.atom.acq.wg.sc0.semsc0.semvis r2, out | ld.atom.acq.wg.sc0.semsc0.semvis r2, out ; beq r1, r2, LC01 | beq r1, r2, LC01 ; @@ -13,6 +13,6 @@ x=0; LC01: | LC01: ; ld.nonpriv.sc0.semsc0 r3, x | ld.nonpriv.sc0.semsc0 r3, x ; st.nonpriv.sc0.semsc0 x, 1 | st.nonpriv.sc0.semsc0 x, 1 ; - rmw.atom.rel.wg.sc0.semsc0.semav.plus r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.plus r4, out, 1 ; + rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 | rmw.atom.rel.wg.sc0.semsc0.semav.add r4, out, 1 ; exists (P0:r1 == P0:r2 /\ P1:r1 == P1:r2 /\ P0:r3 == 0 /\ P1:r3 == 0) \ No newline at end of file From b9c56c3e95e3eff600440713df17d5d7248bebef Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 7 Oct 2023 16:07:57 +0200 Subject: [PATCH 07/21] Changes to XF-Barrier Signed-off-by: Hernan Ponce de Leon --- .../dat3m/dartagnan/program/event/Tag.java | 2 -- litmus/PTX/Manual/XF-Barrier-RA.litmus | 26 -------------- litmus/PTX/Manual/XF-Barrier-atom.litmus | 24 +++++++++++++ litmus/PTX/Manual/XF-Barrier-weak.litmus | 36 +++++++++---------- litmus/VULKAN/Manual/XF-Barrier-atom.litmus | 24 +++++++++++++ litmus/VULKAN/Manual/XF-Barrier-weak.litmus | 24 +++++++++++++ 6 files changed, 89 insertions(+), 47 deletions(-) delete mode 100644 litmus/PTX/Manual/XF-Barrier-RA.litmus create mode 100644 litmus/PTX/Manual/XF-Barrier-atom.litmus create mode 100644 litmus/VULKAN/Manual/XF-Barrier-atom.litmus create mode 100644 litmus/VULKAN/Manual/XF-Barrier-weak.litmus diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java index 5670e4060d..f852aaa779 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java @@ -2,8 +2,6 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.program.event.core.Event; -import com.dat3m.dartagnan.program.event.core.Load; -import com.dat3m.dartagnan.program.event.core.Store; import java.util.List; diff --git a/litmus/PTX/Manual/XF-Barrier-RA.litmus b/litmus/PTX/Manual/XF-Barrier-RA.litmus deleted file mode 100644 index 4d5986e6dd..0000000000 --- a/litmus/PTX/Manual/XF-Barrier-RA.litmus +++ /dev/null @@ -1,26 +0,0 @@ -PTX XF-Barrier-RA -"Adapted from Figure 2 in -Portable Inter-workgroup Barrier Synchronisation for GPUs -https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" -{ -f1=0; -f2=0; -P0:r0=0; -P1:r0=1; -P2:r0=0; -P3:r0=1; -} - P0@cta 0,gpu 0 | P1@cta 0,gpu 0 | P2@cta 1,gpu 0 | P3@cta 1,gpu 0 ; - add r1, r0, 1 | add r1, r0, 1 | fence.sc.cta | fence.sc.cta ; - bge r1, 2, LC01 | bge r1, 2, LC11 | bne r0, 0, LC21 | bne r0, 0, LC31 ; - LC00: | LC10: | st.release.sys f1, 1 | st.release.sys f1, 1 ; - ld.acquire.sys r2, f1 | ld.acquire.sys r2, f2 | LC20: | LC30: ; - bne r2, 0, LC01 | bne r2, 0, LC11 | ld.acquire.sys r2, f1 | ld.acquire.sys r2, f1 ; - goto LC00 | goto LC10 | bne r2, 1, LC21 | bne r2, 1, LC31 ; - LC01: | LC11: | goto LC20 | goto LC30 ; - fence.sc.cta | fence.sc.cta | LC21: | LC31: ; - bge r1, 2, LC02 | bge r1, 2, LC12 | fence.sc.cta | fence.sc.cta ; - st.release.sys f1, 0 | st.release.sys f2, 0 | | ; - LC02: | LC12: | | ; -exists -(P1:r0 == 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/PTX/Manual/XF-Barrier-atom.litmus b/litmus/PTX/Manual/XF-Barrier-atom.litmus new file mode 100644 index 0000000000..b6bb9d847e --- /dev/null +++ b/litmus/PTX/Manual/XF-Barrier-atom.litmus @@ -0,0 +1,24 @@ +PTX XF-Barrier-atom +"Adapted from Figure 2 in +Portable Inter-workgroup Barrier Synchronisation for GPUs +https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" +{ +f=0; +P0:r0=0; +P1:r0=0; +P2:r0=1; +} + P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; + add r1, r0, 1 | bar.cta.sync 1 | bar.cta.sync 1 ; + bge r1, 2, LC01 | bne r0, 0, LC11 | bne r0, 0, LC21 ; + LC00: | st.relaxed.gpu f, 1 | st.relaxed.gpu f, 1 ; + ld.relaxed.gpu r2, f | LC10: | LC20: ; + bne r2, 0, LC01 | ld.relaxed.gpu r2, f | ld.relaxed.gpu r2, f ; + goto LC00 | bne r2, 1, LC11 | bne r2, 1, LC21 ; + LC01: | goto LC10 | goto LC20 ; + bar.cta.sync 1 | LC11: | LC21: ; + bge r1, 2, LC02 | bar.cta.sync 1 | bar.cta.sync 1 ; + st.relaxed.gpu f, 0 | | ; + LC02: | | ; +exists +(P0:r0 == P0:r0) \ No newline at end of file diff --git a/litmus/PTX/Manual/XF-Barrier-weak.litmus b/litmus/PTX/Manual/XF-Barrier-weak.litmus index 88a84420ab..27f5446911 100644 --- a/litmus/PTX/Manual/XF-Barrier-weak.litmus +++ b/litmus/PTX/Manual/XF-Barrier-weak.litmus @@ -1,26 +1,24 @@ -PTX XF-Barrier +PTX XF-Barrier-weak "Adapted from Figure 2 in Portable Inter-workgroup Barrier Synchronisation for GPUs https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" { -f1=0; -f2=0; +f=0; P0:r0=0; -P1:r0=1; -P2:r0=0; -P3:r0=1; +P1:r0=0; +P2:r0=1; } - P0@cta 0,gpu 0 | P1@cta 0,gpu 0 | P2@cta 1,gpu 0 | P3@cta 1,gpu 0 ; - add r1, r0, 1 | add r1, r0, 1 | fence.sc.cta | fence.sc.cta ; - bge r1, 2, LC01 | bge r1, 2, LC11 | bne r0, 0, LC21 | bne r0, 0, LC31 ; - LC00: | LC10: | st.weak f1, 1 | st.weak f1, 1 ; - ld.weak r2, f1 | ld.weak r2, f2 | LC20: | LC30: ; - bne r2, 0, LC01 | bne r2, 0, LC11 | ld.weak r2, f1 | ld.weak r2, f1 ; - goto LC00 | goto LC10 | bne r2, 1, LC21 | bne r2, 1, LC31 ; - LC01: | LC11: | goto LC20 | goto LC30 ; - fence.sc.cta | fence.sc.cta | LC21: | LC31: ; - bge r1, 2, LC02 | bge r1, 2, LC12 | fence.sc.cta | fence.sc.cta ; - st.weak f1, 0 | st.weak f2, 0 | | ; - LC02: | LC12: | | ; + P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; + add r1, r0, 1 | bar.cta.sync 1 | bar.cta.sync 1 ; + bge r1, 2, LC01 | bne r0, 0, LC11 | bne r0, 0, LC21 ; + LC00: | st.weak f, 1 | st.weak f, 1 ; + ld.weak r2, f | LC10: | LC20: ; + bne r2, 0, LC01 | ld.weak r2, f | ld.weak r2, f ; + goto LC00 | bne r2, 1, LC11 | bne r2, 1, LC21 ; + LC01: | goto LC10 | goto LC20 ; + bar.cta.sync 1 | LC11: | LC21: ; + bge r1, 2, LC02 | bar.cta.sync 1 | bar.cta.sync 1 ; + st.weak f, 0 | | ; + LC02: | | ; exists -(P1:r0 == 1 /\ P1:r1 == 0) \ No newline at end of file +(P0:r0 == P0:r0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-atom.litmus b/litmus/VULKAN/Manual/XF-Barrier-atom.litmus new file mode 100644 index 0000000000..5d6281f847 --- /dev/null +++ b/litmus/VULKAN/Manual/XF-Barrier-atom.litmus @@ -0,0 +1,24 @@ +Vulkan XF-Barrier-atom +"Adapted from Figure 2 in +Portable Inter-workgroup Barrier Synchronisation for GPUs +https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" +{ +f=0; +P0:r0=0; +P1:r0=0; +P2:r0=1; +} + P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; + add r1, r0, 1 | cbar.wg 1 | cbar.wg 1 ; + bge r1, 2, LC01 | bne r0, 0, LC11 | bne r0, 0, LC21 ; + LC00: | st.atom.dv.sc0 f, 1 | st.atom.dv.sc0 f, 1 ; + ld.atom.dv.sc0 r2, f | LC10: | LC20: ; + bne r2, 0, LC01 | ld.atom.dv.sc0 r2, f | ld.atom.dv.sc0 r2, f ; + goto LC00 | bne r2, 1, LC11 | bne r2, 1, LC21 ; + LC01: | goto LC10 | goto LC20 ; + cbar.wg 1 | LC11: | LC21: ; + bge r1, 2, LC02 | cbar.wg 1 | cbar.wg 1 ; + st.atom.dv.sc0 f, 0 | | ; + LC02: | | ; +exists +(P0:r0 == P0:r0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus new file mode 100644 index 0000000000..96d64d823c --- /dev/null +++ b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus @@ -0,0 +1,24 @@ +Vulkan XF-Barrier-weak +"Adapted from Figure 2 in +Portable Inter-workgroup Barrier Synchronisation for GPUs +https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" +{ +f=0; +P0:r0=0; +P1:r0=0; +P2:r0=1; +} + P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; + add r1, r0, 1 | cbar.wg 1 | cbar.wg 1 ; + bge r1, 2, LC01 | bne r0, 0, LC11 | bne r0, 0, LC21 ; + LC00: | st.dv.sc0 f, 1 | st.dv.sc0 f, 1 ; + ld.dv.sc0 r2, f | LC10: | LC20: ; + bne r2, 0, LC01 | ld.dv.sc0 r2, f | ld.dv.sc0 r2, f ; + goto LC00 | bne r2, 1, LC11 | bne r2, 1, LC21 ; + LC01: | goto LC10 | goto LC20 ; + cbar.wg 1 | LC11: | LC21: ; + bge r1, 2, LC02 | cbar.wg 1 | cbar.wg 1 ; + st.dv.sc0 f, 0 | | ; + LC02: | | ; +exists +(P0:r0 == P0:r0) \ No newline at end of file From d1e53e8cf04ed80c6ce82d4b49038a7da3b7816b Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 7 Oct 2023 20:19:22 +0200 Subject: [PATCH 08/21] Remove useless (constant) jump in master Signed-off-by: Hernan Ponce de Leon --- litmus/PTX/Manual/XF-Barrier-atom.litmus | 20 +++++++++---------- litmus/PTX/Manual/XF-Barrier-weak.litmus | 20 +++++++++---------- litmus/VULKAN/Manual/XF-Barrier-atom.litmus | 22 ++++++++++----------- litmus/VULKAN/Manual/XF-Barrier-weak.litmus | 20 +++++++++---------- 4 files changed, 37 insertions(+), 45 deletions(-) diff --git a/litmus/PTX/Manual/XF-Barrier-atom.litmus b/litmus/PTX/Manual/XF-Barrier-atom.litmus index b6bb9d847e..325def934a 100644 --- a/litmus/PTX/Manual/XF-Barrier-atom.litmus +++ b/litmus/PTX/Manual/XF-Barrier-atom.litmus @@ -9,16 +9,14 @@ P1:r0=0; P2:r0=1; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; - add r1, r0, 1 | bar.cta.sync 1 | bar.cta.sync 1 ; - bge r1, 2, LC01 | bne r0, 0, LC11 | bne r0, 0, LC21 ; - LC00: | st.relaxed.gpu f, 1 | st.relaxed.gpu f, 1 ; - ld.relaxed.gpu r2, f | LC10: | LC20: ; - bne r2, 0, LC01 | ld.relaxed.gpu r2, f | ld.relaxed.gpu r2, f ; - goto LC00 | bne r2, 1, LC11 | bne r2, 1, LC21 ; - LC01: | goto LC10 | goto LC20 ; - bar.cta.sync 1 | LC11: | LC21: ; - bge r1, 2, LC02 | bar.cta.sync 1 | bar.cta.sync 1 ; - st.relaxed.gpu f, 0 | | ; - LC02: | | ; + LC00: | bar.cta.sync 1 | bar.cta.sync 1 ; + ld.relaxed.gpu r2, f | bne r0, 0, LC11 | bne r0, 0, LC21 ; + bne r2, 0, LC01 | st.relaxed.gpu f, 1 | st.relaxed.gpu f, 1 ; + goto LC00 | LC10: | LC20: ; + LC01: | ld.relaxed.gpu r2, f | ld.relaxed.gpu r2, f ; + bar.cta.sync 1 | bne r2, 1, LC11 | bne r2, 1, LC21 ; + st.relaxed.gpu f, 0 | goto LC10 | goto LC20 ; + | LC11: | LC21: ; + | bar.cta.sync 1 | bar.cta.sync 1 ; exists (P0:r0 == P0:r0) \ No newline at end of file diff --git a/litmus/PTX/Manual/XF-Barrier-weak.litmus b/litmus/PTX/Manual/XF-Barrier-weak.litmus index 27f5446911..bcf2c75bfd 100644 --- a/litmus/PTX/Manual/XF-Barrier-weak.litmus +++ b/litmus/PTX/Manual/XF-Barrier-weak.litmus @@ -9,16 +9,14 @@ P1:r0=0; P2:r0=1; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; - add r1, r0, 1 | bar.cta.sync 1 | bar.cta.sync 1 ; - bge r1, 2, LC01 | bne r0, 0, LC11 | bne r0, 0, LC21 ; - LC00: | st.weak f, 1 | st.weak f, 1 ; - ld.weak r2, f | LC10: | LC20: ; - bne r2, 0, LC01 | ld.weak r2, f | ld.weak r2, f ; - goto LC00 | bne r2, 1, LC11 | bne r2, 1, LC21 ; - LC01: | goto LC10 | goto LC20 ; - bar.cta.sync 1 | LC11: | LC21: ; - bge r1, 2, LC02 | bar.cta.sync 1 | bar.cta.sync 1 ; - st.weak f, 0 | | ; - LC02: | | ; + LC00: | bar.cta.sync 1 | bar.cta.sync 1 ; + ld.weak r2, f | bne r0, 0, LC11 | bne r0, 0, LC21 ; + bne r2, 0, LC01 | st.weak f, 1 | st.weak f, 1 ; + goto LC00 | LC10: | LC20: ; + LC01: | ld.weak r2, f | ld.weak r2, f ; + bar.cta.sync 1 | bne r2, 1, LC11 | bne r2, 1, LC21 ; + st.weak f, 0 | goto LC10 | goto LC20 ; + | LC11: | LC21: ; + | bar.cta.sync 1 | bar.cta.sync 1 ; exists (P0:r0 == P0:r0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-atom.litmus b/litmus/VULKAN/Manual/XF-Barrier-atom.litmus index 5d6281f847..3b046a93cd 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-atom.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-atom.litmus @@ -1,4 +1,4 @@ -Vulkan XF-Barrier-atom +Vulkan XF-Barrier-weak "Adapted from Figure 2 in Portable Inter-workgroup Barrier Synchronisation for GPUs https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" @@ -9,16 +9,14 @@ P1:r0=0; P2:r0=1; } P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; - add r1, r0, 1 | cbar.wg 1 | cbar.wg 1 ; - bge r1, 2, LC01 | bne r0, 0, LC11 | bne r0, 0, LC21 ; - LC00: | st.atom.dv.sc0 f, 1 | st.atom.dv.sc0 f, 1 ; - ld.atom.dv.sc0 r2, f | LC10: | LC20: ; - bne r2, 0, LC01 | ld.atom.dv.sc0 r2, f | ld.atom.dv.sc0 r2, f ; - goto LC00 | bne r2, 1, LC11 | bne r2, 1, LC21 ; - LC01: | goto LC10 | goto LC20 ; - cbar.wg 1 | LC11: | LC21: ; - bge r1, 2, LC02 | cbar.wg 1 | cbar.wg 1 ; - st.atom.dv.sc0 f, 0 | | ; - LC02: | | ; + LC00: | cbar.wg 1 | cbar.wg 1 ; + ld.atom.dv.sc0 r2, f | bne r0, 0, LC11 | bne r0, 0, LC21 ; + bne r2, 0, LC01 | st.atom.dv.sc0 f, 1 | st.atom.dv.sc0 f, 1 ; + goto LC00 | LC10: | LC20: ; + LC01: | ld.atom.dv.sc0 r2, f | ld.atom.dv.sc0 r2, f ; + cbar.wg 1 | bne r2, 1, LC11 | bne r2, 1, LC21 ; + st.atom.dv.sc0 f, 0 | goto LC10 | goto LC20 ; + | LC11: | LC21: ; + | cbar.wg 1 | cbar.wg 1 ; exists (P0:r0 == P0:r0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus index 96d64d823c..18fa83ddda 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus @@ -9,16 +9,14 @@ P1:r0=0; P2:r0=1; } P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; - add r1, r0, 1 | cbar.wg 1 | cbar.wg 1 ; - bge r1, 2, LC01 | bne r0, 0, LC11 | bne r0, 0, LC21 ; - LC00: | st.dv.sc0 f, 1 | st.dv.sc0 f, 1 ; - ld.dv.sc0 r2, f | LC10: | LC20: ; - bne r2, 0, LC01 | ld.dv.sc0 r2, f | ld.dv.sc0 r2, f ; - goto LC00 | bne r2, 1, LC11 | bne r2, 1, LC21 ; - LC01: | goto LC10 | goto LC20 ; - cbar.wg 1 | LC11: | LC21: ; - bge r1, 2, LC02 | cbar.wg 1 | cbar.wg 1 ; - st.dv.sc0 f, 0 | | ; - LC02: | | ; + LC00: | cbar.wg 1 | cbar.wg 1 ; + ld.dv.sc0 r2, f | bne r0, 0, LC11 | bne r0, 0, LC21 ; + bne r2, 0, LC01 | st.dv.sc0 f, 1 | st.dv.sc0 f, 1 ; + goto LC00 | LC10: | LC20: ; + LC01: | ld.dv.sc0 r2, f | ld.dv.sc0 r2, f ; + cbar.wg 1 | bne r2, 1, LC11 | bne r2, 1, LC21 ; + st.dv.sc0 f, 0 | goto LC10 | goto LC20 ; + | LC11: | LC21: ; + | cbar.wg 1 | cbar.wg 1 ; exists (P0:r0 == P0:r0) \ No newline at end of file From dad414f364ae75e10560a3ae427d377f8d2ec817 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 7 Oct 2023 21:39:21 +0200 Subject: [PATCH 09/21] Remove dead code in slaves Signed-off-by: Hernan Ponce de Leon --- litmus/PTX/Manual/XF-Barrier-atom.litmus | 19 +++++++++---------- litmus/PTX/Manual/XF-Barrier-weak.litmus | 19 +++++++++---------- litmus/VULKAN/Manual/XF-Barrier-atom.litmus | 19 +++++++++---------- litmus/VULKAN/Manual/XF-Barrier-weak.litmus | 15 +++++++-------- 4 files changed, 34 insertions(+), 38 deletions(-) diff --git a/litmus/PTX/Manual/XF-Barrier-atom.litmus b/litmus/PTX/Manual/XF-Barrier-atom.litmus index 325def934a..9d385b3489 100644 --- a/litmus/PTX/Manual/XF-Barrier-atom.litmus +++ b/litmus/PTX/Manual/XF-Barrier-atom.litmus @@ -8,15 +8,14 @@ P0:r0=0; P1:r0=0; P2:r0=1; } - P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; - LC00: | bar.cta.sync 1 | bar.cta.sync 1 ; - ld.relaxed.gpu r2, f | bne r0, 0, LC11 | bne r0, 0, LC21 ; - bne r2, 0, LC01 | st.relaxed.gpu f, 1 | st.relaxed.gpu f, 1 ; - goto LC00 | LC10: | LC20: ; - LC01: | ld.relaxed.gpu r2, f | ld.relaxed.gpu r2, f ; - bar.cta.sync 1 | bne r2, 1, LC11 | bne r2, 1, LC21 ; - st.relaxed.gpu f, 0 | goto LC10 | goto LC20 ; - | LC11: | LC21: ; - | bar.cta.sync 1 | bar.cta.sync 1 ; + P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; + LC00: | bar.cta.sync 1 | bar.cta.sync 1 ; + ld.relaxed.gpu r2, f | st.relaxed.gpu f, 1 | bar.cta.sync 1 ; + bne r2, 0, LC01 | LC10: | ; + goto LC00 | ld.relaxed.gpu r2, f | ; + LC01: | bne r2, 1, LC11 | ; + bar.cta.sync 1 | goto LC10 | ; + st.relaxed.gpu f, 0 | LC11: | ; + | bar.cta.sync 1 | ; exists (P0:r0 == P0:r0) \ No newline at end of file diff --git a/litmus/PTX/Manual/XF-Barrier-weak.litmus b/litmus/PTX/Manual/XF-Barrier-weak.litmus index bcf2c75bfd..8fd554d6f3 100644 --- a/litmus/PTX/Manual/XF-Barrier-weak.litmus +++ b/litmus/PTX/Manual/XF-Barrier-weak.litmus @@ -8,15 +8,14 @@ P0:r0=0; P1:r0=0; P2:r0=1; } - P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; - LC00: | bar.cta.sync 1 | bar.cta.sync 1 ; - ld.weak r2, f | bne r0, 0, LC11 | bne r0, 0, LC21 ; - bne r2, 0, LC01 | st.weak f, 1 | st.weak f, 1 ; - goto LC00 | LC10: | LC20: ; - LC01: | ld.weak r2, f | ld.weak r2, f ; - bar.cta.sync 1 | bne r2, 1, LC11 | bne r2, 1, LC21 ; - st.weak f, 0 | goto LC10 | goto LC20 ; - | LC11: | LC21: ; - | bar.cta.sync 1 | bar.cta.sync 1 ; + P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; + LC00: | bar.cta.sync 1 | bar.cta.sync 1 ; + ld.weak r2, f | st.weak f, 1 | bar.cta.sync 1 ; + bne r2, 0, LC01 | LC10: | ; + goto LC00 | ld.weak r2, f | ; + LC01: | bne r2, 1, LC11 | ; + bar.cta.sync 1 | goto LC10 | ; + st.weak f, 0 | LC11: | ; + | bar.cta.sync 1 | ; exists (P0:r0 == P0:r0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-atom.litmus b/litmus/VULKAN/Manual/XF-Barrier-atom.litmus index 3b046a93cd..b180b0f9d9 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-atom.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-atom.litmus @@ -8,15 +8,14 @@ P0:r0=0; P1:r0=0; P2:r0=1; } - P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; - LC00: | cbar.wg 1 | cbar.wg 1 ; - ld.atom.dv.sc0 r2, f | bne r0, 0, LC11 | bne r0, 0, LC21 ; - bne r2, 0, LC01 | st.atom.dv.sc0 f, 1 | st.atom.dv.sc0 f, 1 ; - goto LC00 | LC10: | LC20: ; - LC01: | ld.atom.dv.sc0 r2, f | ld.atom.dv.sc0 r2, f ; - cbar.wg 1 | bne r2, 1, LC11 | bne r2, 1, LC21 ; - st.atom.dv.sc0 f, 0 | goto LC10 | goto LC20 ; - | LC11: | LC21: ; - | cbar.wg 1 | cbar.wg 1 ; + P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; + LC00: | cbar.wg 1 | cbar.wg 1 ; + ld.atom.dv.sc0 r2, f | st.atom.dv.sc0 f, 1 | cbar.wg 1 ; + bne r2, 0, LC01 | LC10: | ; + goto LC00 | ld.atom.dv.sc0 r2, f | ; + LC01: | bne r2, 1, LC11 | ; + cbar.wg 1 | goto LC10 | ; + st.atom.dv.sc0 f, 0 | LC11: | ; + | cbar.wg 1 | ; exists (P0:r0 == P0:r0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus index 18fa83ddda..4ec2df3769 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus @@ -10,13 +10,12 @@ P2:r0=1; } P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; LC00: | cbar.wg 1 | cbar.wg 1 ; - ld.dv.sc0 r2, f | bne r0, 0, LC11 | bne r0, 0, LC21 ; - bne r2, 0, LC01 | st.dv.sc0 f, 1 | st.dv.sc0 f, 1 ; - goto LC00 | LC10: | LC20: ; - LC01: | ld.dv.sc0 r2, f | ld.dv.sc0 r2, f ; - cbar.wg 1 | bne r2, 1, LC11 | bne r2, 1, LC21 ; - st.dv.sc0 f, 0 | goto LC10 | goto LC20 ; - | LC11: | LC21: ; - | cbar.wg 1 | cbar.wg 1 ; + ld.dv.sc0 r2, f | st.dv.sc0 f, 1 | cbar.wg 1 ; + bne r2, 0, LC01 | LC10: | ; + goto LC00 | ld.dv.sc0 r2, f | ; + LC01: | bne r2, 1, LC11 | ; + cbar.wg 1 | goto LC10 | ; + st.dv.sc0 f, 0 | LC11: | ; + | cbar.wg 1 | ; exists (P0:r0 == P0:r0) \ No newline at end of file From de287821a248157e4104804a2a6b51c80a8992d5 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 10 Oct 2023 17:23:20 +0200 Subject: [PATCH 10/21] Add RA version of XF-Barrier Signed-off-by: Hernan Ponce de Leon --- litmus/VULKAN/Manual/XF-Barrier-RA.litmus | 23 +++++++++++++++++++++ litmus/VULKAN/Manual/XF-Barrier-atom.litmus | 22 +++++++++++--------- litmus/VULKAN/Manual/XF-Barrier-weak.litmus | 19 +++++++++-------- 3 files changed, 45 insertions(+), 19 deletions(-) create mode 100644 litmus/VULKAN/Manual/XF-Barrier-RA.litmus diff --git a/litmus/VULKAN/Manual/XF-Barrier-RA.litmus b/litmus/VULKAN/Manual/XF-Barrier-RA.litmus new file mode 100644 index 0000000000..99ec994ccd --- /dev/null +++ b/litmus/VULKAN/Manual/XF-Barrier-RA.litmus @@ -0,0 +1,23 @@ +Vulkan XF-Barrier-RA +"Adapted from Figure 2 in +Portable Inter-workgroup Barrier Synchronisation for GPUs +https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" +{ +x=0; +f=0; +P0:r0=0; +P1:r0=0; +P2:r0=1; +} + P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; + st.av.dv.sc0 x, 1 | cbar.wg 1 | cbar.wg 1 ; + LC00: | st.atom.dv.sc0 f, 1 | cbar.wg 1 ; + ld.atom.dv.sc0 r2, f | LC10: | ; + bne r2, 0, LC01 | ld.atom.acq.dv.sc0.semsc0 r2, f | ; + goto LC00 | bne r2, 1, LC11 | ; + LC01: | goto LC10 | ; + cbar.wg 1 | LC11: | ; + st.atom.rel.dv.sc0.semsc0 f, 0 | cbar.wg 1 | ; + | ld.vis.dv.sc0 r1, x | ; +exists +(P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-atom.litmus b/litmus/VULKAN/Manual/XF-Barrier-atom.litmus index b180b0f9d9..7164220f22 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-atom.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-atom.litmus @@ -1,21 +1,23 @@ -Vulkan XF-Barrier-weak +Vulkan XF-Barrier-atom "Adapted from Figure 2 in Portable Inter-workgroup Barrier Synchronisation for GPUs https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" { +x=0; f=0; P0:r0=0; P1:r0=0; P2:r0=1; } P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; - LC00: | cbar.wg 1 | cbar.wg 1 ; - ld.atom.dv.sc0 r2, f | st.atom.dv.sc0 f, 1 | cbar.wg 1 ; - bne r2, 0, LC01 | LC10: | ; - goto LC00 | ld.atom.dv.sc0 r2, f | ; - LC01: | bne r2, 1, LC11 | ; - cbar.wg 1 | goto LC10 | ; - st.atom.dv.sc0 f, 0 | LC11: | ; - | cbar.wg 1 | ; + st.av.dv.sc0 x, 1 | cbar.wg 1 | cbar.wg 1 ; + LC00: | st.atom.dv.sc0 f, 1 | cbar.wg 1 ; + ld.atom.dv.sc0 r2, f | LC10: | ; + bne r2, 0, LC01 | ld.atom.dv.sc0 r2, f | ; + goto LC00 | bne r2, 1, LC11 | ; + LC01: | goto LC10 | ; + cbar.wg 1 | LC11: | ; + st.atom.dv.sc0 f, 0 | cbar.wg 1 | ; + | ld.vis.dv.sc0 r1, x | ; exists -(P0:r0 == P0:r0) \ No newline at end of file +(P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus index 4ec2df3769..134f846a98 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus @@ -9,13 +9,14 @@ P1:r0=0; P2:r0=1; } P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; - LC00: | cbar.wg 1 | cbar.wg 1 ; - ld.dv.sc0 r2, f | st.dv.sc0 f, 1 | cbar.wg 1 ; - bne r2, 0, LC01 | LC10: | ; - goto LC00 | ld.dv.sc0 r2, f | ; - LC01: | bne r2, 1, LC11 | ; - cbar.wg 1 | goto LC10 | ; - st.dv.sc0 f, 0 | LC11: | ; - | cbar.wg 1 | ; + st.av.dv.sc0 x, 1 | cbar.wg 1 | cbar.wg 1 ; + LC00: | st.dv.sc0 f, 1 | cbar.wg 1 ; + ld.dv.sc0 r2, f | LC10: | ; + bne r2, 0, LC01 | ld.dv.sc0 r2, f | ; + goto LC00 | bne r2, 1, LC11 | ; + LC01: | goto LC10 | ; + cbar.wg 1 | LC11: | ; + st.dv.sc0 f, 0 | cbar.wg 1 | ; + | ld.vis.dv.sc0 r1, x | ; exists -(P0:r0 == P0:r0) \ No newline at end of file +(P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file From 7723400e44de4d4196177038edf89c697b66f9ba Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Wed, 11 Oct 2023 09:48:55 +0200 Subject: [PATCH 11/21] More fixed to XF-Barrier Signed-off-by: Hernan Ponce de Leon --- litmus/PTX/Manual/XF-Barrier-atom.litmus | 20 ++++++++++---------- litmus/PTX/Manual/XF-Barrier-weak.litmus | 20 ++++++++++---------- litmus/VULKAN/Manual/XF-Barrier-RA.litmus | 1 - litmus/VULKAN/Manual/XF-Barrier-atom.litmus | 1 - litmus/VULKAN/Manual/XF-Barrier-weak.litmus | 1 - 5 files changed, 20 insertions(+), 23 deletions(-) diff --git a/litmus/PTX/Manual/XF-Barrier-atom.litmus b/litmus/PTX/Manual/XF-Barrier-atom.litmus index 9d385b3489..e5290660d0 100644 --- a/litmus/PTX/Manual/XF-Barrier-atom.litmus +++ b/litmus/PTX/Manual/XF-Barrier-atom.litmus @@ -6,16 +6,16 @@ https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" f=0; P0:r0=0; P1:r0=0; -P2:r0=1; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; - LC00: | bar.cta.sync 1 | bar.cta.sync 1 ; - ld.relaxed.gpu r2, f | st.relaxed.gpu f, 1 | bar.cta.sync 1 ; - bne r2, 0, LC01 | LC10: | ; - goto LC00 | ld.relaxed.gpu r2, f | ; - LC01: | bne r2, 1, LC11 | ; - bar.cta.sync 1 | goto LC10 | ; - st.relaxed.gpu f, 0 | LC11: | ; - | bar.cta.sync 1 | ; + st.weak x, 1 | bar.cta.sync 1 | bar.cta.sync 1 ; + LC00: | st.relaxed.gpu f, 1 | bar.cta.sync 1 ; + ld.relaxed.gpu r2, f | LC10: | ; + bne r2, 0, LC01 | ld.relaxed.gpu r2, f | ; + goto LC00 | bne r2, 1, LC11 | ; + LC01: | goto LC10 | ; + bar.cta.sync 1 | LC11: | ; + st.relaxed.gpu f, 0 | bar.cta.sync 1 | ; + | ld.weak r1, x | ; exists -(P0:r0 == P0:r0) \ No newline at end of file +(P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/PTX/Manual/XF-Barrier-weak.litmus b/litmus/PTX/Manual/XF-Barrier-weak.litmus index 8fd554d6f3..3c91746c33 100644 --- a/litmus/PTX/Manual/XF-Barrier-weak.litmus +++ b/litmus/PTX/Manual/XF-Barrier-weak.litmus @@ -6,16 +6,16 @@ https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" f=0; P0:r0=0; P1:r0=0; -P2:r0=1; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; - LC00: | bar.cta.sync 1 | bar.cta.sync 1 ; - ld.weak r2, f | st.weak f, 1 | bar.cta.sync 1 ; - bne r2, 0, LC01 | LC10: | ; - goto LC00 | ld.weak r2, f | ; - LC01: | bne r2, 1, LC11 | ; - bar.cta.sync 1 | goto LC10 | ; - st.weak f, 0 | LC11: | ; - | bar.cta.sync 1 | ; + st.weak x, 1 | bar.cta.sync 1 | bar.cta.sync 1 ; + LC00: | st.weak f, 1 | bar.cta.sync 1 ; + ld.weak r2, f | LC10: | ; + bne r2, 0, LC01 | ld.weak r2, f | ; + goto LC00 | bne r2, 1, LC11 | ; + LC01: | goto LC10 | ; + bar.cta.sync 1 | LC11: | ; + st.weak f, 0 | bar.cta.sync 1 | ; + | ld.weak r1, x | ; exists -(P0:r0 == P0:r0) \ No newline at end of file +(P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-RA.litmus b/litmus/VULKAN/Manual/XF-Barrier-RA.litmus index 99ec994ccd..a7933581bf 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-RA.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-RA.litmus @@ -7,7 +7,6 @@ x=0; f=0; P0:r0=0; P1:r0=0; -P2:r0=1; } P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; st.av.dv.sc0 x, 1 | cbar.wg 1 | cbar.wg 1 ; diff --git a/litmus/VULKAN/Manual/XF-Barrier-atom.litmus b/litmus/VULKAN/Manual/XF-Barrier-atom.litmus index 7164220f22..4c07ac952d 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-atom.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-atom.litmus @@ -7,7 +7,6 @@ x=0; f=0; P0:r0=0; P1:r0=0; -P2:r0=1; } P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; st.av.dv.sc0 x, 1 | cbar.wg 1 | cbar.wg 1 ; diff --git a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus index 134f846a98..a0e682b69d 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus @@ -6,7 +6,6 @@ https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" f=0; P0:r0=0; P1:r0=0; -P2:r0=1; } P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; st.av.dv.sc0 x, 1 | cbar.wg 1 | cbar.wg 1 ; From 0a7c6f10cd8654b783a71e180ea301553cfcf9c9 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sun, 22 Oct 2023 21:33:44 +0200 Subject: [PATCH 12/21] Change file names for XF-Barrier Signed-off-by: Hernan Ponce de Leon --- .../PTX/Manual/{XF-Barrier-atom.litmus => XF-Barrier-rlx.litmus} | 0 .../Manual/{XF-Barrier-RA.litmus => XF-Barrier-relacq.litmus} | 0 .../Manual/{XF-Barrier-atom.litmus => XF-Barrier-rlx.litmus} | 0 3 files changed, 0 insertions(+), 0 deletions(-) rename litmus/PTX/Manual/{XF-Barrier-atom.litmus => XF-Barrier-rlx.litmus} (100%) rename litmus/VULKAN/Manual/{XF-Barrier-RA.litmus => XF-Barrier-relacq.litmus} (100%) rename litmus/VULKAN/Manual/{XF-Barrier-atom.litmus => XF-Barrier-rlx.litmus} (100%) diff --git a/litmus/PTX/Manual/XF-Barrier-atom.litmus b/litmus/PTX/Manual/XF-Barrier-rlx.litmus similarity index 100% rename from litmus/PTX/Manual/XF-Barrier-atom.litmus rename to litmus/PTX/Manual/XF-Barrier-rlx.litmus diff --git a/litmus/VULKAN/Manual/XF-Barrier-RA.litmus b/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus similarity index 100% rename from litmus/VULKAN/Manual/XF-Barrier-RA.litmus rename to litmus/VULKAN/Manual/XF-Barrier-relacq.litmus diff --git a/litmus/VULKAN/Manual/XF-Barrier-atom.litmus b/litmus/VULKAN/Manual/XF-Barrier-rlx.litmus similarity index 100% rename from litmus/VULKAN/Manual/XF-Barrier-atom.litmus rename to litmus/VULKAN/Manual/XF-Barrier-rlx.litmus From 46b77a28c60c2e99b891c5860f06ad36666e13a3 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sun, 22 Oct 2023 21:41:07 +0200 Subject: [PATCH 13/21] Add XF-Barrier to unit tests Signed-off-by: Hernan Ponce de Leon --- dartagnan/src/test/resources/PTXv6_0-expected.csv | 2 ++ dartagnan/src/test/resources/PTXv7_5-expected.csv | 2 ++ dartagnan/src/test/resources/VULKAN-CK-expected.csv | 5 ++++- dartagnan/src/test/resources/VULKAN-DR-expected.csv | 5 ++++- dartagnan/src/test/resources/VULKAN-expected.csv | 3 +++ 5 files changed, 15 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/test/resources/PTXv6_0-expected.csv b/dartagnan/src/test/resources/PTXv6_0-expected.csv index b07d6dd039..a7ff03a89c 100644 --- a/dartagnan/src/test/resources/PTXv6_0-expected.csv +++ b/dartagnan/src/test/resources/PTXv6_0-expected.csv @@ -58,3 +58,5 @@ litmus/PTX/Manual/LB-dlb-no-fence-2,1 litmus/PTX/Nvidia/SB+bar-dyn-reg-const,0 litmus/PTX/Nvidia/SB+bar-sta-reg-const,1 litmus/PTX/Manual/CoWW-weak.litmus,1 +litmus/PTX/Manual/XF-Barrier-rlx.litmus,0 +litmus/PTX/Manual/XF-Barrier-weak.litmus,1 \ No newline at end of file diff --git a/dartagnan/src/test/resources/PTXv7_5-expected.csv b/dartagnan/src/test/resources/PTXv7_5-expected.csv index 0f3fba15a6..76ff6a955c 100644 --- a/dartagnan/src/test/resources/PTXv7_5-expected.csv +++ b/dartagnan/src/test/resources/PTXv7_5-expected.csv @@ -123,3 +123,5 @@ litmus/PTX/Manual/LB-dlb-no-fence-2.litmus,1 litmus/PTX/Nvidia/SB+bar-dyn-reg-const.litmus,0 litmus/PTX/Nvidia/SB+bar-sta-reg-const.litmus,1 litmus/PTX/Manual/CoWW-weak.litmus,1 +litmus/PTX/Manual/XF-Barrier-rlx.litmus,0 +litmus/PTX/Manual/XF-Barrier-weak.litmus,1 \ No newline at end of file diff --git a/dartagnan/src/test/resources/VULKAN-CK-expected.csv b/dartagnan/src/test/resources/VULKAN-CK-expected.csv index a06c42c5e3..5a495ef2ab 100644 --- a/dartagnan/src/test/resources/VULKAN-CK-expected.csv +++ b/dartagnan/src/test/resources/VULKAN-CK-expected.csv @@ -134,4 +134,7 @@ litmus/VULKAN/Manual/ticketlock-rel2rlx.litmus,1 litmus/VULKAN/Manual/MP-mesa.litmus,1 litmus/VULKAN/Manual/MP-mesa-load-acq.litmus,1 litmus/VULKAN/Manual/MP-mesa-fence-loop.litmus,1 -litmus/VULKAN/Manual/MP-mesa-optimized.litmus,1 \ No newline at end of file +litmus/VULKAN/Manual/MP-mesa-optimized.litmus,1 +litmus/VULKAN/Manual/XF-Barrier-relacq.litmus,1 +litmus/VULKAN/Manual/XF-Barrier-rlx.litmus,1 +litmus/VULKAN/Manual/XF-Barrier-weak.litmus,1 \ No newline at end of file diff --git a/dartagnan/src/test/resources/VULKAN-DR-expected.csv b/dartagnan/src/test/resources/VULKAN-DR-expected.csv index 4e58ecedf1..9c4d26a5b7 100644 --- a/dartagnan/src/test/resources/VULKAN-DR-expected.csv +++ b/dartagnan/src/test/resources/VULKAN-DR-expected.csv @@ -76,4 +76,7 @@ litmus/VULKAN/Manual/ticketlock-rel2rlx.litmus,1 litmus/VULKAN/Manual/MP-mesa.litmus,0 litmus/VULKAN/Manual/MP-mesa-load-acq.litmus,0 litmus/VULKAN/Manual/MP-mesa-fence-loop.litmus,0 -litmus/VULKAN/Manual/MP-mesa-optimized.litmus,0 \ No newline at end of file +litmus/VULKAN/Manual/MP-mesa-optimized.litmus,0 +litmus/VULKAN/Manual/XF-Barrier-relacq.litmus,0 +litmus/VULKAN/Manual/XF-Barrier-rlx.litmus,1 +litmus/VULKAN/Manual/XF-Barrier-weak.litmus,1 \ No newline at end of file diff --git a/dartagnan/src/test/resources/VULKAN-expected.csv b/dartagnan/src/test/resources/VULKAN-expected.csv index 0b42481b11..c566f47645 100644 --- a/dartagnan/src/test/resources/VULKAN-expected.csv +++ b/dartagnan/src/test/resources/VULKAN-expected.csv @@ -84,3 +84,6 @@ litmus/VULKAN/Manual/MP-mesa-optimized.litmus,1 litmus/VULKAN/Manual/MP-avvis.litmus,0 litmus/VULKAN/Manual/MP-no-avvis.litmus,1 litmus/VULKAN/Manual/CoWW-RR.litmus,1 +litmus/VULKAN/Manual/XF-Barrier-relacq.litmus,0 +litmus/VULKAN/Manual/XF-Barrier-rlx.litmus,1 +litmus/VULKAN/Manual/XF-Barrier-weak.litmus,1 From 6080eb9ee267d788aede254461acd6cc33e13055 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 23 Oct 2023 09:41:31 +0200 Subject: [PATCH 14/21] Fix expected results Signed-off-by: Hernan Ponce de Leon --- dartagnan/src/test/resources/PTXv6_0-expected.csv | 2 +- dartagnan/src/test/resources/PTXv7_5-expected.csv | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/test/resources/PTXv6_0-expected.csv b/dartagnan/src/test/resources/PTXv6_0-expected.csv index a7ff03a89c..625b6e9bf8 100644 --- a/dartagnan/src/test/resources/PTXv6_0-expected.csv +++ b/dartagnan/src/test/resources/PTXv6_0-expected.csv @@ -59,4 +59,4 @@ litmus/PTX/Nvidia/SB+bar-dyn-reg-const,0 litmus/PTX/Nvidia/SB+bar-sta-reg-const,1 litmus/PTX/Manual/CoWW-weak.litmus,1 litmus/PTX/Manual/XF-Barrier-rlx.litmus,0 -litmus/PTX/Manual/XF-Barrier-weak.litmus,1 \ No newline at end of file +litmus/PTX/Manual/XF-Barrier-weak.litmus,0 \ No newline at end of file diff --git a/dartagnan/src/test/resources/PTXv7_5-expected.csv b/dartagnan/src/test/resources/PTXv7_5-expected.csv index 76ff6a955c..8e06a91083 100644 --- a/dartagnan/src/test/resources/PTXv7_5-expected.csv +++ b/dartagnan/src/test/resources/PTXv7_5-expected.csv @@ -124,4 +124,4 @@ litmus/PTX/Nvidia/SB+bar-dyn-reg-const.litmus,0 litmus/PTX/Nvidia/SB+bar-sta-reg-const.litmus,1 litmus/PTX/Manual/CoWW-weak.litmus,1 litmus/PTX/Manual/XF-Barrier-rlx.litmus,0 -litmus/PTX/Manual/XF-Barrier-weak.litmus,1 \ No newline at end of file +litmus/PTX/Manual/XF-Barrier-weak.litmus,0 \ No newline at end of file From f375f6fad394e1b3bdd74235beb73ff8a8ae2c57 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 23 Oct 2023 09:49:28 +0200 Subject: [PATCH 15/21] Fix ids in control barriers Signed-off-by: Hernan Ponce de Leon --- cat/spirv-check.cat | 2 +- litmus/PTX/Manual/XF-Barrier-rlx.litmus | 4 ++-- litmus/PTX/Manual/XF-Barrier-weak.litmus | 4 ++-- litmus/VULKAN/Manual/XF-Barrier-relacq.litmus | 4 ++-- litmus/VULKAN/Manual/XF-Barrier-rlx.litmus | 4 ++-- litmus/VULKAN/Manual/XF-Barrier-weak.litmus | 4 ++-- 6 files changed, 11 insertions(+), 11 deletions(-) diff --git a/cat/spirv-check.cat b/cat/spirv-check.cat index 0807636688..bffbbd4af0 100644 --- a/cat/spirv-check.cat +++ b/cat/spirv-check.cat @@ -195,7 +195,7 @@ let scbarinstIsPo = (syncbar & (po | po^-1)) flag ~empty scbarinstIsPo as checkScbarinstIsPo // can't have two cbars where one comes first in po in one thread and second in po in another thread -let scbarinstIsPo2 = (syncbar & (po; syncbar; po) & syncbar) +let scbarinstIsPo2 = (po; syncbar; po) & syncbar flag ~empty scbarinstIsPo2 as checkScbarinstIsPo2 // the same instance of a control barrier must have same scope, acq/rel, semantics diff --git a/litmus/PTX/Manual/XF-Barrier-rlx.litmus b/litmus/PTX/Manual/XF-Barrier-rlx.litmus index e5290660d0..a37cc4eac9 100644 --- a/litmus/PTX/Manual/XF-Barrier-rlx.litmus +++ b/litmus/PTX/Manual/XF-Barrier-rlx.litmus @@ -9,13 +9,13 @@ P1:r0=0; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; st.weak x, 1 | bar.cta.sync 1 | bar.cta.sync 1 ; - LC00: | st.relaxed.gpu f, 1 | bar.cta.sync 1 ; + LC00: | st.relaxed.gpu f, 1 | bar.cta.sync 2 ; ld.relaxed.gpu r2, f | LC10: | ; bne r2, 0, LC01 | ld.relaxed.gpu r2, f | ; goto LC00 | bne r2, 1, LC11 | ; LC01: | goto LC10 | ; bar.cta.sync 1 | LC11: | ; - st.relaxed.gpu f, 0 | bar.cta.sync 1 | ; + st.relaxed.gpu f, 0 | bar.cta.sync 2 | ; | ld.weak r1, x | ; exists (P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/PTX/Manual/XF-Barrier-weak.litmus b/litmus/PTX/Manual/XF-Barrier-weak.litmus index 3c91746c33..5498d138cb 100644 --- a/litmus/PTX/Manual/XF-Barrier-weak.litmus +++ b/litmus/PTX/Manual/XF-Barrier-weak.litmus @@ -9,13 +9,13 @@ P1:r0=0; } P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; st.weak x, 1 | bar.cta.sync 1 | bar.cta.sync 1 ; - LC00: | st.weak f, 1 | bar.cta.sync 1 ; + LC00: | st.weak f, 1 | bar.cta.sync 2 ; ld.weak r2, f | LC10: | ; bne r2, 0, LC01 | ld.weak r2, f | ; goto LC00 | bne r2, 1, LC11 | ; LC01: | goto LC10 | ; bar.cta.sync 1 | LC11: | ; - st.weak f, 0 | bar.cta.sync 1 | ; + st.weak f, 0 | bar.cta.sync 2 | ; | ld.weak r1, x | ; exists (P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus b/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus index a7933581bf..178cc75034 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus @@ -10,13 +10,13 @@ P1:r0=0; } P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; st.av.dv.sc0 x, 1 | cbar.wg 1 | cbar.wg 1 ; - LC00: | st.atom.dv.sc0 f, 1 | cbar.wg 1 ; + LC00: | st.atom.dv.sc0 f, 1 | cbar.wg 2 ; ld.atom.dv.sc0 r2, f | LC10: | ; bne r2, 0, LC01 | ld.atom.acq.dv.sc0.semsc0 r2, f | ; goto LC00 | bne r2, 1, LC11 | ; LC01: | goto LC10 | ; cbar.wg 1 | LC11: | ; - st.atom.rel.dv.sc0.semsc0 f, 0 | cbar.wg 1 | ; + st.atom.rel.dv.sc0.semsc0 f, 0 | cbar.wg 2 | ; | ld.vis.dv.sc0 r1, x | ; exists (P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-rlx.litmus b/litmus/VULKAN/Manual/XF-Barrier-rlx.litmus index 4c07ac952d..559b04b402 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-rlx.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-rlx.litmus @@ -10,13 +10,13 @@ P1:r0=0; } P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; st.av.dv.sc0 x, 1 | cbar.wg 1 | cbar.wg 1 ; - LC00: | st.atom.dv.sc0 f, 1 | cbar.wg 1 ; + LC00: | st.atom.dv.sc0 f, 1 | cbar.wg 2 ; ld.atom.dv.sc0 r2, f | LC10: | ; bne r2, 0, LC01 | ld.atom.dv.sc0 r2, f | ; goto LC00 | bne r2, 1, LC11 | ; LC01: | goto LC10 | ; cbar.wg 1 | LC11: | ; - st.atom.dv.sc0 f, 0 | cbar.wg 1 | ; + st.atom.dv.sc0 f, 0 | cbar.wg 2 | ; | ld.vis.dv.sc0 r1, x | ; exists (P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus index a0e682b69d..cf350d2afa 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus @@ -9,13 +9,13 @@ P1:r0=0; } P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ; st.av.dv.sc0 x, 1 | cbar.wg 1 | cbar.wg 1 ; - LC00: | st.dv.sc0 f, 1 | cbar.wg 1 ; + LC00: | st.dv.sc0 f, 1 | cbar.wg 2 ; ld.dv.sc0 r2, f | LC10: | ; bne r2, 0, LC01 | ld.dv.sc0 r2, f | ; goto LC00 | bne r2, 1, LC11 | ; LC01: | goto LC10 | ; cbar.wg 1 | LC11: | ; - st.dv.sc0 f, 0 | cbar.wg 1 | ; + st.dv.sc0 f, 0 | cbar.wg 2 | ; | ld.vis.dv.sc0 r1, x | ; exists (P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file From b99877dac60863798f240761881df9017487bb44 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 23 Oct 2023 14:57:35 +0200 Subject: [PATCH 16/21] Different barrier id in same thread, new RA variant Signed-off-by: Hernan Ponce de Leon --- .../src/test/resources/PTXv6_0-expected.csv | 5 +++-- .../src/test/resources/PTXv7_5-expected.csv | 5 +++-- litmus/PTX/Manual/XF-Barrier-relacq.litmus | 21 +++++++++++++++++++ litmus/PTX/Manual/XF-Barrier-rlx.litmus | 2 +- litmus/VULKAN/Manual/XF-Barrier-relacq.litmus | 2 +- litmus/VULKAN/Manual/XF-Barrier-rlx.litmus | 2 +- 6 files changed, 30 insertions(+), 7 deletions(-) create mode 100644 litmus/PTX/Manual/XF-Barrier-relacq.litmus diff --git a/dartagnan/src/test/resources/PTXv6_0-expected.csv b/dartagnan/src/test/resources/PTXv6_0-expected.csv index 625b6e9bf8..aea2f67da1 100644 --- a/dartagnan/src/test/resources/PTXv6_0-expected.csv +++ b/dartagnan/src/test/resources/PTXv6_0-expected.csv @@ -58,5 +58,6 @@ litmus/PTX/Manual/LB-dlb-no-fence-2,1 litmus/PTX/Nvidia/SB+bar-dyn-reg-const,0 litmus/PTX/Nvidia/SB+bar-sta-reg-const,1 litmus/PTX/Manual/CoWW-weak.litmus,1 -litmus/PTX/Manual/XF-Barrier-rlx.litmus,0 -litmus/PTX/Manual/XF-Barrier-weak.litmus,0 \ No newline at end of file +litmus/PTX/Manual/XF-Barrier-relacq.litmus,0 +litmus/PTX/Manual/XF-Barrier-rlx.litmus,1 +litmus/PTX/Manual/XF-Barrier-weak.litmus,1 \ No newline at end of file diff --git a/dartagnan/src/test/resources/PTXv7_5-expected.csv b/dartagnan/src/test/resources/PTXv7_5-expected.csv index 8e06a91083..eeca693bca 100644 --- a/dartagnan/src/test/resources/PTXv7_5-expected.csv +++ b/dartagnan/src/test/resources/PTXv7_5-expected.csv @@ -123,5 +123,6 @@ litmus/PTX/Manual/LB-dlb-no-fence-2.litmus,1 litmus/PTX/Nvidia/SB+bar-dyn-reg-const.litmus,0 litmus/PTX/Nvidia/SB+bar-sta-reg-const.litmus,1 litmus/PTX/Manual/CoWW-weak.litmus,1 -litmus/PTX/Manual/XF-Barrier-rlx.litmus,0 -litmus/PTX/Manual/XF-Barrier-weak.litmus,0 \ No newline at end of file +litmus/PTX/Manual/XF-Barrier-relacq.litmus,0 +litmus/PTX/Manual/XF-Barrier-rlx.litmus,1 +litmus/PTX/Manual/XF-Barrier-weak.litmus,1 \ No newline at end of file diff --git a/litmus/PTX/Manual/XF-Barrier-relacq.litmus b/litmus/PTX/Manual/XF-Barrier-relacq.litmus new file mode 100644 index 0000000000..aee7c56261 --- /dev/null +++ b/litmus/PTX/Manual/XF-Barrier-relacq.litmus @@ -0,0 +1,21 @@ +PTX XF-Barrier-relacq +"Adapted from Figure 2 in +Portable Inter-workgroup Barrier Synchronisation for GPUs +https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" +{ +f=0; +P0:r0=0; +P1:r0=0; +} + P0@cta 0,gpu 0 | P1@cta 1,gpu 0 | P2@cta 1,gpu 0 ; + st.weak x, 1 | bar.cta.sync 1 | bar.cta.sync 1 ; + LC00: | st.relaxed.gpu f, 1 | bar.cta.sync 2 ; + ld.relaxed.gpu r2, f | LC10: | ; + bne r2, 0, LC01 | ld.acquire.gpu r2, f | ; + goto LC00 | bne r2, 1, LC11 | ; + LC01: | goto LC10 | ; + bar.cta.sync 1 | LC11: | ; + st.release.gpu f, 0 | bar.cta.sync 2 | ; + | ld.weak r1, x | ; +exists +(P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file diff --git a/litmus/PTX/Manual/XF-Barrier-rlx.litmus b/litmus/PTX/Manual/XF-Barrier-rlx.litmus index a37cc4eac9..d29aeb0c26 100644 --- a/litmus/PTX/Manual/XF-Barrier-rlx.litmus +++ b/litmus/PTX/Manual/XF-Barrier-rlx.litmus @@ -1,4 +1,4 @@ -PTX XF-Barrier-atom +PTX XF-Barrier-rlx "Adapted from Figure 2 in Portable Inter-workgroup Barrier Synchronisation for GPUs https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" diff --git a/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus b/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus index 178cc75034..78edfefc03 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus @@ -1,4 +1,4 @@ -Vulkan XF-Barrier-RA +Vulkan XF-Barrier-relacq "Adapted from Figure 2 in Portable Inter-workgroup Barrier Synchronisation for GPUs https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" diff --git a/litmus/VULKAN/Manual/XF-Barrier-rlx.litmus b/litmus/VULKAN/Manual/XF-Barrier-rlx.litmus index 559b04b402..5114532174 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-rlx.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-rlx.litmus @@ -1,4 +1,4 @@ -Vulkan XF-Barrier-atom +Vulkan XF-Barrier-rlx "Adapted from Figure 2 in Portable Inter-workgroup Barrier Synchronisation for GPUs https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" From ee1b6ca8d8e49ef93536a916c02eca5e19da273a Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 23 Oct 2023 16:20:26 +0200 Subject: [PATCH 17/21] Add cause-base to the definition of cause Signed-off-by: Hernan Ponce de Leon --- cat/ptx-v7.5.cat | 2 +- litmus/PTX/Manual/MP-cause-base.litmus | 16 ++++++++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 litmus/PTX/Manual/MP-cause-base.litmus diff --git a/cat/ptx-v7.5.cat b/cat/ptx-v7.5.cat index b1701d36b9..7443f1d2e9 100644 --- a/cat/ptx-v7.5.cat +++ b/cat/ptx-v7.5.cat @@ -81,7 +81,7 @@ let proxy-preserved-cause-base | loc & (cause-base & (proxy-fence-ops^-1); cause-base; [F & ALIAS]; cause-base; [GEN]) | loc & ([GEN]; cause-base; [F & ALIAS]; cause-base; cause-base & proxy-fence-ops) | loc & (cause-base & (proxy-fence-ops^-1); cause-base; [F & ALIAS]; cause-base; cause-base & proxy-fence-ops) -let cause = observation?; proxy-preserved-cause-base +let cause = cause-base | (observation?; proxy-preserved-cause-base) (******************************) (* PTX Memory Model Axioms *) diff --git a/litmus/PTX/Manual/MP-cause-base.litmus b/litmus/PTX/Manual/MP-cause-base.litmus new file mode 100644 index 0000000000..0786e1cf39 --- /dev/null +++ b/litmus/PTX/Manual/MP-cause-base.litmus @@ -0,0 +1,16 @@ +PTX MP-cause-base +"Causality should be cause-base | (observation; ...) " +{ +x=0; +f=0; +P0:r0=0; +P1:r0=0; +} + P0@cta 0,gpu 0 | P1@cta 1,gpu 0 ; + st.weak x, 1 | bar.cta.sync 1 ; + st.release.gpu f, 0 | st.relaxed.gpu f, 1 ; + | ld.acquire.gpu r2, f ; + | bar.cta.sync 2 ; + | ld.weak r1, x ; +exists +(P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file From ab9b6a2da434359c974a6ee7cbb16d953e71507a Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 23 Oct 2023 16:21:29 +0200 Subject: [PATCH 18/21] Initialize x in XF-Barrier Signed-off-by: Hernan Ponce de Leon --- litmus/PTX/Manual/XF-Barrier-relacq.litmus | 1 + litmus/PTX/Manual/XF-Barrier-rlx.litmus | 1 + litmus/PTX/Manual/XF-Barrier-weak.litmus | 1 + litmus/VULKAN/Manual/XF-Barrier-weak.litmus | 1 + 4 files changed, 4 insertions(+) diff --git a/litmus/PTX/Manual/XF-Barrier-relacq.litmus b/litmus/PTX/Manual/XF-Barrier-relacq.litmus index aee7c56261..c813c51dd7 100644 --- a/litmus/PTX/Manual/XF-Barrier-relacq.litmus +++ b/litmus/PTX/Manual/XF-Barrier-relacq.litmus @@ -3,6 +3,7 @@ PTX XF-Barrier-relacq Portable Inter-workgroup Barrier Synchronisation for GPUs https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" { +x=0; f=0; P0:r0=0; P1:r0=0; diff --git a/litmus/PTX/Manual/XF-Barrier-rlx.litmus b/litmus/PTX/Manual/XF-Barrier-rlx.litmus index d29aeb0c26..cfa60dbbba 100644 --- a/litmus/PTX/Manual/XF-Barrier-rlx.litmus +++ b/litmus/PTX/Manual/XF-Barrier-rlx.litmus @@ -3,6 +3,7 @@ PTX XF-Barrier-rlx Portable Inter-workgroup Barrier Synchronisation for GPUs https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" { +x=0; f=0; P0:r0=0; P1:r0=0; diff --git a/litmus/PTX/Manual/XF-Barrier-weak.litmus b/litmus/PTX/Manual/XF-Barrier-weak.litmus index 5498d138cb..8c45b8de82 100644 --- a/litmus/PTX/Manual/XF-Barrier-weak.litmus +++ b/litmus/PTX/Manual/XF-Barrier-weak.litmus @@ -3,6 +3,7 @@ PTX XF-Barrier-weak Portable Inter-workgroup Barrier Synchronisation for GPUs https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" { +x=0; f=0; P0:r0=0; P1:r0=0; diff --git a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus index cf350d2afa..9d7497a6b2 100644 --- a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus +++ b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus @@ -3,6 +3,7 @@ Vulkan XF-Barrier-weak Portable Inter-workgroup Barrier Synchronisation for GPUs https://dl.acm.org/doi/pdf/10.1145/2983990.2984032" { +x=0; f=0; P0:r0=0; P1:r0=0; From 079e093f033e88b8cab9eef9a7ea0d6f9f4f1ee7 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 23 Oct 2023 17:40:13 +0200 Subject: [PATCH 19/21] cause-base -> proxy-preserved-cause-base Signed-off-by: Hernan Ponce de Leon --- cat/ptx-v7.5.cat | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cat/ptx-v7.5.cat b/cat/ptx-v7.5.cat index 7443f1d2e9..6d53d3ba66 100644 --- a/cat/ptx-v7.5.cat +++ b/cat/ptx-v7.5.cat @@ -81,7 +81,7 @@ let proxy-preserved-cause-base | loc & (cause-base & (proxy-fence-ops^-1); cause-base; [F & ALIAS]; cause-base; [GEN]) | loc & ([GEN]; cause-base; [F & ALIAS]; cause-base; cause-base & proxy-fence-ops) | loc & (cause-base & (proxy-fence-ops^-1); cause-base; [F & ALIAS]; cause-base; cause-base & proxy-fence-ops) -let cause = cause-base | (observation?; proxy-preserved-cause-base) +let cause = proxy-preserved-cause-base | (observation?; proxy-preserved-cause-base) (******************************) (* PTX Memory Model Axioms *) From d7fb61f709c9f147035169811657d9f32d1f330a Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 23 Oct 2023 20:32:45 +0200 Subject: [PATCH 20/21] Revert change to the definition of cause in PTX v7.5 Signed-off-by: Hernan Ponce de Leon --- cat/ptx-v7.5.cat | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cat/ptx-v7.5.cat b/cat/ptx-v7.5.cat index 6d53d3ba66..b1701d36b9 100644 --- a/cat/ptx-v7.5.cat +++ b/cat/ptx-v7.5.cat @@ -81,7 +81,7 @@ let proxy-preserved-cause-base | loc & (cause-base & (proxy-fence-ops^-1); cause-base; [F & ALIAS]; cause-base; [GEN]) | loc & ([GEN]; cause-base; [F & ALIAS]; cause-base; cause-base & proxy-fence-ops) | loc & (cause-base & (proxy-fence-ops^-1); cause-base; [F & ALIAS]; cause-base; cause-base & proxy-fence-ops) -let cause = proxy-preserved-cause-base | (observation?; proxy-preserved-cause-base) +let cause = observation?; proxy-preserved-cause-base (******************************) (* PTX Memory Model Axioms *) From 4f6d237984d4a15794aa5c39ab2f147d423f1c89 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 23 Oct 2023 20:34:26 +0200 Subject: [PATCH 21/21] Remove unneeded test Signed-off-by: Hernan Ponce de Leon --- litmus/PTX/Manual/MP-cause-base.litmus | 16 ---------------- 1 file changed, 16 deletions(-) delete mode 100644 litmus/PTX/Manual/MP-cause-base.litmus diff --git a/litmus/PTX/Manual/MP-cause-base.litmus b/litmus/PTX/Manual/MP-cause-base.litmus deleted file mode 100644 index 0786e1cf39..0000000000 --- a/litmus/PTX/Manual/MP-cause-base.litmus +++ /dev/null @@ -1,16 +0,0 @@ -PTX MP-cause-base -"Causality should be cause-base | (observation; ...) " -{ -x=0; -f=0; -P0:r0=0; -P1:r0=0; -} - P0@cta 0,gpu 0 | P1@cta 1,gpu 0 ; - st.weak x, 1 | bar.cta.sync 1 ; - st.release.gpu f, 0 | st.relaxed.gpu f, 1 ; - | ld.acquire.gpu r2, f ; - | bar.cta.sync 2 ; - | ld.weak r1, x ; -exists -(P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file