Progress on GPUVerify

9 files changed, 186 insertions, 1316 deletions

diff --git a/Source/GPUVerify/AccessCollector.cs b/Source/GPUVerify/AccessCollector.cs
index a3821952..c0e1e217 100644
--- a/Source/GPUVerify/AccessCollector.cs
+++ b/Source/GPUVerify/AccessCollector.cs
@@ -8,11 +8,13 @@ namespace GPUVerify
 {

     abstract class AccessCollector : StandardVisitor

     {

-        protected GPUVerifier verifier;

+        protected List<Variable> GlobalVariables;

+        protected List<Variable> TileStaticVariables;

 

-        public AccessCollector(GPUVerifier verifier)

+        public AccessCollector(List<Variable> GlobalVariables, List<Variable> TileStaticVariables)

         {

-            this.verifier = verifier;

+            this.GlobalVariables = GlobalVariables;

+            this.TileStaticVariables = TileStaticVariables;

         }

 

         protected void MultiDimensionalMapError()

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index ecbee795..7c667c63 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -15,6 +15,11 @@ namespace GPUVerify
 

         public static string outputFile = null;

         public static string formulaSkeletonsFile = null;

+        public static string formulasFile = null;

+

+        public static bool NewRaceDetectionMethod = false;

+        public static bool OnlyDivergence = false;

+        public static bool FullAbstraction;

 

         public static int Parse(string[] args)

         {

@@ -56,6 +61,35 @@ namespace GPUVerify
                     formulaSkeletonsFile = afterColon;

                     break;

 

+                    case "-formulas":

+                    case "/formulas":

+                    if (!hasColonArgument)

+                    {

+                        Console.WriteLine("Error: filename expected after " + beforeColon + " argument");

+                        Environment.Exit(1);

+                    }

+                    Debug.Assert(afterColon != null);

+                    formulasFile = afterColon;

+                    break;

+

+                    case "-newRaceDetectionMethod":

+                    case "/newRaceDetectionMethod":

+                    NewRaceDetectionMethod = true;

+

+                    break;

+

+                    case "-onlyDivergence":

+                    case "/onlyDivergence":

+                    OnlyDivergence = true;

+

+                    break;

+

+                    case "-fullAbstraction":

+                    case "/fullAbstraction":

+                    FullAbstraction = true;

+

+                    break;

+

                     default:

                         inputFiles.Add(args[i]);

                         break;

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index fb91c284..b643efdd 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -3,63 +3,38 @@ using System.Collections.Generic;
 using System.Linq;

 using System.Text;

 using System.Diagnostics;

+using System.Diagnostics.Contracts;

 using Microsoft.Boogie;

 using Microsoft.Basetypes;

 

 namespace GPUVerify

 {

-    class GPUVerifier : CheckingContext

+    abstract class GPUVerifier : CheckingContext

     {

+        protected Program Program;

 

-        HashSet<string> ReservedNames;

+        protected Procedure KernelProcedure;

+        protected Implementation KernelImplementation;

+        protected Procedure BarrierProcedure;

 

-        private Program Program;

-        private Procedure KernelProcedure;

-        private Implementation KernelImplementation;

-        private Procedure BarrierProcedure;

-        private Microsoft.Boogie.Type ThreadIdType;

-        private String ThreadIdParameterName;

-

-        private HashSet<int> BarrierIds = new HashSet<int>();

-

-        private List<Variable> ThreadLocalVariables = new List<Variable>();

-        private List<Variable> TileStaticVariables = new List<Variable>();

-        private List<Variable> GlobalVariables = new List<Variable>();

+        protected List<Variable> ThreadLocalVariables = new List<Variable>();

+        protected List<Variable> TileStaticVariables = new List<Variable>();

+        protected List<Variable> GlobalVariables = new List<Variable>();

 

+        protected HashSet<string> ReservedNames = new HashSet<string>();

 

         public GPUVerifier(Program program)

             : base((IErrorSink)null)

         {

             this.Program = program;

-

-            ReservedNames = new HashSet<string>();

-            ReservedNames.Add("base");

-            ReservedNames.Add("offset_x");

-            ReservedNames.Add("offset_y");

-            ReservedNames.Add("offset_z");

-            ReservedNames.Add("is_write");

-            ReservedNames.Add("AT_BARRIER");

-            ReservedNames.Add("REACHED_NEXT_BARRIER");

-

-            CheckWellFormedness();

         }

 

-        private void CheckWellFormedness()

-        {

-            int errorCount = check(Program);

-            if (errorCount != 0)

-            {

-                Console.WriteLine("{0} GPUVerify format errors detected in {1}", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);

-                Environment.Exit(1);

-            }

-        }

+        abstract internal void doit();

 

-        internal int check(Program program)

+        virtual internal int Check()

         {

-            BarrierProcedure = CheckExactlyOneBarrierProcedure(program);

-            KernelProcedure = CheckExactlyOneKernelProcedure(program);

-            TypeSynonymDecl ThreadIdDecl = CheckExactlyOneThreadIdType(program);

-            ThreadIdType = new TypeSynonymAnnotation(ThreadIdDecl.tok, ThreadIdDecl, new TypeSeq());

+            BarrierProcedure = CheckExactlyOneBarrierProcedure();

+            KernelProcedure = CheckExactlyOneKernelProcedure();

 

             if (ErrorCount > 0)

             {

@@ -76,13 +51,15 @@ namespace GPUVerify
                 Error(BarrierProcedure, "Barrier procedure must not return any results");

             }

 

-            FindGlobalVariables(program);

+            FindGlobalVariables(Program);

 

-            CheckKernelImplementation(program);

+            CheckKernelImplementation();

 

             return ErrorCount;

         }

 

+

+

         private void FindGlobalVariables(Program program)

         {

             foreach (Declaration D in program.TopLevelDeclarations)

@@ -97,211 +74,26 @@ namespace GPUVerify
             }

         }

 

-

-        private void CheckKernelImplementation(Program Program)

-        {

-            if (KernelProcedure.InParams.Length != 1)

-            {

-                Error(KernelProcedure, "Kernel procedure must take exactly one argument, of type {0}", ThreadIdType.ToString());

-            }

-            else

-            {

-                if (!KernelProcedure.InParams[0].TypedIdent.Type.Equals(ThreadIdType))

-                {

-                    Error(KernelProcedure, "Argument to kernel procedure has wrong type - {0} instead of {1}", KernelProcedure.InParams[0].TypedIdent.Type.ToString(), ThreadIdType.ToString());

-                }

-

-                ThreadIdParameterName = KernelProcedure.InParams[0].TypedIdent.Name;

-

-            }

-

-            if (KernelProcedure.OutParams.Length != 0)

-            {

-                Error(KernelProcedure, "Kernel procedure must not return any results");

-            }

-

-

-            foreach (Declaration decl in Program.TopLevelDeclarations)

-            {

-                if (!(decl is Implementation))

-                {

-                    continue;

-                }

-

-                Implementation Impl = decl as Implementation;

-

-                if (Impl.Proc == KernelProcedure)

-                {

-                    KernelImplementation = Impl;

-                    break;

-                }

-

-            }

-

-            if (KernelImplementation == null)

-            {

-                Error(Token.NoToken, "*** Error: no implementation of kernel procedure");

-                return;

-            }

-

-            // Collect up the local and tile_static variables

-            foreach (LocalVariable LV in KernelImplementation.LocVars)

-            {

-                if (QKeyValue.FindBoolAttribute(LV.Attributes, "tile_static"))

-                {

-                    TileStaticVariables.Add(LV);

-                }

-                else

-                {

-                    ThreadLocalVariables.Add(LV);

-                }

-            }

-

-            // Clear the local variables

-            KernelImplementation.LocVars = new VariableSeq();

-

-            foreach (LocalVariable LV in ThreadLocalVariables)

-            {

-                // Make each local variable a global map from threadid to the usual type

-                GlobalVariable GV = new GlobalVariable(LV.tok, LV.TypedIdent);

-                TypeSeq IndexType = new TypeSeq();

-                IndexType.Add(ThreadIdType);

-                GV.TypedIdent.Type = new MapType(GV.TypedIdent.Type.tok, new TypeVariableSeq(), IndexType, LV.TypedIdent.Type);

-                Program.TopLevelDeclarations.Add(GV);

-                KernelProcedure.Modifies.Add(new IdentifierExpr(GV.tok, GV));

-            }

-

-            foreach (LocalVariable LV in TileStaticVariables)

-            {

-                // Promote each tile-static variable to global

-                GlobalVariable GV = new GlobalVariable(LV.tok, LV.TypedIdent);

-                GV.TypedIdent.Type = LV.TypedIdent.Type;

-                Program.TopLevelDeclarations.Add(GV);

-                KernelProcedure.Modifies.Add(new IdentifierExpr(GV.tok, GV));

-            }

-

-            LocalVariableAccessReplacer replacer = new LocalVariableAccessReplacer(this);

-

-            replacer.VisitImplementation(KernelImplementation);

-

-            // Check that each barrier has a positive integer id

-            // Check that these ids are all distinct

-            foreach (Block B in KernelImplementation.Blocks)

-            {

-                foreach (Cmd C in B.Cmds)

-                {

-                    if (IsBarrier(C))

-                    {

-                        CallCmd Barrier = C as CallCmd;

-

-                        int BarrierId = QKeyValue.FindIntAttribute(Barrier.Attributes, "barrier_id", -1);

-                        if (BarrierId < 1)

-                        {

-                            Error(Barrier, "Barrier must have positive integer attribute \"barrier_id\"");

-                        }

-                        else if (BarrierIds.Contains(BarrierId))

-                        {

-                            Error(Barrier, "Each barrier call must have a unique integer attribute \"barrier_id\" - duplicate id {0} detected", BarrierId);

-                        }

-                        else

-                        {

-                            BarrierIds.Add(BarrierId);

-                        }

-                    }

-                }

-

-            }

-

-

-        }

-

-

-

-        private Procedure CheckExactlyOneKernelProcedure(Program program)

-        {

-            return CheckSingleInstanceOfAttributedProcedure(program, "kernel");

-        }

-

-        private Procedure CheckExactlyOneBarrierProcedure(Program program)

-        {

-            return CheckSingleInstanceOfAttributedProcedure(program, "barrier");

-        }

-

-        private TypeSynonymDecl CheckExactlyOneThreadIdType(Program program)

-        {

-            return CheckSingleInstanceOfAttributedEntity<TypeSynonymDecl>(program, "thread_id");

-        }

-

-        private T CheckSingleInstanceOfAttributedEntity<T>(Program program, string attribute) where T : Declaration

-        {

-            T attributedEntity = null;

-            foreach (Declaration decl in program.TopLevelDeclarations)

-            {

-                if (!QKeyValue.FindBoolAttribute(decl.Attributes, attribute))

-                {

-                    continue;

-                }

-

-                if (decl is T)

-                {

-                    if (attributedEntity == null)

-                    {

-                        attributedEntity = decl as T;

-                    }

-                    else

-                    {

-                        Error(decl, "\"{0}\" attribute specified for {1}, but it has already been specified for procedure {2}", attribute, decl.ToString(), attributedEntity.ToString());

-                    }

-                }

-                else

-                {

-                    Error(decl, "\"{0}\" attribute applied to wrong sort of declaration {1}", attribute, decl.ToString());

-                }

-            }

-

-            if (attributedEntity == null)

-            {

-                Error(program, "\"{0}\" attribute has not been specified for any procedure.  You must mark exactly one procedure with this attribute", attribute);

-            }

-

-            return attributedEntity;

-        }

-

-

-        internal void AddBarrierId(int BarrierId)

-        {

-            BarrierIds.Add(BarrierId);

-        }

-

-        internal int MaxBarrierId()

+        protected void CheckWellFormedness()

         {

-            int result = -1;

-            foreach (int i in BarrierIds)

+            int errorCount = Check();

+            if (errorCount != 0)

             {

-                if (i > result)

-                {

-                    result = i;

-                }

+                Console.WriteLine("{0} GPUVerify format errors detected in {1}", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);

+                Environment.Exit(1);

             }

-            return result;

         }

 

-        internal List<Variable> GetGlobalVariables()

-        {

-            return GlobalVariables;

-        }

-

-        internal List<Variable> GetTileStaticVariables()

+        protected Procedure CheckExactlyOneKernelProcedure()

         {

-            return TileStaticVariables;

+            return CheckSingleInstanceOfAttributedProcedure(Program, "kernel");

         }

 

-        internal List<Variable> GetThreadLocalVariables()

+        protected Procedure CheckExactlyOneBarrierProcedure()

         {

-            return ThreadLocalVariables;

+            return CheckSingleInstanceOfAttributedProcedure(Program, "barrier");

         }

 

-

         private Procedure CheckSingleInstanceOfAttributedProcedure(Program program, string attribute)

         {

             Procedure attributedProcedure = null;

@@ -339,1074 +131,93 @@ namespace GPUVerify
             return attributedProcedure;

         }

 

-        public void AddInitialAndFinalBarriers()

+        private void FindLocalVariables()

         {

-            // Add barrier to start of first block, if it doesn't already start with a barrier

-            if (!IsBarrier(KernelImplementation.Blocks[0].Cmds[0]))

-            {

-                CmdSeq NewCmds = new CmdSeq();

-                NewCmds.Add(MakeBarrierCmd(0));

-                foreach (Cmd C in KernelImplementation.Blocks[0].Cmds)

-                {

-                    NewCmds.Add(C);

-                }

-                KernelImplementation.Blocks[0].Cmds = NewCmds;

-            }

-

-            CmdSeq FinalBarrierCmdSeq = new CmdSeq();

-

-            int FinalBarrierId = MaxBarrierId() + 1;

-

-            FinalBarrierCmdSeq.Add(MakeBarrierCmd(FinalBarrierId));

-

-            string FinalBarrierLabel = "barrier_label" + FinalBarrierId;

-

-            Block FinalBarrierBlock = new Block(Token.NoToken, FinalBarrierLabel, FinalBarrierCmdSeq, new ReturnCmd(Token.NoToken));

-

-            foreach (Block B in KernelImplementation.Blocks)

-            {

-                if (B.TransferCmd is ReturnCmd)

-                {

-                    BlockSeq BlockSeq = new BlockSeq();

-                    BlockSeq.Add(FinalBarrierBlock);

-                    StringSeq StringSeq = new StringSeq();

-                    StringSeq.Add(FinalBarrierLabel);

-                    B.TransferCmd = new GotoCmd(Token.NoToken, StringSeq, BlockSeq);

-                }

-            }

-

-            KernelImplementation.Blocks.Add(FinalBarrierBlock);

-

-        }

-

-        private Cmd MakeBarrierCmd(int BarrierId)

-        {

-            Debug.Assert(!BarrierIds.Contains(BarrierId));

-            AddBarrierId(BarrierId);

-            CallCmd Result = new CallCmd(Token.NoToken, BarrierProcedure.Name, new ExprSeq(), new IdentifierExprSeq());

-            Result.Attributes = new QKeyValue(Token.NoToken, "barrier_id", new List<object>(new object[] { Expr.Literal(BarrierId) }), null);

-            return Result;

-        }

-

-

-        private static Implementation CloneImplementation(Implementation Impl, string NewName)

-        {

-            Implementation Result = new Implementation(Impl.tok, NewName, Impl.TypeParameters, Impl.InParams, Impl.OutParams, Impl.LocVars, new List<Block>());

-

-            Dictionary<Block, Block> OldToNew = new Dictionary<Block, Block>();

-

-            foreach (Block B in Impl.Blocks)

-            {

-                Block NewB = CloneBlock(B);

-

-                OldToNew.Add(B, NewB);

-

-                Result.Blocks.Add(NewB);

-

-            }

-

-            foreach (Block NewB in Result.Blocks)

-            {

-                if (NewB.TransferCmd is GotoCmd)

-                {

-                    GotoCmd NewGotoCmd = NewB.TransferCmd as GotoCmd;

-

-                    for (int i = 0; i < NewGotoCmd.labelTargets.Length; i++)

-                    {

-                        Block NewSuccessor;

-                        bool found = OldToNew.TryGetValue(NewGotoCmd.labelTargets[i], out NewSuccessor);

-                        Debug.Assert(found);

-

-                        NewGotoCmd.labelTargets[i] = NewSuccessor;

-                    }

-

-                }

-            }

-

-            return Result;

-        }

-

-

-        private static Block CloneBlock(Block B)

-        {

-            Block NewB = new Block(B.tok, B.Label, new CmdSeq(), null);

-

-            foreach (Cmd C in B.Cmds)

-            {

-                NewB.Cmds.Add(C); // The contents of each command is *not* cloned

-            }

-

-            if (B.TransferCmd is ReturnCmd)

-            {

-                NewB.TransferCmd = new ReturnCmd((B.TransferCmd as ReturnCmd).tok);

-            }

-            else

-            {

-                GotoCmd GotoCmd = B.TransferCmd as GotoCmd;

-                NewB.TransferCmd = new GotoCmd(GotoCmd.tok, new StringSeq(), new BlockSeq());

-                GotoCmd NewGotoCmd = NewB.TransferCmd as GotoCmd;

-                for (int i = 0; i < GotoCmd.labelNames.Length; i++)

-                {

-                    NewGotoCmd.labelNames.Add(GotoCmd.labelNames[i]);

-                    NewGotoCmd.labelTargets.Add(GotoCmd.labelTargets[i]);

-                }

-            }

-            return NewB;

-        }

-

-

-        private static void AppendDuplicateBlockToStartOfImplementation(Implementation Impl, int i)

-        {

-            Block NewBlock = CloneBlock(Impl.Blocks[i]);

-            NewBlock.Label = "entry_barrier";

-

-            List<Block> NewBlocks = new List<Block>();

-

-            NewBlocks.Add(NewBlock);

-

-            foreach (Block B in Impl.Blocks)

-            {

-                NewBlocks.Add(B);

-            }

-

-            Impl.Blocks = NewBlocks;

-

-        }

-

-        private Implementation ConstructBarrierToNextBarriersImplementation(Block B, String NewProcedureName)

-        {

-            Implementation NewImplementation = CloneImplementation(KernelImplementation, NewProcedureName);

-

-            AppendDuplicateBlockToStartOfImplementation(NewImplementation, KernelImplementation.Blocks.IndexOf(B));

-

-            // Iterate through all blocks except first, immediately following barrier calls with "return"

-

-            for (int i = 1; i < NewImplementation.Blocks.Count; i++)

+            foreach (LocalVariable LV in KernelImplementation.LocVars)

             {

-                if (IsBarrier(NewImplementation.Blocks[i]))

+                if (!QKeyValue.FindBoolAttribute(LV.Attributes, "tile_static"))

                 {

-                    // This is a barrier so we don't want control to get any further.

-                    // To ensure this, we simply remove any commands following the barrier,

-                    // and make the transfer command into a "return".

-                    CmdSeq NewCmdSeq = new CmdSeq();

-                    NewCmdSeq.Add(NewImplementation.Blocks[i].Cmds[0]);

-                    NewImplementation.Blocks[i].Cmds = NewCmdSeq;

-                    NewImplementation.Blocks[i].TransferCmd = new ReturnCmd(Token.NoToken);

+                    ThreadLocalVariables.Add(LV);

                 }

             }

-

-            NewImplementation.PruneUnreachableBlocks();

-            return NewImplementation;

         }

 

-        private void SanityCheckKernel()

+        private void FindTileStaticVariables()

         {

-            foreach (Block C in KernelImplementation.Blocks)

+            foreach (LocalVariable LV in KernelImplementation.LocVars)

             {

-                if (C.TransferCmd is GotoCmd)

+                if (QKeyValue.FindBoolAttribute(LV.Attributes, "tile_static"))

                 {

-                    foreach (Block D in (C.TransferCmd as GotoCmd).labelTargets)

-                    {

-                        Debug.Assert(KernelImplementation.Blocks.Contains(D));

-                    }

+                    TileStaticVariables.Add(LV);

                 }

             }

         }

 

-

-        private void GenerateBarrierToNextBarriersProcedure(Block B)

-        {

-            SanityCheckKernel();

-            Debug.Assert(IsBarrier(B));

-

-            String NewProcedureName = MakeBarrierToNextBarriersProcedureName(B);

-            Procedure NewProcedure = CloneKernelProcedure(NewProcedureName);

-

-            AddTrackingVariablesToModifiesSet(B.tok, NewProcedure.Modifies);

-

-            AddInlineAttribute(NewProcedure);

-

-            Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(B, NewProcedureName);

-

-            InstrumentWithRaceDetection(NewImplementation);

-

-            AddBarrierTracking(NewImplementation);

-

-            Program.TopLevelDeclarations.Add(NewProcedure);

-            Program.TopLevelDeclarations.Add(NewImplementation);

-

-        }

-

-        private string MakeBarrierToNextBarriersProcedureName(Block B)

-        {

-            return "Barrier_" + GetBarrierId(B) + "_to_next_barriers";

-        }

-

-        private string MakeBarrierAToBProcedureName(Block A, Block B)

+        private void GetKernelImplementation()

         {

-            return "Barrier_" + GetBarrierId(A) + "_to_" + GetBarrierId(B);

-        }

-

-        private static CtorType MakeArrayBaseType(IToken tok)

-        {

-            return new CtorType(tok, new TypeCtorDecl(tok, "ArrayBase", 0), new TypeSeq());

-        }

-

-        private IdentifierExpr MakeBaseVariable(IToken tok)

-        {

-            TypeSeq typeSeq = new TypeSeq();

-            typeSeq.Add(ThreadIdType);

-            return new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "base", new MapType(tok, new TypeVariableSeq(), typeSeq, MakeArrayBaseType(tok)))));

-        }

-

-        private IdentifierExpr MakeOffsetVariable(IToken tok, string Dimension)

-        {

-            TypeSeq typeSeq = new TypeSeq();

-            typeSeq.Add(ThreadIdType);

-            return new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "offset_" + Dimension, new MapType(tok, new TypeVariableSeq(), typeSeq, Microsoft.Boogie.Type.Int))));

-        }

-

-        private IdentifierExpr MakeOffsetXVariable(IToken tok)

-        {

-            return MakeOffsetVariable(tok, "x");

-        }

-

-        private IdentifierExpr MakeOffsetYVariable(IToken tok)

-        {

-            return MakeOffsetVariable(tok, "y");

-        }

-

-        private IdentifierExpr MakeOffsetZVariable(IToken tok)

-        {

-            return MakeOffsetVariable(tok, "z");

-        }

-

-        private IdentifierExpr MakeIsWriteVariable(IToken tok)

-        {

-            TypeSeq typeSeq = new TypeSeq();

-            typeSeq.Add(ThreadIdType);

-            return new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "is_write", new MapType(tok, new TypeVariableSeq(), typeSeq, Microsoft.Boogie.Type.Bool))));

-        }

-

-        private void InstrumentWithRaceDetection(Implementation Impl)

-        {

-            foreach (Block B in Impl.Blocks)

+            foreach (Declaration decl in Program.TopLevelDeclarations)

             {

-                CmdSeq NewCmds = new CmdSeq();

-

-                foreach (Cmd C in B.Cmds)

+                if (!(decl is Implementation))

                 {

-                    ReadCollector rc = new ReadCollector(this);

-                    rc.Visit(C);

-                    WriteCollector wc = new WriteCollector(this);

-                    wc.Visit(C);

-

-                    if (wc.FoundWrite())

-                    {

-                        AccessRecord write = wc.GetAccess();

-                        ExprSeq InParams = ConstructLogAccessParameters(C, write);

-                        NewCmds.Add(new CallCmd(C.tok, "LOG_WRITE", InParams, new IdentifierExprSeq()));

-                    }

-

-                    foreach (AccessRecord read in rc.accesses)

-                    {

-                        ExprSeq InParams = ConstructLogAccessParameters(C, read);

-                        NewCmds.Add(new CallCmd(C.tok, "LOG_READ", InParams, new IdentifierExprSeq()));

-                    }

-

-                    NewCmds.Add(C);

+                    continue;

                 }

-                B.Cmds = NewCmds;

-            }

-        }

-

-        private ExprSeq ConstructLogAccessParameters(Cmd C, AccessRecord access)

-        {

-            ExprSeq InParams = new ExprSeq();

-            InParams.Add(new IdentifierExpr(C.tok, new GlobalVariable(C.tok, new TypedIdent(C.tok, access.v.Name + "_base", Microsoft.Boogie.Type.Int))));

-            InParams.Add(access.IndexZ);

-            InParams.Add(access.IndexY);

-            InParams.Add(access.IndexX);

-            InParams.Add(MakeThreadIdExpr(C.tok));

-            return InParams;

-        }

 

-        private void GenerateBarrierAToBarrierBProcedure(Block A, Block B)

-        {

-            Debug.Assert(IsBarrier(A));

-            Debug.Assert(IsBarrier(B));

-

-            if (!BarrierReachesBarrier(A, B))

-            {

-                return;

-            }

-

-            String NewProcedureName = MakeBarrierAToBProcedureName(A, B);

-            Procedure NewProcedure = CloneKernelProcedure(NewProcedureName);

-            Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(A, NewProcedureName);

-

-            AddInlineAttribute(NewProcedure);

-

-            NewProcedure.Modifies.Add(MakeReachedNextBarrierVariable(B.tok));

+                Implementation Impl = decl as Implementation;

 

-            Block NewA = NewImplementation.Blocks[0];

-            Block NewB = null;

-            for (int i = 1; i < NewImplementation.Blocks.Count; i++)

-            {

-                if (IsBarrier(NewImplementation.Blocks[i]) && GetBarrierId(B) == GetBarrierId(NewImplementation.Blocks[i]))

+                if (Impl.Proc == KernelProcedure)

                 {

-                    NewB = NewImplementation.Blocks[i];

+                    KernelImplementation = Impl;

                     break;

                 }

-            }

-            Debug.Assert(NewB != null);

-

-            NewImplementation.ComputePredecessorsForBlocks();

-

-            HashSet<Block> NodesToKeep = BlocksReaching(NewB);

-

-            Debug.Assert(NodesToKeep.Count > 1);

-

-            foreach (Block D in NewImplementation.Blocks)

-            {

-                if (D.TransferCmd is GotoCmd)

-                {

-                    GotoCmd GotoCmd = D.TransferCmd as GotoCmd;

-                    GotoCmd NewGotoCmd = new GotoCmd(GotoCmd.tok, new StringSeq(), new BlockSeq());

-                    for (int i = 0; i < GotoCmd.labelNames.Length; i++)

-                    {

-                        if (NodesToKeep.Contains(GotoCmd.labelTargets[i]))

-                        {

-                            NewGotoCmd.labelNames.Add(GotoCmd.labelNames[i]);

-                            NewGotoCmd.labelTargets.Add(GotoCmd.labelTargets[i]);

-                        }

-                    }

-                    D.TransferCmd = NewGotoCmd;

-                }

-            }

-

-            NewImplementation.PruneUnreachableBlocks();

-

-            AddReachedNextBarrierTracking(NewImplementation, A, B);

-

-            Program.TopLevelDeclarations.Add(NewProcedure);

-            Program.TopLevelDeclarations.Add(NewImplementation);

-

-        }

-

-        private bool BarrierReachesBarrier(Block A, Block B)

-        {

-            Debug.Assert(IsBarrier(A));

-            Debug.Assert(IsBarrier(B));

-

-            Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(A, "noname");

-

-            for (int i = 1; i < NewImplementation.Blocks.Count; i++)

-            {

-                if (IsBarrier(NewImplementation.Blocks[i]) && GetBarrierId(B) == GetBarrierId(NewImplementation.Blocks[i]))

-                {

-                    return true;

-                }

-            }

-

-            return false;

-        }

-

-        private static void AddInlineAttribute(Procedure NewProcedure)

-        {

-            NewProcedure.AddAttribute("inline", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(1)) });

-        }

-

-        private Procedure CloneKernelProcedure(string NewProcedureName)

-        {

-            RequiresSeq NewRequiresSeq = new RequiresSeq();

-            foreach(Requires r in KernelProcedure.Requires)

-            {

-                NewRequiresSeq.Add(r);

-            }

-            EnsuresSeq NewEnsuresSeq = new EnsuresSeq();

-            foreach (Ensures e in KernelProcedure.Ensures)

-            {

-                NewEnsuresSeq.Add(e);

-            }

-            IdentifierExprSeq NewModifiesSeq = new IdentifierExprSeq();

-            foreach (IdentifierExpr ies in KernelProcedure.Modifies)

-            {

-                NewModifiesSeq.Add(ies);

-            }

-            return new Procedure(KernelProcedure.tok, NewProcedureName, KernelProcedure.TypeParameters, KernelProcedure.InParams, KernelProcedure.OutParams, NewRequiresSeq, NewModifiesSeq, NewEnsuresSeq);

-        }

-

-        private void AddBarrierTracking(Implementation Impl)

-        {

-            Debug.Assert(IsBarrier(Impl.Blocks[0]));

-            CmdSeq NewBlock0Commands = new CmdSeq();

-

-            NewBlock0Commands.Add(Impl.Blocks[0].Cmds[0]);

-

-            NewBlock0Commands.Add(MakeAssignToAtBarrier(Impl.Blocks[0].Cmds[0].tok, -1));

 

-            for (int i = 1; i < Impl.Blocks[0].Cmds.Length; i++)

-            {

-                NewBlock0Commands.Add(Impl.Blocks[0].Cmds[i]);

-            }

-

-            Impl.Blocks[0].Cmds = NewBlock0Commands;

-

-            for (int i = 1; i < Impl.Blocks.Count; i++)

-            {

-                if (IsBarrier(Impl.Blocks[i]))

-                {

-                    // At this stage, the barrier should be followed immediately by a return

-                    Debug.Assert(Impl.Blocks[i].Cmds.Length == 1);

-

-                    Impl.Blocks[i].Cmds.Add(MakeAssignToAtBarrier(Impl.Blocks[i].Cmds[0].tok, GetBarrierId(Impl.Blocks[i])));

-

-                }

             }

 

-        }

-

-

-        private void AddReachedNextBarrierTracking(Implementation Impl, Block A, Block B)

-        {

-            Debug.Assert(IsBarrier(Impl.Blocks[0]) && GetBarrierId(Impl.Blocks[0]) == GetBarrierId(A));

-

-            for (int i = 1; i < Impl.Blocks.Count; i++)

+            if (KernelImplementation == null)

             {

-                if (IsBarrier(Impl.Blocks[i]))

-                {

-                    // At this stage, the barrier should be followed immediately by a return

-                    Debug.Assert(Impl.Blocks[i].Cmds.Length == 1 && GetBarrierId(Impl.Blocks[i]) == GetBarrierId(B));

-

-                    Impl.Blocks[i].Cmds.Add(MakeSetReachedNextBarrier(Impl.Blocks[i].Cmds[0].tok));

-

-                }

+                Error(Token.NoToken, "*** Error: no implementation of kernel procedure");

             }

         }

 

 

-        private AssignCmd MakeAssignToAtBarrier(IToken tok, int p)

-        {

-            List<AssignLhs> lhss = new List<AssignLhs>();

-            List<Expr> rhss = new List<Expr>();

-

-            List<Expr> indexes = new List<Expr>();

-            indexes.Add(MakeThreadIdExpr(tok));

-            lhss.Add(new MapAssignLhs(tok, new SimpleAssignLhs(tok, MakeAtBarrierVariable(tok)), indexes));

-            rhss.Add(new LiteralExpr(tok, BigNum.FromInt(p)));

-            return new AssignCmd(tok, lhss, rhss);

-        }

-

-        private AssignCmd MakeSetReachedNextBarrier(IToken tok)

-        {

-            List<AssignLhs> lhss = new List<AssignLhs>();

-            List<Expr> rhss = new List<Expr>();

-

-            List<Expr> indexes = new List<Expr>();

-            indexes.Add(MakeThreadIdExpr(tok));

-            lhss.Add(new MapAssignLhs(tok, new SimpleAssignLhs(tok, MakeReachedNextBarrierVariable(tok)), indexes));

-            rhss.Add(new LiteralExpr(tok, true));

-            return new AssignCmd(tok, lhss, rhss);

-        }

-

-        private NAryExpr MakeAtBarrierAccess(IToken tok, string ThreadIdName)

-        {

-            ExprSeq args = new ExprSeq();

-            args.Add(MakeAtBarrierVariable(tok));

-            args.Add(MakeThreadIdExpr(tok, ThreadIdName));

-            return new NAryExpr(tok, new MapSelect(tok, 1), args);

-        }

-

-        private NAryExpr MakeReachedNextBarrierAccess(IToken tok, string ThreadIdName)

-        {

-            ExprSeq args = new ExprSeq();

-            args.Add(MakeReachedNextBarrierVariable(tok));

-            args.Add(MakeThreadIdExpr(tok, ThreadIdName));

-            return new NAryExpr(tok, new MapSelect(tok, 1), args);

-        }

-

-        private IdentifierExpr MakeAtBarrierVariable(IToken tok)

-        {

-            TypeSeq IndexType = new TypeSeq();

-            IndexType.Add(ThreadIdType);

-            return new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "AT_BARRIER", new MapType(tok, new TypeVariableSeq(), IndexType, Microsoft.Boogie.Type.Int))));

-        }

-

-        private IdentifierExpr MakeReachedNextBarrierVariable(IToken tok)

-        {

-            TypeSeq IndexType = new TypeSeq();

-            IndexType.Add(ThreadIdType);

-            return new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "REACHED_NEXT_BARRIER", new MapType(tok, new TypeVariableSeq(), IndexType, Microsoft.Boogie.Type.Bool))));

-        }

-

-        private static HashSet<Block> BlocksReaching(Block B)

-        {

-            HashSet<Block> Result = new HashSet<Block>();

-            ComputeReachingBlocksRecursive(B, Result);

-            return Result;

-        }

-

-        private static void ComputeReachingBlocksRecursive(Block B, HashSet<Block> Result)

-        {

-            if (Result.Contains(B))

-            {

-                return;

-            }

 

-            Result.Add(B);

-            foreach (Block C in B.Predecessors)

-            {

-                ComputeReachingBlocksRecursive(C, Result);

-            }

-        }

 

-        private static HashSet<Block> BlocksReachableFrom(Block B)

+        protected virtual void CheckKernelImplementation()

         {

-            HashSet<Block> Result = new HashSet<Block>();

-            ComputeReachableBlocksRecursive(B, Result);

-            return Result;

-        }

+            CheckKernelParameters();

+            GetKernelImplementation();

 

-        private static void ComputeReachableBlocksRecursive(Block B, HashSet<Block> Result)

-        {

-            if (Result.Contains(B))

+            if (KernelImplementation == null)

             {

                 return;

             }

-            Result.Add(B);

-            if (B.TransferCmd is GotoCmd)

-            {

-                foreach (Block C in (B.TransferCmd as GotoCmd).labelTargets)

-                {

-                    ComputeReachableBlocksRecursive(C, Result);

-                }

-            }

-        }

-

-

-

-

-        private Block FindBarrierBlock(Implementation Impl, int BarrierId)

-        {

-            foreach (Block B in Impl.Blocks)

-            {

-                if (B.Cmds.Length > 0 && IsBarrier(B.Cmds[0]) && GetBarrierId(B) == BarrierId)

-                {

-                    return B;

-                }

-            }

-

-            Debug.Assert(false);

-

-            return null;

-        }

-

-        private int GetBarrierId(Cmd C)

-        {

-            Debug.Assert(IsBarrier(C));

-            return QKeyValue.FindIntAttribute((C as CallCmd).Attributes, "barrier_id", -1);

-        }

-

-        public int GetBarrierId(Block A)

-        {

-            Debug.Assert(A.Cmds.Length > 0);

-            return GetBarrierId(A.Cmds[0]);

-        }

-

-        public bool IsBarrier(Cmd C)

-        {

-            return C is CallCmd && (C as CallCmd).callee == BarrierProcedure.Name;

-        }

-

-        public bool IsBarrier(Block B)

-        {

-            return B.Cmds.Length > 0 && IsBarrier(B.Cmds[0]);

-        }

-

-

-

-

-        public void SplitBlocksAtBarriers()

-        {

-

-            int NumBlocksBeforeSplitting = KernelImplementation.Blocks.Count;

-

-            for (int i = 0; i < NumBlocksBeforeSplitting; i++)

-            {

-                Block B = KernelImplementation.Blocks[i];

-

-                List<CmdSeq> Segments = new List<CmdSeq>();

-                CmdSeq CurrentSequence = new CmdSeq();

-                foreach (Cmd C in B.Cmds)

-                {

-                    if (IsBarrier(C))

-                    {

-                        if (CurrentSequence.Length > 0)

-                        {

-                            Segments.Add(CurrentSequence);

-                            CurrentSequence = new CmdSeq();

-                        }

-                    }

-

-                    CurrentSequence.Add(C);

-                }

-                if (CurrentSequence.Length > 0)

-                {

-                    Segments.Add(CurrentSequence);

-                }

-

-                if (Segments.Count > 1)

-                {

-                    TransferCmd OriginalTransferCmd = B.TransferCmd;

-

-                    // Set the block's commands to be the first command sequence

-                    B.Cmds = Segments[0];

-                    B.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq());

-                    Block LastBlock = B;

-                    for (int j = 1; j < Segments.Count; j++)

-                    {

-                        Block NewBlock = new Block(Token.NoToken, "barrier_label_" + GetBarrierId(Segments[j][0]), Segments[j], new GotoCmd(Token.NoToken, new BlockSeq()));

-                        KernelImplementation.Blocks.Add(NewBlock);

-                        (LastBlock.TransferCmd as GotoCmd).AddTarget(NewBlock);

-                        LastBlock = NewBlock;

-                    }

-                    LastBlock.TransferCmd = OriginalTransferCmd;

-

-                }

-

-            }

-        }

-

-        private bool ContainsInternalBarrier(Block B)

-        {

-            bool first = true;

-            foreach (Cmd C in B.Cmds)

-            {

-                if (first)

-                {

-                    first = false;

-                    continue;

-                }

-

-                if (C is CallCmd)

-                {

-                    CallCmd Call = C as CallCmd;

-                    if (QKeyValue.FindBoolAttribute(Call.Proc.Attributes, "barrier"))

-                    {

-                        return true;

-                    }

-                }

-

-            }

-

-            return false;

-        }

-

-

-

-        internal Implementation GetKernel()

-        {

-            return KernelImplementation;

-        }

-

-        internal void GenerateBarrierToNextBarriersProcedures()

-        {

-            foreach (Block B in KernelImplementation.Blocks)

-            {

-                if (IsBarrier(B) && (GetBarrierId(B) < MaxBarrierId()))

-                {

-                    GenerateBarrierToNextBarriersProcedure(B);

-                }

-            }

-        }

-

-        internal void GenerateBarrierToBarrierPairProcedures()

-        {

-            foreach (Block A in KernelImplementation.Blocks)

-            {

-                if (IsBarrier(A))

-                {

-                    foreach (Block B in KernelImplementation.Blocks)

-                    {

-                        if (IsBarrier(B))

-                        {

-                            GenerateBarrierAToBarrierBProcedure(A, B);

-                        }

-                    }

-                }

-            }

-        }

 

-        internal IdentifierExpr MakeThreadIdExpr(IToken tok, string name)

-        {

-            return new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, name, ThreadIdType)));

+            FindLocalVariables();

+            FindTileStaticVariables();

+            CheckNoReturns();

         }

 

-        internal IdentifierExpr MakeThreadIdExpr(IToken tok)

+        private void CheckNoReturns()

         {

-            return MakeThreadIdExpr(tok, ThreadIdParameterName);

+            // TODO!

         }

 

+        protected abstract void CheckKernelParameters();

 

-        internal void AddArrayBaseDeclarations()

-        {

-            foreach (Variable V in GetGlobalVariables())

-            {

-                Program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V.tok)), true));

-            }

 

-            foreach (Variable V in GetTileStaticVariables())

-            {

-                Program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V.tok)), true));

-            }

-        }

-

-        internal void GenerateBarrierToNextBarriersVCs()

-        {

-            foreach (Block B in KernelImplementation.Blocks)

-            {

-                if (IsBarrier(B) && (GetBarrierId(B) < MaxBarrierId()))

-                {

-                    GenerateBarrierToNextBarriersVC(B);

-                }

-            }

-        }

-

-        private void GenerateBarrierToNextBarriersVC(Block B)

-        {

-            VariableSeq InParams = new VariableSeq();

-            InParams.Add(new LocalVariable(B.tok, new TypedIdent(B.tok, "__i", ThreadIdType)));

-            InParams.Add(new LocalVariable(B.tok, new TypedIdent(B.tok, "__j", ThreadIdType)));

-

-            VariableSeq OutParams = new VariableSeq();

-

-            IdentifierExprSeq Modifies = new IdentifierExprSeq();

-            foreach (IdentifierExpr ie in KernelProcedure.Modifies)

-            {

-                Modifies.Add(ie);

-            }

-

-            AddTrackingVariablesToModifiesSet(B.tok, Modifies);

-

-            RequiresSeq Requires = new RequiresSeq();

-            Requires.Add(new Requires(false, MakePreconditionExpr(B)));

-            AddDistinctSameTile(B.tok, Requires, "__i", "__j");

-            AddNothingInitiallyTracked(B.tok, Requires, "__i", "__j");

-

-

-            EnsuresSeq Ensures = new EnsuresSeq();

-            AddNoRace(B.tok, Ensures, "__i", "__j");

-            AddSameBarrier(B.tok, Ensures, "__i", "__j");

-

-            string BarrierIsRaceAndDivergenceFree = "Check_Barrier_" + GetBarrierId(B) + "_Race_And_Divergence_Free";

-

-            Procedure NewProcedure = new Procedure(B.tok, BarrierIsRaceAndDivergenceFree, new TypeVariableSeq(), InParams, OutParams, Requires, Modifies, Ensures);

-

-            List<Block> Blocks = new List<Block>();

-

-            Blocks.Add(new Block());

-

-            Blocks[0].TransferCmd = new ReturnCmd(B.tok);

-

-            Blocks[0].Label = "entry";

-

-            Blocks[0].Cmds = new CmdSeq();

-

-            ExprSeq i = new ExprSeq();

-            i.Add(new IdentifierExpr(B.tok, new LocalVariable(B.tok, new TypedIdent(B.tok, "__i", ThreadIdType))));

-            Blocks[0].Cmds.Add(new CallCmd(B.tok, MakeBarrierToNextBarriersProcedureName(B), i, new IdentifierExprSeq()));

-

-            ExprSeq j = new ExprSeq();

-            j.Add(new IdentifierExpr(B.tok, new LocalVariable(B.tok, new TypedIdent(B.tok, "__j", ThreadIdType))));

-            Blocks[0].Cmds.Add(new CallCmd(B.tok, MakeBarrierToNextBarriersProcedureName(B), j, new IdentifierExprSeq()));

-

-            Implementation NewImplementation = new Implementation(B.tok, BarrierIsRaceAndDivergenceFree, new TypeVariableSeq(), InParams, OutParams, new VariableSeq(), Blocks);

-

-            Program.TopLevelDeclarations.Add(NewProcedure);

-            Program.TopLevelDeclarations.Add(NewImplementation);

-

-        }

-

-        private void AddNothingInitiallyTracked(IToken tok, RequiresSeq Requires, string i, string j)

-        {

-            Requires.Add(new Requires(false, Expr.And(BaseEqualsNothing(tok, i), BaseEqualsNothing(tok, j))));

-        }

-

-        private Expr BaseEqualsNothing(IToken tok, string i)

-        {

-            ExprSeq MapSelectArgs = new ExprSeq();

-            MapSelectArgs.Add(MakeBaseVariable(tok));

-            MapSelectArgs.Add(MakeThreadIdExpr(tok, i));

-            return Expr.Eq(new NAryExpr(tok, new MapSelect(tok, 1), MapSelectArgs), new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "nothing", MakeArrayBaseType(tok)))));

-        }

-

-        private void AddSameBarrier(IToken tok, EnsuresSeq Ensures, string i, string j)

-        {

-            ExprSeq args1 = new ExprSeq();

-            args1.Add(MakeAtBarrierVariable(tok));

-            args1.Add(MakeThreadIdExpr(tok, i));

-

-            ExprSeq args2 = new ExprSeq();

-            args2.Add(MakeAtBarrierVariable(tok));

-            args2.Add(MakeThreadIdExpr(tok, j));

-

-            Ensures.Add(new Ensures(false, Expr.Eq( new NAryExpr(tok, new MapSelect(tok, 1), args1), new NAryExpr(tok, new MapSelect(tok, 1), args2) ) ) );

-

-        }

-

-        private void AddNoRace(IToken tok, EnsuresSeq Ensures, string i, string j)

-        {

-            ExprSeq RaceArgs = new ExprSeq();

-            RaceArgs.Add(MakeBaseVariable(tok));

-            RaceArgs.Add(MakeOffsetZVariable(tok));

-            RaceArgs.Add(MakeOffsetYVariable(tok));

-            RaceArgs.Add(MakeOffsetXVariable(tok));

-            RaceArgs.Add(MakeIsWriteVariable(tok));

-            RaceArgs.Add(MakeThreadIdExpr(tok, i));

-            RaceArgs.Add(MakeThreadIdExpr(tok, j));

-

-            NAryExpr RaceExpr = new NAryExpr(tok, new FunctionCall(new IdentifierExpr(tok, "race", Microsoft.Boogie.Type.Bool)), RaceArgs);

-            Ensures.Add(new Ensures(false, Expr.Not(RaceExpr)));

-        }

-

-        private void AddDistinctSameTile(IToken tok, RequiresSeq Requires, string i, string j)

-        {

-            ExprSeq args = new ExprSeq();

-            args.Add(new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, i, ThreadIdType))));

-            args.Add(new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, j, ThreadIdType))));

-            Requires.Add(new Requires(false, new NAryExpr(tok, new FunctionCall(new IdentifierExpr(tok, "distinct_same_tile", Microsoft.Boogie.Type.Bool)), args)));

-        }

-

-        private NAryExpr MakePreconditionExpr(Block B)

-        {

-            ExprSeq PreconditionArgs = new ExprSeq();

-            foreach (Variable v in MakeFormulaFunctionArguments(B.tok, false))

-            {

-                PreconditionArgs.Add(new IdentifierExpr(B.tok, v));

-            }

-

-            NAryExpr nary = new NAryExpr(B.tok, new FunctionCall(new IdentifierExpr(B.tok, MakePreconditionName(B), Microsoft.Boogie.Type.Bool)), PreconditionArgs);

-            return nary;

-        }

-

-        private void AddTrackingVariablesToModifiesSet(IToken tok, IdentifierExprSeq Modifies)

-        {

-            Modifies.Add(MakeBaseVariable(tok));

-            Modifies.Add(MakeOffsetXVariable(tok));

-            Modifies.Add(MakeOffsetYVariable(tok));

-            Modifies.Add(MakeOffsetZVariable(tok));

-            Modifies.Add(MakeIsWriteVariable(tok));

-            Modifies.Add(MakeAtBarrierVariable(tok));

-        }

-

-        internal void GenerateBarrierToBarrierPairVCs()

-        {

-            foreach (Block A in KernelImplementation.Blocks)

-            {

-                if (IsBarrier(A))

-                {

-                    foreach (Block B in KernelImplementation.Blocks)

-                    {

-                        if (IsBarrier(B) && BarrierReachesBarrier(A, B))

-                        {

-                            GenerateBarrierAToBarrierBVCs(A, B);

-                        }

-                    }

-                }

-            }

-        }

-

-        private void GenerateBarrierAToBarrierBVCs(Block A, Block B)

-        {

-            GenerateVC_AToB_Pre(A, B);

-            GenerateVC_AToB_Induction(A, B);

-            GenerateVC_AToB_Post(A, B);

-        }

-

-        private ForallExpr MakeAllReachedNextBarrierExpr(IToken tok)

-        {

-            VariableSeq i = new VariableSeq();

-            i.Add(MakeThreadIdExpr(tok, "__i").Decl);

-            ForallExpr forallexpr = new ForallExpr(tok, i, MakeReachedNextBarrierAccess(tok, "__i"));

-            return forallexpr;

-        }

-

-        private ForallExpr MakeNoneReachedNextBarrierExpr(IToken tok)

-        {

-            VariableSeq i = new VariableSeq();

-            i.Add(MakeThreadIdExpr(tok, "__i").Decl);

-            ForallExpr forallexpr = new ForallExpr(tok, i, Expr.Not(MakeReachedNextBarrierAccess(tok, "__i")));

-            return forallexpr;

-        }

-

-        private string MakeIHName(Block A, Block B)

-        {

-            return "IH_" + GetBarrierId(A) + "_" + GetBarrierId(B);

-        }

-

-

-        private NAryExpr MakeIHExpr(Block A, Block B)

-        {

-            ExprSeq IHArgs = new ExprSeq();

-            foreach (Variable v in MakeFormulaFunctionArguments(B.tok, true))

-            {

-                IHArgs.Add(new IdentifierExpr(B.tok, v));

-            }

-

-            NAryExpr nary = new NAryExpr(B.tok, new FunctionCall(new IdentifierExpr(A.tok, MakeIHName(A, B), Microsoft.Boogie.Type.Bool)), IHArgs);

-            return nary;

-        }

-

-        private Expr MakeThreadNotReachedNextBarrierExpr(IToken tok, string ThreadIdName)

-        {

-            return Expr.Not(MakeReachedNextBarrierAccess(tok, ThreadIdName));

-        }

-

-        private void GenerateVC_AToB_Pre(Block A, Block B)

-        {

-            string ProcedureName = "Check_" + GetBarrierId(A) + "_to_" + GetBarrierId(B) + "_Pre";

-

-            Procedure NewProcedure = new Procedure(A.tok, ProcedureName, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

-            NewProcedure.Requires.Add(new Requires(false, MakePreconditionExpr(A)));

-            NewProcedure.Requires.Add(new Requires(false, MakeNoneReachedNextBarrierExpr(A.tok)));

-            NewProcedure.Ensures.Add(new Ensures(false, MakeIHExpr(A, B)));

-

-            Implementation NewImplementation = new Implementation(A.tok, ProcedureName, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new VariableSeq(), new List<Block>());

-

-            Program.TopLevelDeclarations.Add(NewProcedure);

-            Program.TopLevelDeclarations.Add(NewImplementation);

-        }

-

-        private void GenerateVC_AToB_Induction(Block A, Block B)

-        {

-            string ProcedureName = "Check_" + GetBarrierId(A) + "_to_" + GetBarrierId(B) + "_Induction";

-

-            VariableSeq InParams = new VariableSeq();

-            InParams.Add(MakeThreadIdExpr(A.tok).Decl);

-

-            IdentifierExprSeq Modifies = new IdentifierExprSeq();

-            foreach (IdentifierExpr ie in KernelProcedure.Modifies)

-            {

-                Modifies.Add(ie);

-            }

-

-            Modifies.Add(MakeReachedNextBarrierVariable(B.tok));

-

-            Procedure NewProcedure = new Procedure(A.tok, ProcedureName, new TypeVariableSeq(), InParams, new VariableSeq(), new RequiresSeq(), Modifies, new EnsuresSeq());

-            NewProcedure.Requires.Add(new Requires(false, MakeIHExpr(A, B)));

-            NewProcedure.Requires.Add(new Requires(false, MakeThreadNotReachedNextBarrierExpr(A.tok, ThreadIdParameterName)));

-            NewProcedure.Ensures.Add(new Ensures(false, MakeIHExpr(A, B)));

-

-            Implementation NewImplementation = new Implementation(A.tok, ProcedureName, new TypeVariableSeq(), InParams, new VariableSeq(), new VariableSeq(), new List<Block>());

-            NewImplementation.Blocks.Add(new Block());

-            NewImplementation.Blocks[0].Label = "entry";

-            NewImplementation.Blocks[0].TransferCmd = new ReturnCmd(A.tok);

-            NewImplementation.Blocks[0].Cmds = new CmdSeq();

-            ExprSeq i = new ExprSeq();

-            i.Add(MakeThreadIdExpr(A.tok));

-            NewImplementation.Blocks[0].Cmds.Add(new CallCmd(A.tok, MakeBarrierAToBProcedureName(A, B), i, new IdentifierExprSeq()));

-

-            Program.TopLevelDeclarations.Add(NewProcedure);

-            Program.TopLevelDeclarations.Add(NewImplementation);

-        }

-

-        private void GenerateVC_AToB_Post(Block A, Block B)

-        {

-            string ProcedureName = "Check_" + GetBarrierId(A) + "_to_" + GetBarrierId(B) + "_Post";

-

-            Procedure NewProcedure = new Procedure(A.tok, ProcedureName, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

-            NewProcedure.Requires.Add(new Requires(false, MakeIHExpr(A, B)));

-            NewProcedure.Requires.Add(new Requires(false, MakeAllReachedNextBarrierExpr(B.tok)));

-            NewProcedure.Ensures.Add(new Ensures(false, MakePreconditionExpr(B)));

-

-            Implementation NewImplementation = new Implementation(A.tok, ProcedureName, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new VariableSeq(), new List<Block>());

-

-            Program.TopLevelDeclarations.Add(NewProcedure);

-            Program.TopLevelDeclarations.Add(NewImplementation);

-

-        }

-

-        internal void GenerateFormulaSkeletons(string filename)

-        {

-            Program FormulaSkeletons = new Program();

-

-            foreach (Block B in KernelImplementation.Blocks)

-            {

-                if (IsBarrier(B))

-                {

-                    FormulaSkeletons.TopLevelDeclarations.Add(MakeSkeletonFormula(B, MakePreconditionName(B), false));

-                }

-            }

-

-            foreach (Block A in KernelImplementation.Blocks)

-            {

-                if (IsBarrier(A))

-                {

-                    foreach (Block B in KernelImplementation.Blocks)

-                    {

-                        if (IsBarrier(B) && BarrierReachesBarrier(A, B))

-                        {

-                            FormulaSkeletons.TopLevelDeclarations.Add(MakeSkeletonFormula(B, MakeIHName(A, B), true));

-                        }

-                    }

-                }

-            }

-

-            using (TokenTextWriter writer = new TokenTextWriter(filename))

-            {

-                FormulaSkeletons.Emit(writer);

-            }

-

-

-        }

-

-        private string MakePreconditionName(Block B)

+        internal List<Variable> GetThreadLocalVariables()

         {

-            return "Pre_" + GetBarrierId(B);

+            return ThreadLocalVariables;

         }

 

-        private Function MakeSkeletonFormula(Block B, string FunctionName, bool isIH)

+        internal List<Variable> GetTileStaticVariables()

         {

-

-            Function precondition = new Function(B.tok, FunctionName, MakeFormulaFunctionArguments(B.tok, isIH), MakeFunctionReturnTemp(B.tok));

-

-            precondition.AddAttribute("inline", new object[] { });

-

-            precondition.Body = new LiteralExpr(B.tok, true);

-            return precondition;

+            return TileStaticVariables;

         }

 

-        private Variable MakeFunctionReturnTemp(IToken tok)

+        internal List<Variable> GetGlobalVariables()

         {

-            return new LocalVariable(tok, new TypedIdent(tok, "result", Microsoft.Boogie.Type.Bool));

+            return GlobalVariables;

         }

 

-        private VariableSeq MakeFormulaFunctionArguments(IToken tok, bool isIH)

-        {

-            VariableSeq arguments = new VariableSeq();

-

-            foreach (Variable v in ThreadLocalVariables)

-            {

-                arguments.Add(v);

-            }

-

-            foreach (Variable v in TileStaticVariables)

-            {

-                arguments.Add(v);

-            }

-

-            foreach (Variable v in GlobalVariables)

-            {

-                arguments.Add(v);

-            }

-

-            if (isIH)

-            {

-                arguments.Add(MakeReachedNextBarrierVariable(tok).Decl);

-            }

-            return arguments;

-        }

     }

-

 }

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 407ebe5f..dd2f9c27 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -13,6 +13,7 @@
     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <TargetFrameworkProfile>Client</TargetFrameworkProfile>

     <FileAlignment>512</FileAlignment>

+    <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">

     <PlatformTarget>x86</PlatformTarget>

@@ -23,6 +24,33 @@
     <DefineConstants>DEBUG;TRACE</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>

+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly />

+    <CodeContractsCustomRewriterClass />

+    <CodeContractsLibPaths />

+    <CodeContractsExtraRewriteOptions />

+    <CodeContractsExtraAnalysisOptions />

+    <CodeContractsBaseLineFile />

+    <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+    <CodeContractsAnalysisPrecisionLevel>0</CodeContractsAnalysisPrecisionLevel>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">

     <PlatformTarget>x86</PlatformTarget>

@@ -36,6 +64,7 @@
   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Core" />

+    <Reference Include="System.Windows.Forms" />

     <Reference Include="System.Xml.Linq" />

     <Reference Include="System.Data.DataSetExtensions" />

     <Reference Include="Microsoft.CSharp" />

@@ -47,10 +76,15 @@
     <Compile Include="AccessRecord.cs" />

     <Compile Include="CommandLineOptions.cs" />

     <Compile Include="GPUVerifier.cs" />

+    <Compile Include="GPUVerifierAsynchronous.cs" />

+    <Compile Include="GPUVerifierLockStep.cs" />

     <Compile Include="LocalVariableAccessReplacer.cs" />

     <Compile Include="Main.cs" />

+    <Compile Include="NonLocalAccessCollector.cs" />

+    <Compile Include="NonLocalAccessExtractor.cs" />

     <Compile Include="Properties\AssemblyInfo.cs" />

     <Compile Include="ReadCollector.cs" />

+    <Compile Include="VariableDualiser.cs" />

     <Compile Include="WriteCollector.cs" />

   </ItemGroup>

   <ItemGroup>

diff --git a/Source/GPUVerify/LocalVariableAccessReplacer.cs b/Source/GPUVerify/LocalVariableAccessReplacer.cs
index 64dde7dc..0da4ee71 100644
--- a/Source/GPUVerify/LocalVariableAccessReplacer.cs
+++ b/Source/GPUVerify/LocalVariableAccessReplacer.cs
@@ -10,9 +10,9 @@ namespace GPUVerify
     class LocalVariableAccessReplacer : StandardVisitor

     {

 

-        GPUVerifier verifier;

+        GPUVerifierAsynchronous verifier;

 

-        public LocalVariableAccessReplacer(GPUVerifier verifier)

+        public LocalVariableAccessReplacer(GPUVerifierAsynchronous verifier)

         {

             this.verifier = verifier;

         }

diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
index 90524bb1..1e4136b9 100644
--- a/Source/GPUVerify/Main.cs
+++ b/Source/GPUVerify/Main.cs
@@ -4,6 +4,9 @@ using System.Linq;
 using System.Text;

 using System.IO;

 using System.Diagnostics;

+using System.Windows.Forms;

+

+

 

 using Microsoft.Boogie;

 

@@ -11,7 +14,7 @@ namespace GPUVerify
 {

     class GPUVerify

     {

-

+        static bool ASYNCHRONOUS_METHOD = false;

 

         public static void Main(string[] args)

         {

@@ -38,6 +41,36 @@ namespace GPUVerify
                 }

             }

 

+            if (ASYNCHRONOUS_METHOD)

+            {

+

+                string[] preprocessArguments = new string[CommandLineOptions.inputFiles.Count + 4];

+                preprocessArguments[0] = "/noVerify";

+                preprocessArguments[1] = "/printUnstructured";

+                preprocessArguments[2] = "/print:temp_unstructured.bpl";

+                preprocessArguments[3] = Path.GetDirectoryName(Application.ExecutablePath) + "\\..\\..\\BoogieLibrary\\GPUVerifyLibrary.bpl";

+                for (int i = 0; i < CommandLineOptions.inputFiles.Count; i++)

+                {

+                    preprocessArguments[i + 4] = CommandLineOptions.inputFiles[i];

+                }

+

+                OnlyBoogie.Main(preprocessArguments);

+

+                if ((CommandLineOptions.formulasFile == null && CommandLineOptions.formulaSkeletonsFile == null) || (CommandLineOptions.formulasFile != null && CommandLineOptions.formulaSkeletonsFile != null))

+                {

+                    Console.WriteLine("Error, specify one of /formulas:... or /generateFormulaSkeletons:...");

+                    Environment.Exit(1);

+                }

+

+                CommandLineOptions.inputFiles = new List<string>();

+                CommandLineOptions.inputFiles.Add("temp_unstructured.bpl");

+                if (CommandLineOptions.formulasFile != null)

+                {

+                    CommandLineOptions.inputFiles.Add(CommandLineOptions.formulasFile);

+                }

+

+            }

+

             Program program = ParseBoogieProgram(CommandLineOptions.inputFiles, false);

             if (program == null)

             {

@@ -59,54 +92,10 @@ namespace GPUVerify
                 Environment.Exit(1);

             }

 

-            GPUVerifier verifier = new GPUVerifier(program);

-

-            // TODO: check that no non-barrier procedures are called from the kernel

-

-            verifier.AddInitialAndFinalBarriers();

-

-            verifier.SplitBlocksAtBarriers();

-

-

-            if (CommandLineOptions.formulaSkeletonsFile != null)

-            {

-                Console.WriteLine("Generating skeleton formulas to \"" + CommandLineOptions.formulaSkeletonsFile + "\" and exiting");

-                verifier.GenerateFormulaSkeletons(CommandLineOptions.formulaSkeletonsFile);

-                Environment.Exit(0);

-            }

-

-            verifier.GenerateBarrierToNextBarriersProcedures();

-

-            verifier.GenerateBarrierToBarrierPairProcedures();

-

-            verifier.GenerateBarrierToNextBarriersVCs();

-

-            verifier.GenerateBarrierToBarrierPairVCs();

-

-            verifier.AddArrayBaseDeclarations();

-

-            using (TokenTextWriter writer = (CommandLineOptions.outputFile == null ? new TokenTextWriter("<console>", Console.Out) : new TokenTextWriter(CommandLineOptions.outputFile)))

-            {

-                program.Emit(writer);

-            }

-

-

-            /*            errorCount = program.Resolve();

-                        if (errorCount != 0)

-                        {

-                            Console.WriteLine("{0} name resolution errors detected in {1} after transformation", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);

-                            Environment.Exit(1);

-                        }

+            GPUVerifier verifier = new GPUVerifierLockStep(program);

 

-                        errorCount = program.Typecheck();

+            verifier.doit();

 

-                        if (errorCount != 0)

-                        {

-                            Console.WriteLine("{0} type checking errors detected in {1} after transformation", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);

-                            Environment.Exit(1);

-                        }

-            */

-            //Console.ReadLine();

 

         }

 

diff --git a/Source/GPUVerify/ReadCollector.cs b/Source/GPUVerify/ReadCollector.cs
index e7fd1eee..7c2d2dfc 100644
--- a/Source/GPUVerify/ReadCollector.cs
+++ b/Source/GPUVerify/ReadCollector.cs
@@ -17,8 +17,8 @@ namespace GPUVerify
 

         public HashSet<AccessRecord> accesses = new HashSet<AccessRecord>();

 

-        public ReadCollector(GPUVerifier verifier)

-            : base(verifier)

+        public ReadCollector(List<Variable> GlobalVariables, List<Variable> TileStaticVariables)

+            : base(GlobalVariables, TileStaticVariables)

         {

         }

 

@@ -38,8 +38,8 @@ namespace GPUVerify
 

                 Variable ReadVariable = null;

                 Expr IndexX = node.Args[1];

-                Expr IndexY = new LiteralExpr(Token.NoToken, BigNum.FromInt(0));

-                Expr IndexZ = new LiteralExpr(Token.NoToken, BigNum.FromInt(0));

+                Expr IndexY = null;

+                Expr IndexZ = null;

 

                 if (node.Args[0] is NAryExpr)

                 {

@@ -83,7 +83,7 @@ namespace GPUVerify
                 this.VisitExpr(node.Args[1]);

 

 

-                if (verifier.GetGlobalVariables().Contains(ReadVariable) || verifier.GetTileStaticVariables().Contains(ReadVariable))

+                if (GlobalVariables.Contains(ReadVariable) || TileStaticVariables.Contains(ReadVariable))

                 {

                     accesses.Add(new AccessRecord(ReadVariable, IndexZ, IndexY, IndexX));

                 }

@@ -100,12 +100,12 @@ namespace GPUVerify
 

         public override Variable VisitVariable(Variable node)

         {

-            if (!(verifier.GetGlobalVariables().Contains(node) || verifier.GetTileStaticVariables().Contains(node)))

+            if (!(GlobalVariables.Contains(node) || TileStaticVariables.Contains(node)))

             {

                 return node;

             }

 

-            accesses.Add(new AccessRecord(node, new LiteralExpr(node.tok, BigNum.FromInt(0)), new LiteralExpr(node.tok, BigNum.FromInt(0)), new LiteralExpr(node.tok, BigNum.FromInt(0))));

+            accesses.Add(new AccessRecord(node, null, null, null));

 

             return node;

         }

diff --git a/Source/GPUVerify/Scripts/GPUVerifyDriver.bat b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat
index d81c0fc1..959a326b 100644
--- a/Source/GPUVerify/Scripts/GPUVerifyDriver.bat
+++ b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat
@@ -40,7 +40,7 @@ GOTO Generate
 

 :Verify

 echo Verify

-GPUVerify temp_unstructured.bpl /print:temp_ready_to_verify.bpl

+GPUVerify temp_unstructured.bpl /print:temp_ready_to_verify.bpl /newRaceDetectionMethod

 Boogie temp_ready_to_verify.bpl formulas.bpl /prover:smtlib

 del temp_unstructured.bpl

 GOTO End

diff --git a/Source/GPUVerify/WriteCollector.cs b/Source/GPUVerify/WriteCollector.cs
index e91244cb..14472f85 100644
--- a/Source/GPUVerify/WriteCollector.cs
+++ b/Source/GPUVerify/WriteCollector.cs
@@ -13,17 +13,17 @@ namespace GPUVerify
 

         private AccessRecord access = null;

 

-        public WriteCollector(GPUVerifier verifier)

-            : base(verifier)

+        public WriteCollector(List<Variable> GlobalVariables, List<Variable> TileStaticVariables)

+            : base(GlobalVariables, TileStaticVariables)

         {

         }

 

         public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)

         {

             Debug.Assert(NoWrittenVariable());

-            if (verifier.GetGlobalVariables().Contains(node.DeepAssignedVariable) || verifier.GetTileStaticVariables().Contains(node.DeepAssignedVariable))

+            if (GlobalVariables.Contains(node.DeepAssignedVariable) || TileStaticVariables.Contains(node.DeepAssignedVariable))

             {

-                access = new AccessRecord(node.DeepAssignedVariable, new LiteralExpr(node.tok, BigNum.FromInt(0)), new LiteralExpr(node.tok, BigNum.FromInt(0)), new LiteralExpr(node.tok, BigNum.FromInt(0)));

+                access = new AccessRecord(node.DeepAssignedVariable, null, null, null);

             }

             return node;

         }

@@ -37,7 +37,7 @@ namespace GPUVerify
         {

             Debug.Assert(NoWrittenVariable());

 

-            if (!(verifier.GetGlobalVariables().Contains(node.DeepAssignedVariable) || verifier.GetTileStaticVariables().Contains(node.DeepAssignedVariable)))

+            if (!(GlobalVariables.Contains(node.DeepAssignedVariable) || TileStaticVariables.Contains(node.DeepAssignedVariable)))

             {

                 return node;

             }

@@ -48,8 +48,8 @@ namespace GPUVerify
 

             CheckMapIndex(MapAssignX);

             Expr IndexX = MapAssignX.Indexes[0];

-            Expr IndexY = new LiteralExpr(Token.NoToken, BigNum.FromInt(0));

-            Expr IndexZ = new LiteralExpr(Token.NoToken, BigNum.FromInt(0));

+            Expr IndexY = null;

+            Expr IndexZ = null;

 

             if (MapAssignX.Map is MapAssignLhs)

             {