Support for barrier invariants.

1 files changed, 157 insertions, 2 deletions

diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs
index 201018bb..526e39a0 100644
--- a/Source/GPUVerify/KernelDualiser.cs
+++ b/Source/GPUVerify/KernelDualiser.cs
@@ -9,10 +9,13 @@ using Microsoft.Basetypes;
 

 namespace GPUVerify {

   class KernelDualiser {

-    private GPUVerifier verifier;

+    internal GPUVerifier verifier;

+

+    private List<BarrierInvariantDescriptor> BarrierInvariantDescriptors;

 

     public KernelDualiser(GPUVerifier verifier) {

       this.verifier = verifier;

+      BarrierInvariantDescriptors = new List<BarrierInvariantDescriptor>();

     }

 

     private string procName = null;

@@ -74,7 +77,7 @@ namespace GPUVerify {
       return result;

     }

 

-    private QKeyValue MakeThreadSpecificAttributes(QKeyValue attributes, int Thread) {

+    internal QKeyValue MakeThreadSpecificAttributes(QKeyValue attributes, int Thread) {

       if (attributes == null) {

         return null;

       }

@@ -100,6 +103,41 @@ namespace GPUVerify {
       if (c is CallCmd) {

         CallCmd Call = c as CallCmd;

 

+        if (QKeyValue.FindBoolAttribute(Call.Proc.Attributes, "barrier_invariant")) {

+          // There should be a predicate, an invariant expression, and at least one instantiation

+          Debug.Assert(Call.Ins.Count >= 3);

+          var BIDescriptor = new UnaryBarrierInvariantDescriptor(Call.Ins[0],
+            Expr.Neq(Call.Ins[1], 
+              new LiteralExpr(Token.NoToken, BigNum.FromInt(0), 1)), this);

+          for (var i = 2; i < Call.Ins.Count; i++) {

+            BIDescriptor.AddInstantiationExpr(Call.Ins[i]);

+          }

+          BarrierInvariantDescriptors.Add(BIDescriptor);

+          return;

+        }

+

+        if (QKeyValue.FindBoolAttribute(Call.Proc.Attributes, "binary_barrier_invariant")) {

+          // There should be a predicate, an invariant expression, and at least one pair of

+          // instantiation expressions

+          Debug.Assert(Call.Ins.Count >= 4);

+          var BIDescriptor = new BinaryBarrierInvariantDescriptor(Call.Ins[0],

+            Expr.Neq(Call.Ins[1],

+              new LiteralExpr(Token.NoToken, BigNum.FromInt(0), 1)), this);

+          for (var i = 2; i < Call.Ins.Count; i += 2) {

+            BIDescriptor.AddInstantiationExprPair(Call.Ins[i], Call.Ins[i + 1]);

+          }

+          BarrierInvariantDescriptors.Add(BIDescriptor);

+          return;

+        }

+

+

+        if (Call.callee.Equals(verifier.BarrierProcedure.Name)) {

+          // Assert barrier invariants

+          foreach (var BIDescriptor in BarrierInvariantDescriptors) {

+            cs.Add(BIDescriptor.GetAssertCmd(Call.Attributes));

+          }

+        }

+

         List<Expr> uniformNewIns = new List<Expr>();

         List<Expr> nonUniformNewIns = new List<Expr>();

         for (int i = 0; i < Call.Ins.Count; i++) {

@@ -148,6 +186,16 @@ namespace GPUVerify {
         NewCallCmd.Attributes = Call.Attributes;

 

         cs.Add(NewCallCmd);

+

+        if (Call.callee.Equals(verifier.BarrierProcedure.Name)) {

+          foreach (var BIDescriptor in BarrierInvariantDescriptors) {

+            foreach (var Instantiation in BIDescriptor.GetInstantiationCmds()) {

+              cs.Add(Instantiation);

+            }

+          }

+          BarrierInvariantDescriptors.Clear();

+        }

+

       }

       else if (c is AssignCmd) {

         AssignCmd assign = c as AssignCmd;

@@ -370,4 +418,111 @@ namespace GPUVerify {
 

   }

 

+  class ThreadInstantiator : Duplicator {

+

+    private GPUVerifier verifier;

+    private Expr InstantiationExpr;

+    private int Thread;

+

+    internal ThreadInstantiator(GPUVerifier verifier, Expr InstantiationExpr, int Thread) {

+      this.verifier = verifier;

+      this.InstantiationExpr = InstantiationExpr;

+      this.Thread = Thread;

+    }

+

+    public override Expr VisitIdentifierExpr(IdentifierExpr node) {

+      Debug.Assert(!(node.Decl is Formal));

+

+      if (GPUVerifier.IsThreadLocalIdConstant(node.Decl)) {

+        Debug.Assert(node.Decl.Name.Equals(GPUVerifier._X.Name));

+        return InstantiationExpr.Clone() as Expr;

+      }

+

+      Debug.Assert(node.Decl is Constant ||

+        verifier.KernelArrayInfo.getGroupSharedArrays().Contains(node.Decl) ||

+        verifier.KernelArrayInfo.getGlobalArrays().Contains(node.Decl));

+

+      return base.VisitIdentifierExpr(node);

+    }

+

+    public override Expr VisitNAryExpr(NAryExpr node) {

+      if (node.Fun is MapSelect) {

+        Debug.Assert((node.Fun as MapSelect).Arity == 1);

+        Debug.Assert(node.Args[0] is IdentifierExpr);

+        var v = (node.Args[0] as IdentifierExpr).Decl;

+        if (QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {

+          return new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),

+            new ExprSeq(new Expr[] { new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), 

+              new ExprSeq(new Expr[] { node.Args[0], GPUVerifier.GroupSharedIndexingExpr(Thread) })), VisitExpr(node.Args[1]) }));

+        }

+      }

+      return base.VisitNAryExpr(node);

+    }

+

+

+  }

+

+

+

+  class ThreadPairInstantiator : Duplicator {

+

+    private GPUVerifier verifier;

+    private Tuple<Expr, Expr> InstantiationExprs;

+    private int Thread;

+

+    internal ThreadPairInstantiator(GPUVerifier verifier, Expr InstantiationExpr1, Expr InstantiationExpr2, int Thread) {

+      this.verifier = verifier;

+      this.InstantiationExprs = new Tuple<Expr, Expr>(InstantiationExpr1, InstantiationExpr2);

+      this.Thread = Thread;

+    }

+

+    public override Expr VisitIdentifierExpr(IdentifierExpr node) {

+      Debug.Assert(!(node.Decl is Formal));

+

+      if (GPUVerifier.IsThreadLocalIdConstant(node.Decl)) {

+        Debug.Assert(node.Decl.Name.Equals(GPUVerifier._X.Name));

+        return InstantiationExprs.Item1.Clone() as Expr;

+      }

+

+      Debug.Assert(node.Decl is Constant ||

+        verifier.KernelArrayInfo.getGroupSharedArrays().Contains(node.Decl) ||

+        verifier.KernelArrayInfo.getGlobalArrays().Contains(node.Decl));

+

+      return base.VisitIdentifierExpr(node);

+    }

+

+    public override Expr VisitNAryExpr(NAryExpr node) {

+      if (node.Fun is MapSelect) {

+        Debug.Assert((node.Fun as MapSelect).Arity == 1);

+        Debug.Assert(node.Args[0] is IdentifierExpr);

+        var v = (node.Args[0] as IdentifierExpr).Decl;

+

+        if (QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {

+          return new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),

+            new ExprSeq(new Expr[] { new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), 

+              new ExprSeq(new Expr[] { node.Args[0], GPUVerifier.GroupSharedIndexingExpr(Thread) })), VisitExpr(node.Args[1]) }));

+        }

+      }

+

+      if (node.Fun is FunctionCall) {

+        FunctionCall call = node.Fun as FunctionCall;

+

+        // Alternate instantiation order for "other thread" functions.

+        // Note that we do not alternatve the "Thread" field, as we are not switching the

+        // thread for which instantiation is being performed

+        if (VariableDualiser.otherFunctionNames.Contains(call.Func.Name)) {

+          return new ThreadPairInstantiator(verifier, InstantiationExprs.Item2, InstantiationExprs.Item1, Thread)

+            .VisitExpr(node.Args[0]);

+        }

+

+      }

+

+      return base.VisitNAryExpr(node);

+    }

+

+

+  }

+

+

+

 }