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/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/antlr4/LitmusVulkan.g4 b/dartagnan/src/main/antlr4/LitmusVulkan.g4 index 26b03ad14f..25507017b3 100644 --- a/dartagnan/src/main/antlr4/LitmusVulkan.g4 +++ b/dartagnan/src/main/antlr4/LitmusVulkan.g4 @@ -108,12 +108,32 @@ storeInstruction ; loadInstruction - : localConstant + : localValue + | localAdd + | localSub + | localMul + | localDiv | 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 + ; + +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 @@ -121,16 +141,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 +176,7 @@ label ; branchCond - : cond register Comma register Comma Label + : cond value Comma value Comma Label ; jump @@ -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/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)); } 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..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 @@ -207,10 +207,46 @@ 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 + 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 @@ -244,10 +280,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 +291,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 +300,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 +312,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 +393,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)); } 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/dartagnan/src/test/resources/PTXv6_0-expected.csv b/dartagnan/src/test/resources/PTXv6_0-expected.csv index b07d6dd039..aea2f67da1 100644 --- a/dartagnan/src/test/resources/PTXv6_0-expected.csv +++ b/dartagnan/src/test/resources/PTXv6_0-expected.csv @@ -58,3 +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-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 0f3fba15a6..eeca693bca 100644 --- a/dartagnan/src/test/resources/PTXv7_5-expected.csv +++ b/dartagnan/src/test/resources/PTXv7_5-expected.csv @@ -123,3 +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-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/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 diff --git a/litmus/PTX/Manual/XF-Barrier-relacq.litmus b/litmus/PTX/Manual/XF-Barrier-relacq.litmus new file mode 100644 index 0000000000..c813c51dd7 --- /dev/null +++ b/litmus/PTX/Manual/XF-Barrier-relacq.litmus @@ -0,0 +1,22 @@ +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" +{ +x=0; +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 new file mode 100644 index 0000000000..cfa60dbbba --- /dev/null +++ b/litmus/PTX/Manual/XF-Barrier-rlx.litmus @@ -0,0 +1,22 @@ +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" +{ +x=0; +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.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 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 new file mode 100644 index 0000000000..8c45b8de82 --- /dev/null +++ b/litmus/PTX/Manual/XF-Barrier-weak.litmus @@ -0,0 +1,22 @@ +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" +{ +x=0; +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.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 2 | ; + | ld.weak r1, x | ; +exists +(P1:r2 != 1 /\ P1:r1 == 0) \ No newline at end of file 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 | ; diff --git a/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus b/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus new file mode 100644 index 0000000000..78edfefc03 --- /dev/null +++ b/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus @@ -0,0 +1,22 @@ +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" +{ +x=0; +f=0; +P0:r0=0; +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 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 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 new file mode 100644 index 0000000000..5114532174 --- /dev/null +++ b/litmus/VULKAN/Manual/XF-Barrier-rlx.litmus @@ -0,0 +1,22 @@ +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" +{ +x=0; +f=0; +P0:r0=0; +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 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 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 new file mode 100644 index 0000000000..9d7497a6b2 --- /dev/null +++ b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus @@ -0,0 +1,22 @@ +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" +{ +x=0; +f=0; +P0:r0=0; +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 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 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/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