From 45415e8c070cfe424d4aaa01c3c19cac4dea3345 Mon Sep 17 00:00:00 2001 From: Unknown Date: Tue, 6 Sep 2011 08:57:15 -0700 Subject: Added driver script and GPUVerify libary. The driver script works around the fact that Boogie does not do deep cloning of expressions when turning a structured program into an unstructured one. --- .../GPUVerify/BoogieLibrary/GPUVerifyLibrary.bpl | 100 +++++++++++++++++++++ Source/GPUVerify/CommandLineOptions.cs | 33 ++++++- Source/GPUVerify/GPUVerifier.cs | 71 ++++++++++++--- Source/GPUVerify/LocalVariableAccessReplacer.cs | 7 +- Source/GPUVerify/Main.cs | 16 +--- Source/GPUVerify/Scripts/GPUVerifyDriver.bat | 9 ++ 6 files changed, 205 insertions(+), 31 deletions(-) create mode 100644 Source/GPUVerify/BoogieLibrary/GPUVerifyLibrary.bpl create mode 100644 Source/GPUVerify/Scripts/GPUVerifyDriver.bat (limited to 'Source/GPUVerify') diff --git a/Source/GPUVerify/BoogieLibrary/GPUVerifyLibrary.bpl b/Source/GPUVerify/BoogieLibrary/GPUVerifyLibrary.bpl new file mode 100644 index 00000000..d553689f --- /dev/null +++ b/Source/GPUVerify/BoogieLibrary/GPUVerifyLibrary.bpl @@ -0,0 +1,100 @@ +procedure {:barrier} BARRIER(); // Used to mark out barriers in the code; parameter simply lets us label each barrier + +type {:thread_id} ThreadId = Pair; + +type Pair; + +function constructPair(int, int) returns (Pair); +function getX(Pair) returns (int); +function getY(Pair) returns (int); + +axiom (forall x, y: int :: {constructPair(y, x)} (getX(constructPair(y, x)) == x) && (getY(constructPair(y, x)) == y)); +axiom (forall p: Pair :: {getX(p)} {getY(p)} constructPair(getY(p), getX(p)) == p); + +function {:inline} setX(p: Pair, x: int) returns (Pair) +{ + constructPair(getY(p), x) +} + +function {:inline} setY(p: Pair, y: int) returns (Pair) +{ + constructPair(y, getX(p)) +} + +// Thread ids + +axiom BLOCK_X == BLOCK_SIZE; +axiom BLOCK_Y == BLOCK_SIZE; +axiom TILE_X == BLOCK_SIZE; +axiom TILE_Y == BLOCK_SIZE; + +const BLOCK_X: int; +const TILE_X: int; +const NUM_TILES_X: int; +axiom TILE_X*NUM_TILES_X == BLOCK_X; + +const BLOCK_Y: int; +const TILE_Y: int; +const NUM_TILES_Y: int; +axiom TILE_Y*NUM_TILES_Y == BLOCK_Y; + +function {:inline} localId(t: ThreadId) returns (Pair) +{ + constructPair( mod(getY(t), TILE_Y ), mod(getX(t), TILE_X) ) +} + +function {:inline} tileId(t: ThreadId) returns (Pair) +{ + constructPair( div(getY(t), TILE_Y ), div(getX(t), TILE_X) ) +} + +function {:inline} distinct_same_tile(i: ThreadId, j: ThreadId) returns (bool) +{ + i != j && tileId(i) == tileId(j) +} + +function {:builtin "div"} div(int, int) : int; +function {:builtin "mod"} mod(int, int) : int; + +// These are the declarations that allow race and divergence checking + +var AT_BARRIER : [ThreadId]int; + +type ArrayBase; + +const unique nothing: ArrayBase; + +var base : [ThreadId]ArrayBase; +var offset_x : [ThreadId]int; +var offset_y : [ThreadId]int; +var offset_z : [ThreadId]int; +var is_write : [ThreadId]bool; + +function race(b: [ThreadId]ArrayBase, z: [ThreadId]int, y: [ThreadId]int, x: [ThreadId]int, is_w: [ThreadId]bool, i: ThreadId, j: ThreadId) returns (bool) +{ + (is_w[i] || is_w[j]) && (b[i] != nothing && b[j] != nothing) && (b[i] == b[j]) && (z[i] == z[j]) && (y[i] == y[j]) && (x[i] == x[j]) +} + +procedure {:inline 1} LOG_READ(b: ArrayBase, z: int, y: int, x: int, i: ThreadId) +modifies base, offset_z, offset_y, offset_x, is_write; +{ + if(*) { + base[i] := b; + offset_z[i] := z; + offset_y[i] := y; + offset_x[i] := x; + is_write[i] := false; + } +} + +procedure {:inline 1} LOG_WRITE(b: ArrayBase, z: int, y: int, x: int, i: ThreadId) +modifies base, offset_z, offset_y, offset_x, is_write; +{ + if(*) { + base[i] := b; + offset_z[i] := z; + offset_y[i] := y; + offset_x[i] := x; + is_write[i] := true; + } +} diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 80dc18ef..812d9f20 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -3,6 +3,7 @@ using System.Collections.Generic; using System.Linq; using System.Text; using System.IO; +using System.Diagnostics; namespace GPUVerify { @@ -12,11 +13,41 @@ namespace GPUVerify public static List inputFiles = new List(); + public static string outputFile = null; + public static int Parse(string[] args) { for (int i = 0; i < args.Length; i++) { - inputFiles.Add(args[i]); + bool hasColonArgument = false; + string beforeColon; + string afterColon = null; + int colonIndex = args[i].IndexOf(':'); + if (colonIndex >= 0 && (args[i].StartsWith("-") || args[i].StartsWith("/"))) { + hasColonArgument = true; + beforeColon = args[i].Substring(0, colonIndex); + afterColon = args[i].Substring(colonIndex + 1); + } else { + beforeColon = args[i]; + } + + switch (beforeColon) + { + case "-print": + case "/print": + if (!hasColonArgument) + { + Console.WriteLine("Error: filename expected after " + beforeColon + " argument"); + Environment.Exit(1); + } + Debug.Assert(afterColon != null); + outputFile = afterColon; + break; + + default: + inputFiles.Add(args[i]); + break; + } } return 0; } diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 391d7bdf..f90e521e 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -181,16 +181,6 @@ namespace GPUVerify replacer.VisitImplementation(KernelImplementation); - Console.WriteLine("After replacement we have "); - - using (TokenTextWriter writer = new TokenTextWriter("", Console.Out)) - { - KernelImplementation.Emit(writer, 1); - } - - Environment.Exit(1); - - // Check that each barrier has a positive integer id // Check that these ids are all distinct foreach (Block B in KernelImplementation.Blocks) @@ -527,6 +517,13 @@ namespace GPUVerify String NewProcedureName = "Barrier_" + GetBarrierId(B) + "_to_next_barriers"; Procedure NewProcedure = new Procedure(KernelProcedure.tok, NewProcedureName, KernelProcedure.TypeParameters, KernelProcedure.InParams, KernelProcedure.OutParams, KernelProcedure.Requires, KernelProcedure.Modifies, KernelProcedure.Ensures); + + NewProcedure.Modifies.Add(MakeBaseVariable(B.tok)); + NewProcedure.Modifies.Add(MakeOffsetXVariable(B.tok)); + NewProcedure.Modifies.Add(MakeOffsetYVariable(B.tok)); + NewProcedure.Modifies.Add(MakeOffsetZVariable(B.tok)); + NewProcedure.Modifies.Add(MakeIsWriteVariable(B.tok)); + Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(B, NewProcedureName); InstrumentWithRaceDetection(NewImplementation); @@ -536,6 +533,47 @@ namespace GPUVerify } + 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) @@ -839,6 +877,19 @@ namespace GPUVerify } + + 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)); + } + } } } diff --git a/Source/GPUVerify/LocalVariableAccessReplacer.cs b/Source/GPUVerify/LocalVariableAccessReplacer.cs index 4ec382ad..64dde7dc 100644 --- a/Source/GPUVerify/LocalVariableAccessReplacer.cs +++ b/Source/GPUVerify/LocalVariableAccessReplacer.cs @@ -33,16 +33,11 @@ namespace GPUVerify { if (verifier.GetThreadLocalVariables().Contains(node.Decl)) { - Console.WriteLine("Replacing " + node); - ExprSeq MapNameAndThreadID = new ExprSeq(); MapNameAndThreadID.Add(new IdentifierExpr(node.tok, node.Decl)); MapNameAndThreadID.Add(verifier.MakeThreadIdExpr(node.tok)); - Expr result = new NAryExpr(node.tok, new MapSelect(node.tok, 1), MapNameAndThreadID); - - Console.WriteLine("with " + result); - return result; + return new NAryExpr(node.tok, new MapSelect(node.tok, 1), MapNameAndThreadID); } diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index 7c72a87c..a0576f45 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -71,17 +71,9 @@ namespace GPUVerify verifier.ComputeBarrierToBarrierPairs(); - foreach (Variable V in verifier.GetGlobalVariables()) - { - program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V)), true)); - } + verifier.AddArrayBaseDeclarations(); - foreach (Variable V in verifier.GetTileStaticVariables()) - { - program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V)), true)); - } - - using (TokenTextWriter writer = new TokenTextWriter("", Console.Out)) + using (TokenTextWriter writer = (CommandLineOptions.outputFile == null ? new TokenTextWriter("", Console.Out) : new TokenTextWriter(CommandLineOptions.outputFile))) { program.Emit(writer); } @@ -106,10 +98,6 @@ namespace GPUVerify } - private static CtorType MakeArrayBaseType(Variable V) - { - return new CtorType(V.tok, new TypeCtorDecl(V.tok, "ArrayBase", 0), new TypeSeq()); - } diff --git a/Source/GPUVerify/Scripts/GPUVerifyDriver.bat b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat new file mode 100644 index 00000000..dda5ddcf --- /dev/null +++ b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat @@ -0,0 +1,9 @@ +echo off + +Boogie /noVerify /printUnstructured /print:temp_instrumented.bpl %1 %~p0..\BoogieLibrary\GPUVerifyLibrary.bpl + +GPUVerify temp_unstructured.bpl /print:temp_ready_to_verify.bpl + +Boogie temp_ready_to_verify.bpl /prover:smtlib + +del temp_instrumented.bpl -- cgit v1.2.3