Inter-thread race checking implementation done.

6 files changed, 22 insertions, 16 deletions

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

         }

 

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

-        {

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

-        }

-

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

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 2f8fa464..a49461c7 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -1485,7 +1485,7 @@ namespace GPUVerify
             List<BigBlock> ResetAndHavocBlocks = new List<BigBlock>();

             foreach (Variable v in NonLocalState.getAllNonLocalVariables())

             {

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

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

                 if (!ArrayModelledAdversarially(v))

                 {

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

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

         void AddRaceCheckingDeclarations();

 

-        BigBlock MakeResetReadWriteSetsStatements(Variable v, int thread);

+        BigBlock MakeResetReadWriteSetStatements(Variable v, int thread);

 

         void AddRaceCheckingCandidateRequires(Procedure Proc);

 

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

         }

 

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

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

         {

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

         }

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

 

 

-        public BigBlock MakeResetReadWriteSetsStatements(Variable v, int Thread)

+        public BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread)

         {

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

             if (Thread == 2)

             {

                 return result;

             }

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

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

+

+            Expr ResetReadAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,

+                new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ"))));

+            Expr ResetWriteAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,

+                new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE"))));

+

+            if (CommandLineOptions.InterGroupRaceChecking && verifier.NonLocalState.getGlobalVariables().Contains(v))

+            {

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

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

+            }

+

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

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

             return result;

         }

 

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

-

         protected Procedure MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite)

         {

             VariableSeq inParams = new VariableSeq();

diff --git a/Source/GPUVerify/UniformityAnalyser.cs b/Source/GPUVerify/UniformityAnalyser.cs
index bd0e3f74..35f297ed 100644
--- a/Source/GPUVerify/UniformityAnalyser.cs
+++ b/Source/GPUVerify/UniformityAnalyser.cs
@@ -63,6 +63,10 @@ namespace GPUVerify
                     SetNonUniform(Impl.Name, GPUVerifier._Y.Name);

                     SetNonUniform(Impl.Name, GPUVerifier._Z.Name);

 

+                    SetNonUniform(Impl.Name, GPUVerifier._GROUP_X.Name);

+                    SetNonUniform(Impl.Name, GPUVerifier._GROUP_Y.Name);

+                    SetNonUniform(Impl.Name, GPUVerifier._GROUP_Z.Name);

+

                     foreach (Variable v in Impl.LocVars)

                     {

                         if (CommandLineOptions.DoUniformityAnalysis)