Merge branch 'development' into liveness

hernanponcedeleon · Oct 23, 2023 · 9d2c9b5 · 9d2c9b5
2 parents 24e3ec9 + a0ce1fb
commit 9d2c9b5
Show file tree

Hide file tree

Showing 36 changed files with 664 additions and 197 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-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/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/antlr4/LitmusPTX.g4 b/dartagnan/src/main/antlr4/LitmusPTX.g4
@@ -94,45 +94,36 @@ 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
     |   localDiv
     |   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,18 +155,13 @@ barrier
     ;
 
 atomInstruction
-    :   atomConstant
-    |   atomRegister
+    :   atomOp
     |   atomCAS
     |   atomExchange
     ;
 
-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
@@ -187,20 +173,11 @@ atomExchange
     ;
 
 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 value 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
@@ -108,29 +108,49 @@ 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
     :   Load atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList register Comma location
     ;
 
 rmwInstruction
-    :   rmwExch
+    :   rmwValue
     |   rmwOp
     ;
 
-rmwExch
+rmwValue
     :   RMW atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList register Comma location Comma value
     ;
 
 rmwOp
-    :   RMW atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList operation register Comma location Comma constant
+    :   RMW atomic mo? avvis? scope? storageClass storageClassSemanticList avvisSemanticList operation register Comma location Comma value
     ;
 
 fenceInstruction
@@ -156,7 +176,7 @@ label
     ;
 
 branchCond
-    :   cond register Comma value 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';