From a2297d606807975c8e5c8678f7ecf3c21563e8e4 Mon Sep 17 00:00:00 2001 From: haining Date: Sun, 8 Oct 2023 12:51:03 +0300 Subject: [PATCH 1/5] remove scope of weak instructions --- .../program/visitors/VisitorLitmusPTX.java | 25 ++++++++----------- 1 file changed, 10 insertions(+), 15 deletions(-) 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 2998b6cfdc..8e67a35f13 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 @@ -142,19 +142,18 @@ public Object visitStoreConstant(LitmusPTXParser.StoreConstantContext ctx) { MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText()); IConst constant = (IConst) ctx.constant().accept(this); String mo = ctx.mo().content; - String scope; + Store store = EventFactory.newStoreWithMo(object, constant, mo); switch (mo) { case Tag.PTX.WEAK -> { if (ctx.scope() != null) { throw new ParsingException("Weak store instruction doesn't need scope: " + ctx.scope().content); } - scope = Tag.PTX.SYS; + store.addTags(Tag.PTX.CON); } - case Tag.PTX.REL, Tag.PTX.RLX -> 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 store = EventFactory.newStoreWithMo(object, constant, mo); - store.addTags(scope, ctx.store().storeProxy, Tag.PTX.CON); + store.addTags(ctx.store().storeProxy); return programBuilder.addChild(mainThread, store); } @@ -163,19 +162,17 @@ public Object visitStoreRegister(LitmusPTXParser.StoreRegisterContext ctx) { MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText()); Register register = (Register) ctx.register().accept(this); String mo = ctx.mo().content; - String scope; + 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); } - scope = Tag.PTX.SYS; } - case Tag.PTX.REL, Tag.PTX.RLX -> 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 store = EventFactory.newStoreWithMo(object, register, mo); - store.addTags(scope, ctx.store().storeProxy); + store.addTags(ctx.store().storeProxy); return programBuilder.addChild(mainThread, store); } @@ -227,19 +224,17 @@ public Object visitLoadLocation(LitmusPTXParser.LoadLocationContext ctx) { Register register = (Register) ctx.register().accept(this); MemoryObject location = programBuilder.getOrNewMemoryObject(ctx.location().getText()); String mo = ctx.mo().content; - String scope; + Load load = EventFactory.newLoadWithMo(register, location, mo); switch (mo) { case Tag.PTX.WEAK -> { if (ctx.scope() != null) { throw new ParsingException("Weak load instruction doesn't need scope: " + ctx.scope().content); } - scope = Tag.PTX.SYS; } - case Tag.PTX.ACQ, Tag.PTX.RLX -> scope = ctx.scope().content; + case Tag.PTX.ACQ, Tag.PTX.RLX -> load.addTags(ctx.scope().content); default -> throw new ParsingException("Load instruction doesn't support mo: " + mo); } - Load load = EventFactory.newLoadWithMo(register, location, mo); - load.addTags(scope, ctx.load().loadProxy); + load.addTags(ctx.load().loadProxy); return programBuilder.addChild(mainThread, load); } From 0fe9303252550c41633becc43d9d74bc65fb3818 Mon Sep 17 00:00:00 2001 From: haining Date: Sun, 8 Oct 2023 15:43:50 +0300 Subject: [PATCH 2/5] remove constant proxy cause --- cat/ptx-v7.5.cat | 2 -- litmus/PTX/Nvidia/Proxy-Const-ConstFence.litmus | 2 +- litmus/PTX/Nvidia/Proxy-Const-MP-cause1.litmus | 2 +- litmus/PTX/Nvidia/Proxy-Const-MP-cause2.litmus | 2 +- .../PTX/Nvidia/Proxy-SingleThread-rf-surW-surF-conF-conR.litmus | 2 +- 5 files changed, 4 insertions(+), 6 deletions(-) diff --git a/cat/ptx-v7.5.cat b/cat/ptx-v7.5.cat index 58868482f0..b1701d36b9 100644 --- a/cat/ptx-v7.5.cat +++ b/cat/ptx-v7.5.cat @@ -77,8 +77,6 @@ let proxy-preserved-cause-base | vloc & (cause-base & (proxy-fence-ops^-1); cause-base; [GEN]) | vloc & ([GEN]; cause-base; cause-base & proxy-fence-ops) | vloc & (cause-base & (proxy-fence-ops^-1); cause-base; cause-base & proxy-fence-ops) - // The alloy model does not support the constant proxy below - | loc & ([M & CON]; cause-base; [F & CON]; cause-base; [M & CON]) | loc & ([GEN]; cause-base; [F & ALIAS]; cause-base; [GEN]) | 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) diff --git a/litmus/PTX/Nvidia/Proxy-Const-ConstFence.litmus b/litmus/PTX/Nvidia/Proxy-Const-ConstFence.litmus index f418f110ea..0888d86466 100644 --- a/litmus/PTX/Nvidia/Proxy-Const-ConstFence.litmus +++ b/litmus/PTX/Nvidia/Proxy-Const-ConstFence.litmus @@ -2,7 +2,7 @@ PTX Proxy-Const-with-ConstFence "A single thread example showing constant proxy fence usage" { rd1 = 0; -rd2 @ generic aliases rd1; +rd2 @ constant aliases rd1; P0:r0=0; } P0@cta 0,gpu 0 ; diff --git a/litmus/PTX/Nvidia/Proxy-Const-MP-cause1.litmus b/litmus/PTX/Nvidia/Proxy-Const-MP-cause1.litmus index 3fdeeac60a..3f67de9638 100644 --- a/litmus/PTX/Nvidia/Proxy-Const-MP-cause1.litmus +++ b/litmus/PTX/Nvidia/Proxy-Const-MP-cause1.litmus @@ -3,7 +3,7 @@ PTX Proxy-Const-MP-cause1 "The constant fence along the base causality path from the weak st to the cold, hence rf is guaranteed" { rd1 = 0; -rd2 @ generic aliases rd1; +rd2 @ constant aliases rd1; rd4 = 0; P0:r0=0; } diff --git a/litmus/PTX/Nvidia/Proxy-Const-MP-cause2.litmus b/litmus/PTX/Nvidia/Proxy-Const-MP-cause2.litmus index e086fd0a8c..cefbfb6f6d 100644 --- a/litmus/PTX/Nvidia/Proxy-Const-MP-cause2.litmus +++ b/litmus/PTX/Nvidia/Proxy-Const-MP-cause2.litmus @@ -3,7 +3,7 @@ PTX Proxy-Const-MP-cause2 "The constant fence along the base causality path from the weak st to the cold, hence rf is guaranteed" { rd1 = 0; -rd2 @ generic aliases rd1; +rd2 @ constant aliases rd1; rd4 = 0; P1:r3=0; P1:r5=0; diff --git a/litmus/PTX/Nvidia/Proxy-SingleThread-rf-surW-surF-conF-conR.litmus b/litmus/PTX/Nvidia/Proxy-SingleThread-rf-surW-surF-conF-conR.litmus index f1fc67f8ae..80d05480df 100644 --- a/litmus/PTX/Nvidia/Proxy-SingleThread-rf-surW-surF-conF-conR.litmus +++ b/litmus/PTX/Nvidia/Proxy-SingleThread-rf-surW-surF-conF-conR.litmus @@ -3,7 +3,7 @@ PTX Proxy-SingleThread-rf-surW-surF-conF-conR "The generic memory is synchronize with surface cache by surface fence, then constant fence synchronize the data from generic memory to constant cache. Hence the cold is guaranteed to rf sust" { rd1 = 0; -rd2 @ generic aliases rd1; +rd2 @ constant aliases rd1; rd3 @ surface aliases rd1; P0:r0=0; } From a1c47e3c3b3326499b248c5f959e379d91dbc6d2 Mon Sep 17 00:00:00 2001 From: Haining Date: Mon, 9 Oct 2023 12:50:58 +0300 Subject: [PATCH 3/5] remove CON tag from visitStoreConstant() --- .../dartagnan/parsers/program/visitors/VisitorLitmusPTX.java | 1 - 1 file changed, 1 deletion(-) 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 8e67a35f13..40a1c1cf84 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 @@ -148,7 +148,6 @@ public Object visitStoreConstant(LitmusPTXParser.StoreConstantContext ctx) { if (ctx.scope() != null) { throw new ParsingException("Weak store instruction doesn't need scope: " + ctx.scope().content); } - store.addTags(Tag.PTX.CON); } case Tag.PTX.REL, Tag.PTX.RLX -> store.addTags(ctx.scope().content); default -> throw new ParsingException("Store instruction doesn't support mo: " + mo); From f55be5f7e013ae4601fdb5f05cc3bb32c6cea4bb Mon Sep 17 00:00:00 2001 From: haining Date: Wed, 11 Oct 2023 18:42:27 +0300 Subject: [PATCH 4/5] remove unused w-locord --- cat/spirv.cat | 2 -- 1 file changed, 2 deletions(-) diff --git a/cat/spirv.cat b/cat/spirv.cat index d46758d168..e94382b535 100644 --- a/cat/spirv.cat +++ b/cat/spirv.cat @@ -129,8 +129,6 @@ let locord = loc & ( ([W]; (hb & avvisinc); avdv; (hb); visdv; (hb & avvisinc); [R])) // RaW (via device domain) ) -let w-locord = [W]; locord - (***********************) (* Memory Model Axioms *) (***********************) From f978c91ac598eb5caf5cb45acae2bb85824f843b Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sun, 22 Oct 2023 17:41:44 +0200 Subject: [PATCH 5/5] Remove w-locord from nochains version Signed-off-by: Hernan Ponce de Leon --- cat/spirv-nochains.cat | 2 -- 1 file changed, 2 deletions(-) diff --git a/cat/spirv-nochains.cat b/cat/spirv-nochains.cat index 89941c8c89..0607eab516 100644 --- a/cat/spirv-nochains.cat +++ b/cat/spirv-nochains.cat @@ -129,8 +129,6 @@ let locord = loc & ( ([W]; (hb & avvisinc); avdv; (hb); visdv; (hb & avvisinc); [R])) // RaW (via device domain) ) -let w-locord = [W]; locord - (***********************) (* Memory Model Axioms *) (***********************)