Update Ptx constant-proxy rule (#531)

* remove scope of weak instructions * remove constant proxy cause * remove CON tag from visitStoreConstant() * remove unused w-locord
hernanponcedeleon · Oct 22, 2023 · 469233c · 469233c
1 parent 00045b2
commit 469233c
Show file tree

Hide file tree

Showing 8 changed files with 13 additions and 25 deletions.
diff --git 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/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 *)
 (***********************)

diff --git 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 *)
 (***********************)

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
@@ -142,19 +142,17 @@ 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;
             }
-            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 +161,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 +223,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);
     }
 

diff --git 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
@@ -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
@@ -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
@@ -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;
 }