Reinstated support for barrier flags.

3 files changed, 122 insertions, 40 deletions

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 966f98eb..018917d5 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -44,6 +44,8 @@ namespace GPUVerify
 

         public static bool InterGroupRaceChecking = false;

 

+        public static bool BarrierParameters = false;

+

         public static int Parse(string[] args)

         {

             for (int i = 0; i < args.Length; i++)

@@ -191,6 +193,11 @@ namespace GPUVerify
                     InterGroupRaceChecking = true;

                     break;

 

+                    case "-barrierParameters":

+                    case "/barrierParameters":

+                    BarrierParameters = true;

+                    break;

+

                     default:

                         inputFiles.Add(args[i]);

                         break;

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index e3d94fcc..90b4c707 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -58,6 +58,9 @@ namespace GPUVerify
         internal static Constant _NUM_GROUPS_Y = null;

         internal static Constant _NUM_GROUPS_Z = null;

 

+        internal const int CLK_LOCAL_MEM_FENCE = 1;

+        internal const int CLK_GLOBAL_MEM_FENCE = 2;

+

         public IRaceInstrumenter RaceInstrumenter;

 

         public UniformityAnalyser uniformityAnalyser;

@@ -115,7 +118,9 @@ namespace GPUVerify
             if (p == null)

             {

                 p = new Procedure(Token.NoToken, "barrier", new TypeVariableSeq(),

-                                  new VariableSeq(), new VariableSeq(),

+                                  new VariableSeq(CommandLineOptions.BarrierParameters ? 

+                                      new Variable[] { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__flags", new BvType(32)), true) } : new Variable[] { }),

+                                  new VariableSeq(),

                                   new RequiresSeq(), new IdentifierExprSeq(),

                                   new EnsuresSeq(),

                                   new QKeyValue(Token.NoToken, "barrier", new List<object>(), null));

@@ -332,8 +337,6 @@ namespace GPUVerify
 

             RemoveElseIfs();

 

-            AddStartAndEndBarriers();

-

             PullOutNonLocalAccesses();

         }

 

@@ -1050,24 +1053,6 @@ namespace GPUVerify
             return StripThreadIdentifier(p, out id);

         }

 

-        private void AddStartAndEndBarriers()

-        {

-            CallCmd FirstBarrier = new CallCmd(KernelImplementation.tok, BarrierProcedure.Name, new ExprSeq(), new IdentifierExprSeq());

-            CallCmd LastBarrier = new CallCmd(KernelImplementation.tok, BarrierProcedure.Name, new ExprSeq(), new IdentifierExprSeq());

-

-            FirstBarrier.Proc = KernelProcedure;

-            LastBarrier.Proc = KernelProcedure;

-

-            CmdSeq newCommands = new CmdSeq();

-            newCommands.Add(FirstBarrier);

-            foreach (Cmd c in KernelImplementation.StructuredStmts.BigBlocks[0].simpleCmds)

-            {

-                newCommands.Add(c);

-            }

-            KernelImplementation.StructuredStmts.BigBlocks[0].simpleCmds = newCommands;

-

-        }

-

         private void GenerateStandardKernelContract()

         {

             RaceInstrumenter.AddKernelPrecondition();

@@ -1450,8 +1435,13 @@ namespace GPUVerify
             BigBlock checkNonDivergence = new BigBlock(tok, "__BarrierImpl", new CmdSeq(), null, null);

             bigblocks.Add(checkNonDivergence);

 

+            Debug.Assert((BarrierProcedure.InParams.Length % 2) == 0);

+            int paramsPerThread = BarrierProcedure.InParams.Length / 2;

             IdentifierExpr P1 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[0].TypedIdent));

-            IdentifierExpr P2 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[1].TypedIdent));

+            IdentifierExpr P2 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[paramsPerThread].TypedIdent));

+

+            IdentifierExpr Flags1 = CommandLineOptions.BarrierParameters ? new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[1].TypedIdent)) : null;

+            IdentifierExpr Flags2 = CommandLineOptions.BarrierParameters ? new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[paramsPerThread + 1].TypedIdent)) : null;

 

             Expr DivergenceCondition = Expr.Eq(P1, P2);

             if (CommandLineOptions.InterGroupRaceChecking)

@@ -1466,43 +1456,72 @@ namespace GPUVerify
                 List<BigBlock> returnbigblocks = new List<BigBlock>();

                 returnbigblocks.Add(new BigBlock(tok, "__Disabled", new CmdSeq(), null, new ReturnCmd(tok)));

                 StmtList returnstatement = new StmtList(returnbigblocks, BarrierProcedure.tok);

+

+                Expr IfGuard;

+

+                if (CommandLineOptions.InterGroupRaceChecking)

+                {

+                    IfGuard = Expr.Or(Expr.And(Expr.Not(P1), Expr.Not(P2)), Expr.And(ThreadsInSameGroup(), Expr.Or(Expr.Not(P1), Expr.Not(P2))));

+                }

+                else

+                {

                 // We make this an "Or", not an "And", because "And" is implied by the assertion that the variables

                 // are equal, together with the "Or".  The weaker "Or" ensures that many auxiliary assertions will not

                 // fail if divergence has not been proved.

-                checkNonDivergence.ec = new IfCmd(tok, Expr.Or(Expr.Not(P1), Expr.Not(P2)), returnstatement, null, null);

+                    IfGuard = Expr.Or(Expr.Not(P1), Expr.Not(P2));

+            }

+                checkNonDivergence.ec = new IfCmd(tok, IfGuard, returnstatement, null, null);

             }

 

-            if (CommandLineOptions.InterGroupRaceChecking)

+            if(NonLocalState.getGroupSharedVariables().Count > 0) {

+                Expr IfGuard1 = CommandLineOptions.InterGroupRaceChecking ? (Expr)P1 : (Expr)Expr.True;

+                Expr IfGuard2 = CommandLineOptions.InterGroupRaceChecking ? (Expr)P2 : (Expr)Expr.True;

+

+                if (CommandLineOptions.BarrierParameters)

             {

+                    IfGuard1 = Expr.And(IfGuard1, CLK_LOCAL_MEM_FENCE_isSet(Flags1));

+                    IfGuard2 = Expr.And(IfGuard2, CLK_LOCAL_MEM_FENCE_isSet(Flags2));

+                }

+

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

-                    new IfCmd(Token.NoToken, P1, new StmtList(MakeResetAndHavocBlocks(1), Token.NoToken), null, null),

+                    new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, NonLocalState.getGroupSharedVariables()), Token.NoToken), null, null),

                     null));

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

-                    new IfCmd(Token.NoToken, P2, new StmtList(MakeResetAndHavocBlocks(2), Token.NoToken), null, null),

+                    new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetAndHavocBlocks(2, NonLocalState.getGroupSharedVariables()), Token.NoToken), null, null),

                     null));

             }

-            else

+

+            if (NonLocalState.getGlobalVariables().Count > 0)

             {

-                foreach (BigBlock bb in MakeResetAndHavocBlocks(1))

-                {

-                    bigblocks.Add(bb);

-                }

-                foreach (BigBlock bb in MakeResetAndHavocBlocks(2))

+                Expr IfGuard1 = CommandLineOptions.InterGroupRaceChecking ? (Expr)P1 : (Expr)Expr.True;

+                Expr IfGuard2 = CommandLineOptions.InterGroupRaceChecking ? (Expr)P2 : (Expr)Expr.True;

+

+                if (CommandLineOptions.BarrierParameters)

                 {

-                    bigblocks.Add(bb);

+                    IfGuard1 = Expr.And(IfGuard1, CLK_GLOBAL_MEM_FENCE_isSet(Flags1));

+                    IfGuard2 = Expr.And(IfGuard2, CLK_GLOBAL_MEM_FENCE_isSet(Flags2));

                 }

+

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

+                    new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, NonLocalState.getGlobalVariables()), Token.NoToken), null, null),

+                    null));

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

+                    new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetAndHavocBlocks(2, NonLocalState.getGlobalVariables()), Token.NoToken), null, null),

+                    null));

             }

 

             foreach (Variable v in NonLocalState.getAllNonLocalVariables())

             {

                 if (!ArrayModelledAdversarially(v))

                 {

-                    bigblocks.Add(AssumeEqualityBetweenSharedArrays(v, P1, P2));

+                    bigblocks.Add(AssumeEqualityBetweenSharedArrays(v, P1, P2, Flags1, Flags2));

                 }

             }

 

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

-            Implementation BarrierImplementation = new Implementation(BarrierProcedure.tok, BarrierProcedure.Name, new TypeVariableSeq(), BarrierProcedure.InParams, BarrierProcedure.OutParams, new VariableSeq(), statements);

+            Implementation BarrierImplementation = 

+                new Implementation(BarrierProcedure.tok, BarrierProcedure.Name, new TypeVariableSeq(), 

+                    BarrierProcedure.InParams, BarrierProcedure.OutParams, new VariableSeq(), statements);

 

             if (CommandLineOptions.Unstructured)

                 BarrierImplementation.Resolve(ResContext);

@@ -1515,10 +1534,28 @@ namespace GPUVerify
             Program.TopLevelDeclarations.Add(BarrierImplementation);

         }

 

-        private List<BigBlock> MakeResetAndHavocBlocks(int Thread)

+        private static Expr flagIsSet(Expr Flags, int flag)

         {

+            return Expr.Eq(new BvExtractExpr(

+                                    Token.NoToken, Flags, flag, flag - 1),

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

+        }

+

+        private static Expr CLK_GLOBAL_MEM_FENCE_isSet(Expr Flags)

+        {

+            return flagIsSet(Flags, CLK_GLOBAL_MEM_FENCE);

+        }

+

+        private static Expr CLK_LOCAL_MEM_FENCE_isSet(Expr Flags)

+        {

+            return flagIsSet(Flags, CLK_LOCAL_MEM_FENCE);

+        }

+

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

+        {

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

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

-            foreach (Variable v in NonLocalState.getAllNonLocalVariables())

+            foreach (Variable v in variables)

             {

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

                 if (!ArrayModelledAdversarially(v))

@@ -1526,6 +1563,7 @@ namespace GPUVerify
                     ResetAndHavocBlocks.Add(HavocSharedArray(v, Thread));

                 }

             }

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

             return ResetAndHavocBlocks;

         }

 

@@ -1565,18 +1603,36 @@ namespace GPUVerify
             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)

+        private BigBlock AssumeEqualityBetweenSharedArrays(Variable v, Expr P1, Expr P2, Expr Flags1, Expr Flags2)

         {

             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 = Expr.True;

+

             if (CommandLineOptions.InterGroupRaceChecking)

             {

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

+                EqualityCondition = ThreadsInSameGroup();

             }

 

+            if (CommandLineOptions.BarrierParameters)

+            {

+                if (NonLocalState.getGroupSharedVariables().Contains(v))

+                {

+                    EqualityCondition = Expr.And(EqualityCondition,

+                        Expr.And(CLK_LOCAL_MEM_FENCE_isSet(Flags1), CLK_LOCAL_MEM_FENCE_isSet(Flags2)));

+                }

+                else if (NonLocalState.getGlobalVariables().Contains(v))

+                {

+                    EqualityCondition = Expr.And(EqualityCondition,

+                        Expr.And(CLK_GLOBAL_MEM_FENCE_isSet(Flags1), CLK_GLOBAL_MEM_FENCE_isSet(Flags2)));

+                }

+            }

+

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

+

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

         }

 

@@ -2260,11 +2316,23 @@ namespace GPUVerify
                 return ErrorCount;

             }

 

-            if (BarrierProcedure.InParams.Length != 0)

+            if(!CommandLineOptions.BarrierParameters && BarrierProcedure.InParams.Length != 0)

             {

                 Error(BarrierProcedure, "Barrier procedure must not take any arguments");

             }

 

+            if (CommandLineOptions.BarrierParameters)

+            {

+                if (BarrierProcedure.InParams.Length != 1)

+                {

+                    Error(BarrierProcedure, "Barrier procedure must take exactly one argument");

+                }

+                else if (!BarrierProcedure.InParams[0].TypedIdent.Type.Equals(new BvType(32)))

+                {

+                    Error(BarrierProcedure, "Argument to barrier procedure must have type bv32");

+                }

+            }

+

             if (BarrierProcedure.OutParams.Length != 0)

             {

                 Error(BarrierProcedure, "Barrier procedure must not return any results");

diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs
index 2c95216f..6a2f3392 100644
--- a/Source/GPUVerify/RaceInstrumenter.cs
+++ b/Source/GPUVerify/RaceInstrumenter.cs
@@ -675,6 +675,13 @@ namespace GPUVerify
             foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

             {

                 AddRequiresNoPendingAccess(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)));

+                }

             }

         }