Dualisation modified so that global arrays are not dualised, and group-shared

arrays are turned into 2D maps with first index type bool.  Thread 1 always
indexes into "true", while threads 2 indexes into "samegroup" (a formula which
is true iff threads 1 and 2 are in the same group).  Thus if the threads are in
different groups they operate on different shared arrays, but if they are in the
same group they operate on the same shared array.  This paves the way for
implementing support for barrier invariants.

3 files changed, 119 insertions, 97 deletions

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 7e1c9370..26dffc0f 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -834,25 +834,25 @@ namespace GPUVerify
 

         

 

-        public Microsoft.Boogie.Type GetTypeOfIdX()

+        public static Microsoft.Boogie.Type GetTypeOfIdX()

         {

             Contract.Requires(_X != null);

             return _X.TypedIdent.Type;

         }

 

-        public Microsoft.Boogie.Type GetTypeOfIdY()

+        public static Microsoft.Boogie.Type GetTypeOfIdY()

         {

             Contract.Requires(_Y != null);

             return _Y.TypedIdent.Type;

         }

 

-        public Microsoft.Boogie.Type GetTypeOfIdZ()

+        public static Microsoft.Boogie.Type GetTypeOfIdZ()

         {

             Contract.Requires(_Z != null);

             return _Z.TypedIdent.Type;

         }

 

-        public Microsoft.Boogie.Type GetTypeOfId(string dimension)

+        public static Microsoft.Boogie.Type GetTypeOfId(string dimension)

         {

             Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));

             if (dimension.Equals("X")) return GetTypeOfIdX();

@@ -1060,7 +1060,7 @@ namespace GPUVerify
 

         }

 

-        internal Expr ThreadsInSameGroup()

+        internal static Expr ThreadsInSameGroup()

         {

             return Expr.And(

                                         Expr.And(

@@ -1297,7 +1297,7 @@ namespace GPUVerify
             return new Constant(tok, new TypedIdent(tok, resultWithoutThreadId.Name + "$" + number, GetTypeOfId(dimension)));

         }

 

-        internal Constant GetGroupId(string dimension)

+        internal static Constant GetGroupId(string dimension)

         {

             Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));

             if (dimension.Equals("X")) return _GROUP_X;

@@ -1307,7 +1307,7 @@ namespace GPUVerify
             return null;

         }

 

-        internal Constant MakeGroupId(string dimension, int number)

+        internal static Constant MakeGroupId(string dimension, int number)

         {

             Constant resultWithoutThreadId = GetGroupId(dimension);

             return new Constant(Token.NoToken, new TypedIdent(Token.NoToken, resultWithoutThreadId.Name + "$" + number, GetTypeOfId(dimension)));

@@ -1367,11 +1367,13 @@ namespace GPUVerify
                 Expr IfGuard2 = Expr.And(P2, LocalFence2);

 

                 bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),

-                    new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),

+                    new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetBlocks(1, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),

                     null));

                 bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),

-                    new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetAndHavocBlocks(2, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),

+                    new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetBlocks(2, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),

                     null));

+

+                bigblocks.AddRange(MakeHavocBlocks(KernelArrayInfo.getGroupSharedArrays()));

             }

 

             if (KernelArrayInfo.getGlobalArrays().Count > 0)

@@ -1380,19 +1382,13 @@ namespace GPUVerify
                 Expr IfGuard2 = Expr.And(P2, GlobalFence2);

 

                 bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),

-                    new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),

+                    new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetBlocks(1, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),

                     null));

                 bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),

-                    new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetAndHavocBlocks(2, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),

+                    new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetBlocks(2, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),

                     null));

-            }

 

-            foreach (Variable v in KernelArrayInfo.getAllNonLocalArrays())

-            {

-                if (!ArrayModelledAdversarially(v))

-                {

-                    bigblocks.Add(AssumeEqualityBetweenSharedArrays(v, P1, P2, LocalFence1, LocalFence2, GlobalFence1, GlobalFence2));

-                }

+                bigblocks.AddRange(MakeHavocBlocks(KernelArrayInfo.getGlobalArrays()));

             }

 

             StmtList statements = new StmtList(bigblocks, BarrierProcedure.tok);

@@ -1423,22 +1419,28 @@ namespace GPUVerify
                                     new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 1));

         }

 

-        private List<BigBlock> MakeResetAndHavocBlocks(int Thread, ICollection<Variable> variables)

+        private List<BigBlock> MakeResetBlocks(int Thread, ICollection<Variable> variables)

         {

             Debug.Assert(variables.Count > 0);

             List<BigBlock> ResetAndHavocBlocks = new List<BigBlock>();

             foreach (Variable v in variables)

             {

                 ResetAndHavocBlocks.Add(RaceInstrumenter.MakeResetReadWriteSetStatements(v, Thread));

-                if (!ArrayModelledAdversarially(v))

-                {

-                    ResetAndHavocBlocks.Add(HavocSharedArray(v, Thread));

-                }

             }

             Debug.Assert(ResetAndHavocBlocks.Count > 0);

             return ResetAndHavocBlocks;

         }

 

+        private List<BigBlock> MakeHavocBlocks(ICollection<Variable> variables) {

+          Debug.Assert(variables.Count > 0);

+          List<BigBlock> result = new List<BigBlock>();

+          foreach (Variable v in variables) {

+            if (!ArrayModelledAdversarially(v)) {

+              result.Add(HavocSharedArray(v));

+            }

+          }

+          return result;

+        }

 

         public static bool HasZDimension(Variable v)

         {

@@ -1459,38 +1461,13 @@ namespace GPUVerify
             return false;

         }

 

-        private BigBlock HavocSharedArray(Variable v, int thread)

+        private BigBlock HavocSharedArray(Variable v)

         {

-            IdentifierExpr vForThread = new IdentifierExpr(Token.NoToken, new VariableDualiser(thread, null, null).VisitVariable(v.Clone() as Variable));

-            return new BigBlock(Token.NoToken, null, new CmdSeq(new Cmd[] { new HavocCmd(Token.NoToken, new IdentifierExprSeq(new IdentifierExpr[] { vForThread })) }), null, null);

-        }

-

-        private BigBlock AssumeEqualityBetweenSharedArrays(Variable v, Expr P1, Expr P2, Expr LocalFence1, Expr LocalFence2, Expr GlobalFence1, Expr GlobalFence2)

-        {

-            IdentifierExpr v1 = new IdentifierExpr(Token.NoToken, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));

-            IdentifierExpr v2 = new IdentifierExpr(Token.NoToken, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable));

-

-            Expr AssumeGuard = Expr.Eq(v1, v2);

-

-            Expr EqualityCondition = ThreadsInSameGroup();

-

-            if (KernelArrayInfo.getGroupSharedArrays().Contains(v))

-            {

-                EqualityCondition = Expr.And(EqualityCondition,

-                    Expr.And(LocalFence1, LocalFence2));

-            }

-            else if (KernelArrayInfo.getGlobalArrays().Contains(v))

-            {

-                EqualityCondition = Expr.And(EqualityCondition,

-                    Expr.And(GlobalFence1, GlobalFence2));

-            }

-

-            AssumeGuard = Expr.Imp(EqualityCondition, AssumeGuard);

-

-            return new BigBlock(Token.NoToken, null, new CmdSeq(new Cmd[] { new AssumeCmd(Token.NoToken, AssumeGuard) }), null, null);

+            return new BigBlock(Token.NoToken, null, 

+              new CmdSeq(new Cmd[] { new HavocCmd(Token.NoToken, 

+                new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(Token.NoToken, v) })) }), null, null);

         }

 

-

         internal static bool ModifiesSetContains(IdentifierExprSeq Modifies, IdentifierExpr v)

         {

             foreach (IdentifierExpr ie in Modifies)

@@ -1880,16 +1857,32 @@ namespace GPUVerify
 

                 }

 

-                if (d is Variable && ((d as Variable).IsMutable || IsThreadLocalIdConstant(d as Variable)

-                    || IsGroupIdConstant(d as Variable) ))

-                {

-                    NewTopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable((Variable)d.Clone()));

-                    if (!QKeyValue.FindBoolAttribute(d.Attributes, "race_checking"))

-                    {

-                        NewTopLevelDeclarations.Add(new VariableDualiser(2, null, null).VisitVariable((Variable)d.Clone()));

-                    }

+                if (d is Variable && ((d as Variable).IsMutable || 

+                    IsThreadLocalIdConstant(d as Variable) || 

+                    IsGroupIdConstant(d as Variable))) {

+                  var v = d as Variable;

 

+                  if (KernelArrayInfo.getGlobalArrays().Contains(v)) {

+                    NewTopLevelDeclarations.Add(v);

                     continue;

+                  }

+

+                  if (KernelArrayInfo.getGroupSharedArrays().Contains(v)) {

+                    Variable newV = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken,

+                        v.Name, new MapType(Token.NoToken, new TypeVariableSeq(), 

+                        new TypeSeq(new Microsoft.Boogie.Type[] { Microsoft.Boogie.Type.Bool }),

+                        v.TypedIdent.Type)));

+                    newV.Attributes = v.Attributes;

+                    NewTopLevelDeclarations.Add(newV);

+                    continue;

+                  }

+

+                  NewTopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable((Variable)v.Clone()));

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

+                    NewTopLevelDeclarations.Add(new VariableDualiser(2, null, null).VisitVariable((Variable)v.Clone()));

+                  }

+

+                  continue;

                 }

 

                 NewTopLevelDeclarations.Add(d);

diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs
index 35e7da4b..1e462635 100644
--- a/Source/GPUVerify/RaceInstrumenter.cs
+++ b/Source/GPUVerify/RaceInstrumenter.cs
@@ -304,12 +304,6 @@ namespace GPUVerify {
       foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {

         AddRequiresNoPendingAccess(v);

         AddRequiresSourceAccessZero(v);

-

-        if (!verifier.ArrayModelledAdversarially(v)) {

-          IdentifierExpr v1 = new IdentifierExpr(Token.NoToken, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));

-          IdentifierExpr v2 = new IdentifierExpr(Token.NoToken, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable));

-          verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.Eq(v1, v2)));

-        }

       }

     }

 

@@ -491,8 +485,8 @@ namespace GPUVerify {
           new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE"))));

 

       if (verifier.KernelArrayInfo.getGlobalArrays().Contains(v)) {

-        ResetReadAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetReadAssumeGuard);

-        ResetWriteAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetWriteAssumeGuard);

+        ResetReadAssumeGuard = Expr.Imp(GPUVerifier.ThreadsInSameGroup(), ResetReadAssumeGuard);

+        ResetWriteAssumeGuard = Expr.Imp(GPUVerifier.ThreadsInSameGroup(), ResetWriteAssumeGuard);

       }

 

       result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetReadAssumeGuard));

@@ -747,13 +741,15 @@ namespace GPUVerify {
 

         if (!verifier.ArrayModelledAdversarially(v)) {

           WriteReadGuard = Expr.And(WriteReadGuard, Expr.Neq(

-              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),

-              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")

+              new VariableDualiser(1, null, null).VisitExpr(

+                MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, WriteOffsetVariable), "WRITE")),

+              new VariableDualiser(2, null, null).VisitExpr(

+                MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, OffsetParameter), "READ"))

               ));

         }

 

         if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {

-          WriteReadGuard = Expr.And(WriteReadGuard, verifier.ThreadsInSameGroup());

+          WriteReadGuard = Expr.And(WriteReadGuard, GPUVerifier.ThreadsInSameGroup());

         }

 

         WriteReadGuard = Expr.Not(WriteReadGuard);

@@ -776,13 +772,15 @@ namespace GPUVerify {
                                         new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));

         if (!verifier.ArrayModelledAdversarially(v)) {

           WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Neq(

-              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),

-              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "WRITE")

+              new VariableDualiser(1, null, null).VisitExpr(

+                MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, WriteOffsetVariable), "WRITE")),

+              new VariableDualiser(2, null, null).VisitExpr(

+                MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, OffsetParameter), "WRITE"))

               ));

         }

 

         if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {

-          WriteWriteGuard = Expr.And(WriteWriteGuard, verifier.ThreadsInSameGroup());

+          WriteWriteGuard = Expr.And(WriteWriteGuard, GPUVerifier.ThreadsInSameGroup());

         }

 

         WriteWriteGuard = Expr.Not(WriteWriteGuard);

@@ -801,13 +799,15 @@ namespace GPUVerify {
                                         new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));

         if (!verifier.ArrayModelledAdversarially(v)) {

           ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Neq(

-              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetVariable)), 1, "WRITE"),

-              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")

+              new VariableDualiser(1, null, null).VisitExpr(

+                MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, ReadOffsetVariable), "WRITE")),

+              new VariableDualiser(2, null, null).VisitExpr(

+                MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, OffsetParameter), "READ"))

               ));

         }

 

         if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {

-          ReadWriteGuard = Expr.And(ReadWriteGuard, verifier.ThreadsInSameGroup());

+          ReadWriteGuard = Expr.And(ReadWriteGuard, GPUVerifier.ThreadsInSameGroup());

         }

 

         ReadWriteGuard = Expr.Not(ReadWriteGuard);

@@ -847,8 +847,8 @@ namespace GPUVerify {
       return new AssignCmd(lhs.tok, lhss, rhss);

     }

 

-    private Expr MakeAccessedIndex(Variable v, Expr offsetExpr, int Thread, string AccessType) {

-      Expr result = new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(v.Clone() as Variable));

+    private Expr MakeAccessedIndex(Variable v, Expr offsetExpr, string AccessType) {

+      Expr result = new IdentifierExpr(v.tok, v.Clone() as Variable);

       Debug.Assert(v.TypedIdent.Type is MapType);

       MapType mt = v.TypedIdent.Type as MapType;

       Debug.Assert(mt.Arguments.Length == 1);

diff --git a/Source/GPUVerify/VariableDualiser.cs b/Source/GPUVerify/VariableDualiser.cs
index d5d9917a..ce5f78ee 100644
--- a/Source/GPUVerify/VariableDualiser.cs
+++ b/Source/GPUVerify/VariableDualiser.cs
@@ -54,13 +54,18 @@ namespace GPUVerify
 

         private TypedIdent DualiseTypedIdent(Variable v)

         {

+          if (QKeyValue.FindBoolAttribute(v.Attributes, "global") ||

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

+            return new TypedIdent(v.tok, v.Name, v.TypedIdent.Type);

+          }

 

-            if (uniformityAnalyser == null || !uniformityAnalyser.IsUniform(procName, v.Name))

-            {

-                return new TypedIdent(v.tok, v.Name + "$" + id, v.TypedIdent.Type);

-            }

-

+          if (uniformityAnalyser != null && uniformityAnalyser.IsUniform(procName, v.Name))

+          {

             return new TypedIdent(v.tok, v.Name, v.TypedIdent.Type);

+          }

+

+          return new TypedIdent(v.tok, v.Name + "$" + id, v.TypedIdent.Type);

+

         }

 

         public override Variable VisitVariable(Variable node)

@@ -79,26 +84,50 @@ namespace GPUVerify
 

         public override Expr VisitNAryExpr(NAryExpr node)

         {

-            // The point of this override is to avoid dualisation of certain special

-            // intrinsics that are cross-thread

+          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], GroupSharedIndexingExpr() })), VisitExpr(node.Args[1]) }));

+            }

+          }

 

-            if (node.Fun is FunctionCall)

+          // Avoid dualisation of certain special builtin functions that are cross-thread

+          if (node.Fun is FunctionCall)

+          {

+            FunctionCall call = node.Fun as FunctionCall;

+

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

             {

-                FunctionCall call = node.Fun as FunctionCall;

+              Debug.Assert(id == 1 || id == 2);

+              int otherId = id == 1 ? 2 : 1;

+              return new VariableDualiser(otherId, uniformityAnalyser, procName).VisitExpr(

+                  node.Args[0]);

+            }

 

-                if (otherFunctionNames.Contains(call.Func.Name))

-                {

-                    Debug.Assert(id == 1 || id == 2);

-                    int otherId = id == 1 ? 2 : 1;

-                    return new VariableDualiser(otherId, uniformityAnalyser, procName).VisitExpr(

-                        node.Args[0]);

-                }

+          }

 

-            }

+          return base.VisitNAryExpr(node);

+        }

 

-            return base.VisitNAryExpr(node);

+

+        public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) {

+

+          var v = node.DeepAssignedVariable;

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

+            return new MapAssignLhs(Token.NoToken, new MapAssignLhs(Token.NoToken, node.Map,

+              new List<Expr>(new Expr[] { GroupSharedIndexingExpr() })), node.Indexes.Select(idx => this.VisitExpr(idx)).ToList());

+

+          }

+          return base.VisitMapAssignLhs(node);

         }

 

+        private Expr GroupSharedIndexingExpr() {

+          return id == 1 ? Expr.True : GPUVerifier.ThreadsInSameGroup();

+        }

 

     }