Progress on inter-group race checking

5 files changed, 71 insertions, 28 deletions

diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
index 5fd780f7..643317ca 100644
--- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
@@ -174,9 +174,9 @@ namespace GPUVerify
             return new AssignCmd(lhs.tok, lhss, rhss);

         }

 

-        protected override void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v, string AccessType)

+        protected override void SetNoAccessOccurred(BigBlock bb, Variable v, string AccessType)

         {

-            IdentifierExpr AccessOccurred1 = new IdentifierExpr(tok,

+            IdentifierExpr AccessOccurred1 = new IdentifierExpr(Token.NoToken,

                 new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, AccessType)));

 

             bb.simpleCmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(AccessOccurred1)));

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 83cfabf9..2f8fa464 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -1418,7 +1418,13 @@ namespace GPUVerify
             IdentifierExpr P1 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[0].TypedIdent));

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

 

-            checkNonDivergence.simpleCmds.Add(new AssertCmd(tok, Expr.Eq(P1, P2)));

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

+            if (CommandLineOptions.InterGroupRaceChecking)

+            {

+                DivergenceCondition = Expr.Imp(ThreadsInSameGroup(), DivergenceCondition);

+            }

+

+            checkNonDivergence.simpleCmds.Add(new AssertCmd(tok, DivergenceCondition));

 

             if (!CommandLineOptions.OnlyDivergence)

             {

@@ -1431,15 +1437,32 @@ namespace GPUVerify
                 checkNonDivergence.ec = new IfCmd(tok, Expr.Or(Expr.Not(P1), Expr.Not(P2)), returnstatement, null, null);

             }

 

-            bigblocks.Add(RaceInstrumenter.MakeResetReadWriteSetsStatements(tok));

+            if (CommandLineOptions.InterGroupRaceChecking)

+            {

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

+                    new IfCmd(Token.NoToken, P1, new StmtList(MakeResetAndHavocBlocks(1), 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),

+                    null));

+            }

+            else

+            {

+                foreach (BigBlock bb in MakeResetAndHavocBlocks(1))

+                {

+                    bigblocks.Add(bb);

+                }

+                foreach (BigBlock bb in MakeResetAndHavocBlocks(2))

+                {

+                    bigblocks.Add(bb);

+                }

+            }

 

-            BigBlock havocSharedState = new BigBlock(tok, "__HavocSharedState", new CmdSeq(), null, null);

-            bigblocks.Add(havocSharedState);

             foreach (Variable v in NonLocalState.getAllNonLocalVariables())

             {

                 if (!ArrayModelledAdversarially(v))

                 {

-                    HavocAndAssumeEquality(tok, havocSharedState, v);

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

                 }

             }

 

@@ -1457,6 +1480,20 @@ namespace GPUVerify
             Program.TopLevelDeclarations.Add(BarrierImplementation);

         }

 

+        private List<BigBlock> MakeResetAndHavocBlocks(int Thread)

+        {

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

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

+            {

+                ResetAndHavocBlocks.Add(RaceInstrumenter.MakeResetReadWriteSetsStatements(v, Thread));

+                if (!ArrayModelledAdversarially(v))

+                {

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

+                }

+            }

+            return ResetAndHavocBlocks;

+        }

+

 

         public static bool HasZDimension(Variable v)

         {

@@ -1487,17 +1524,28 @@ namespace GPUVerify
             return v.TypedIdent.Type is MapType;

         }

 

-        private void HavocAndAssumeEquality(IToken tok, BigBlock bb, Variable v)

+        private BigBlock HavocSharedArray(Variable v, int thread)

         {

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

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

+            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)

+        {

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

 

-            IdentifierExprSeq ModifiedVars = new IdentifierExprSeq(new IdentifierExpr[] { v1, v2 });

-            bb.simpleCmds.Add(new HavocCmd(tok, ModifiedVars));

-            bb.simpleCmds.Add(new AssumeCmd(tok, Expr.Eq(v1, v2)));

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

 

+            if (CommandLineOptions.InterGroupRaceChecking)

+            {

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

+            }

+

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

         }

 

+

         internal static bool ModifiesSetContains(IdentifierExprSeq Modifies, IdentifierExpr v)

         {

             foreach (IdentifierExpr ie in Modifies)

diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs
index 4845a0c3..2182eb6a 100644
--- a/Source/GPUVerify/IRaceInstrumenter.cs
+++ b/Source/GPUVerify/IRaceInstrumenter.cs
@@ -20,7 +20,7 @@ namespace GPUVerify
 

         void AddRaceCheckingDeclarations();

 

-        BigBlock MakeResetReadWriteSetsStatements(IToken tok);

+        BigBlock MakeResetReadWriteSetsStatements(Variable v, int thread);

 

         void AddRaceCheckingCandidateRequires(Procedure Proc);

 

diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs
index d38c57af..84d21106 100644
--- a/Source/GPUVerify/NullRaceInstrumenter.cs
+++ b/Source/GPUVerify/NullRaceInstrumenter.cs
@@ -24,9 +24,9 @@ namespace GPUVerify
             return true;

         }

 

-        public Microsoft.Boogie.BigBlock MakeResetReadWriteSetsStatements(Microsoft.Boogie.IToken tok)

+        public Microsoft.Boogie.BigBlock MakeResetReadWriteSetsStatements(Variable v, int Thread)

         {

-            return new BigBlock(tok, "__ResetReadWriteSets", new CmdSeq(), null, null);

+            return new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);

         }

 

         public void AddRaceCheckingCandidateRequires(Procedure Proc)

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index ad0fd9f6..20dbf87a 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -930,24 +930,19 @@ namespace GPUVerify
         protected abstract void AddLogAccessProcedure(Variable v, string ReadOrWrite);

 

 

-        public BigBlock MakeResetReadWriteSetsStatements(IToken tok)

+        public BigBlock MakeResetReadWriteSetsStatements(Variable v, int Thread)

         {

-            BigBlock result = new BigBlock(tok, "__ResetReadWriteSets", new CmdSeq(), null, null);

-

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

+            BigBlock result = new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);

+            if (Thread == 2)

             {

-                SetNoAccessOccurred(tok, result, v);

+                return result;

             }

+            SetNoAccessOccurred(result, v, "READ");

+            SetNoAccessOccurred(result, v, "WRITE");

             return result;

         }

 

-        private void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v)

-        {

-            SetNoAccessOccurred(tok, bb, v, "READ");

-            SetNoAccessOccurred(tok, bb, v, "WRITE");

-        }

-

-        protected abstract void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v, string AccessType);

+        protected abstract void SetNoAccessOccurred(BigBlock bb, Variable v, string AccessType);

 

         protected Procedure MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite)

         {