Improvements to GPU grammars + new benchmark

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

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,38 +155,24 @@ 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
     :   atom Period mo Period scope Period Cas register Comma location Comma value Comma value
     ;
 
 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

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
-    :   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';

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));
     }