diff options
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 113 | ||||
| -rw-r--r-- | Source/GPUVerify/RaceInstrumenter.cs | 38 | ||||
| -rw-r--r-- | Source/GPUVerify/VariableDualiser.cs | 65 |
3 files changed, 119 insertions, 97 deletions
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 7e1c9370..26dffc0f 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -834,25 +834,25 @@ namespace GPUVerify - public Microsoft.Boogie.Type GetTypeOfIdX()
+ public static Microsoft.Boogie.Type GetTypeOfIdX()
{
Contract.Requires(_X != null);
return _X.TypedIdent.Type;
}
- public Microsoft.Boogie.Type GetTypeOfIdY()
+ public static Microsoft.Boogie.Type GetTypeOfIdY()
{
Contract.Requires(_Y != null);
return _Y.TypedIdent.Type;
}
- public Microsoft.Boogie.Type GetTypeOfIdZ()
+ public static Microsoft.Boogie.Type GetTypeOfIdZ()
{
Contract.Requires(_Z != null);
return _Z.TypedIdent.Type;
}
- public Microsoft.Boogie.Type GetTypeOfId(string dimension)
+ public static Microsoft.Boogie.Type GetTypeOfId(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
if (dimension.Equals("X")) return GetTypeOfIdX();
@@ -1060,7 +1060,7 @@ namespace GPUVerify }
- internal Expr ThreadsInSameGroup()
+ internal static Expr ThreadsInSameGroup()
{
return Expr.And(
Expr.And(
@@ -1297,7 +1297,7 @@ namespace GPUVerify return new Constant(tok, new TypedIdent(tok, resultWithoutThreadId.Name + "$" + number, GetTypeOfId(dimension)));
}
- internal Constant GetGroupId(string dimension)
+ internal static Constant GetGroupId(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
if (dimension.Equals("X")) return _GROUP_X;
@@ -1307,7 +1307,7 @@ namespace GPUVerify return null;
}
- internal Constant MakeGroupId(string dimension, int number)
+ internal static Constant MakeGroupId(string dimension, int number)
{
Constant resultWithoutThreadId = GetGroupId(dimension);
return new Constant(Token.NoToken, new TypedIdent(Token.NoToken, resultWithoutThreadId.Name + "$" + number, GetTypeOfId(dimension)));
@@ -1367,11 +1367,13 @@ namespace GPUVerify Expr IfGuard2 = Expr.And(P2, LocalFence2);
bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
- new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),
+ new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetBlocks(1, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),
null));
bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
- new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetAndHavocBlocks(2, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),
+ new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetBlocks(2, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),
null));
+
+ bigblocks.AddRange(MakeHavocBlocks(KernelArrayInfo.getGroupSharedArrays()));
}
if (KernelArrayInfo.getGlobalArrays().Count > 0)
@@ -1380,19 +1382,13 @@ namespace GPUVerify Expr IfGuard2 = Expr.And(P2, GlobalFence2);
bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
- new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),
+ new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetBlocks(1, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),
null));
bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
- new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetAndHavocBlocks(2, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),
+ new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetBlocks(2, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),
null));
- }
- foreach (Variable v in KernelArrayInfo.getAllNonLocalArrays())
- {
- if (!ArrayModelledAdversarially(v))
- {
- bigblocks.Add(AssumeEqualityBetweenSharedArrays(v, P1, P2, LocalFence1, LocalFence2, GlobalFence1, GlobalFence2));
- }
+ bigblocks.AddRange(MakeHavocBlocks(KernelArrayInfo.getGlobalArrays()));
}
StmtList statements = new StmtList(bigblocks, BarrierProcedure.tok);
@@ -1423,22 +1419,28 @@ namespace GPUVerify new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 1));
}
- private List<BigBlock> MakeResetAndHavocBlocks(int Thread, ICollection<Variable> variables)
+ private List<BigBlock> MakeResetBlocks(int Thread, ICollection<Variable> variables)
{
Debug.Assert(variables.Count > 0);
List<BigBlock> ResetAndHavocBlocks = new List<BigBlock>();
foreach (Variable v in variables)
{
ResetAndHavocBlocks.Add(RaceInstrumenter.MakeResetReadWriteSetStatements(v, Thread));
- if (!ArrayModelledAdversarially(v))
- {
- ResetAndHavocBlocks.Add(HavocSharedArray(v, Thread));
- }
}
Debug.Assert(ResetAndHavocBlocks.Count > 0);
return ResetAndHavocBlocks;
}
+ private List<BigBlock> MakeHavocBlocks(ICollection<Variable> variables) {
+ Debug.Assert(variables.Count > 0);
+ List<BigBlock> result = new List<BigBlock>();
+ foreach (Variable v in variables) {
+ if (!ArrayModelledAdversarially(v)) {
+ result.Add(HavocSharedArray(v));
+ }
+ }
+ return result;
+ }
public static bool HasZDimension(Variable v)
{
@@ -1459,38 +1461,13 @@ namespace GPUVerify return false;
}
- private BigBlock HavocSharedArray(Variable v, int thread)
+ private BigBlock HavocSharedArray(Variable v)
{
- 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, Expr LocalFence1, Expr LocalFence2, Expr GlobalFence1, Expr GlobalFence2)
- {
- IdentifierExpr v1 = new IdentifierExpr(Token.NoToken, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));
- IdentifierExpr v2 = new IdentifierExpr(Token.NoToken, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable));
-
- Expr AssumeGuard = Expr.Eq(v1, v2);
-
- Expr EqualityCondition = ThreadsInSameGroup();
-
- if (KernelArrayInfo.getGroupSharedArrays().Contains(v))
- {
- EqualityCondition = Expr.And(EqualityCondition,
- Expr.And(LocalFence1, LocalFence2));
- }
- else if (KernelArrayInfo.getGlobalArrays().Contains(v))
- {
- EqualityCondition = Expr.And(EqualityCondition,
- Expr.And(GlobalFence1, GlobalFence2));
- }
-
- AssumeGuard = Expr.Imp(EqualityCondition, AssumeGuard);
-
- return new BigBlock(Token.NoToken, null, new CmdSeq(new Cmd[] { new AssumeCmd(Token.NoToken, AssumeGuard) }), null, null);
+ return new BigBlock(Token.NoToken, null,
+ new CmdSeq(new Cmd[] { new HavocCmd(Token.NoToken,
+ new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(Token.NoToken, v) })) }), null, null);
}
-
internal static bool ModifiesSetContains(IdentifierExprSeq Modifies, IdentifierExpr v)
{
foreach (IdentifierExpr ie in Modifies)
@@ -1880,16 +1857,32 @@ namespace GPUVerify }
- if (d is Variable && ((d as Variable).IsMutable || IsThreadLocalIdConstant(d as Variable)
- || IsGroupIdConstant(d as Variable) ))
- {
- NewTopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable((Variable)d.Clone()));
- if (!QKeyValue.FindBoolAttribute(d.Attributes, "race_checking"))
- {
- NewTopLevelDeclarations.Add(new VariableDualiser(2, null, null).VisitVariable((Variable)d.Clone()));
- }
+ if (d is Variable && ((d as Variable).IsMutable ||
+ IsThreadLocalIdConstant(d as Variable) ||
+ IsGroupIdConstant(d as Variable))) {
+ var v = d as Variable;
+ if (KernelArrayInfo.getGlobalArrays().Contains(v)) {
+ NewTopLevelDeclarations.Add(v);
continue;
+ }
+
+ if (KernelArrayInfo.getGroupSharedArrays().Contains(v)) {
+ Variable newV = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken,
+ v.Name, new MapType(Token.NoToken, new TypeVariableSeq(),
+ new TypeSeq(new Microsoft.Boogie.Type[] { Microsoft.Boogie.Type.Bool }),
+ v.TypedIdent.Type)));
+ newV.Attributes = v.Attributes;
+ NewTopLevelDeclarations.Add(newV);
+ continue;
+ }
+
+ NewTopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable((Variable)v.Clone()));
+ if (!QKeyValue.FindBoolAttribute(v.Attributes, "race_checking")) {
+ NewTopLevelDeclarations.Add(new VariableDualiser(2, null, null).VisitVariable((Variable)v.Clone()));
+ }
+
+ continue;
}
NewTopLevelDeclarations.Add(d);
diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs index 35e7da4b..1e462635 100644 --- a/Source/GPUVerify/RaceInstrumenter.cs +++ b/Source/GPUVerify/RaceInstrumenter.cs @@ -304,12 +304,6 @@ namespace GPUVerify { foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {
AddRequiresNoPendingAccess(v);
AddRequiresSourceAccessZero(v);
-
- if (!verifier.ArrayModelledAdversarially(v)) {
- IdentifierExpr v1 = new IdentifierExpr(Token.NoToken, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));
- IdentifierExpr v2 = new IdentifierExpr(Token.NoToken, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable));
- verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.Eq(v1, v2)));
- }
}
}
@@ -491,8 +485,8 @@ namespace GPUVerify { new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE"))));
if (verifier.KernelArrayInfo.getGlobalArrays().Contains(v)) {
- ResetReadAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetReadAssumeGuard);
- ResetWriteAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetWriteAssumeGuard);
+ ResetReadAssumeGuard = Expr.Imp(GPUVerifier.ThreadsInSameGroup(), ResetReadAssumeGuard);
+ ResetWriteAssumeGuard = Expr.Imp(GPUVerifier.ThreadsInSameGroup(), ResetWriteAssumeGuard);
}
result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetReadAssumeGuard));
@@ -747,13 +741,15 @@ namespace GPUVerify { if (!verifier.ArrayModelledAdversarially(v)) {
WriteReadGuard = Expr.And(WriteReadGuard, Expr.Neq(
- MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),
- MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
+ new VariableDualiser(1, null, null).VisitExpr(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, WriteOffsetVariable), "WRITE")),
+ new VariableDualiser(2, null, null).VisitExpr(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, OffsetParameter), "READ"))
));
}
if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {
- WriteReadGuard = Expr.And(WriteReadGuard, verifier.ThreadsInSameGroup());
+ WriteReadGuard = Expr.And(WriteReadGuard, GPUVerifier.ThreadsInSameGroup());
}
WriteReadGuard = Expr.Not(WriteReadGuard);
@@ -776,13 +772,15 @@ namespace GPUVerify { new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
if (!verifier.ArrayModelledAdversarially(v)) {
WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Neq(
- MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),
- MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "WRITE")
+ new VariableDualiser(1, null, null).VisitExpr(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, WriteOffsetVariable), "WRITE")),
+ new VariableDualiser(2, null, null).VisitExpr(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, OffsetParameter), "WRITE"))
));
}
if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {
- WriteWriteGuard = Expr.And(WriteWriteGuard, verifier.ThreadsInSameGroup());
+ WriteWriteGuard = Expr.And(WriteWriteGuard, GPUVerifier.ThreadsInSameGroup());
}
WriteWriteGuard = Expr.Not(WriteWriteGuard);
@@ -801,13 +799,15 @@ namespace GPUVerify { new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
if (!verifier.ArrayModelledAdversarially(v)) {
ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Neq(
- MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetVariable)), 1, "WRITE"),
- MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
+ new VariableDualiser(1, null, null).VisitExpr(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, ReadOffsetVariable), "WRITE")),
+ new VariableDualiser(2, null, null).VisitExpr(
+ MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, OffsetParameter), "READ"))
));
}
if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {
- ReadWriteGuard = Expr.And(ReadWriteGuard, verifier.ThreadsInSameGroup());
+ ReadWriteGuard = Expr.And(ReadWriteGuard, GPUVerifier.ThreadsInSameGroup());
}
ReadWriteGuard = Expr.Not(ReadWriteGuard);
@@ -847,8 +847,8 @@ namespace GPUVerify { return new AssignCmd(lhs.tok, lhss, rhss);
}
- 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));
+ private Expr MakeAccessedIndex(Variable v, Expr offsetExpr, string AccessType) {
+ Expr result = new IdentifierExpr(v.tok, v.Clone() as Variable);
Debug.Assert(v.TypedIdent.Type is MapType);
MapType mt = v.TypedIdent.Type as MapType;
Debug.Assert(mt.Arguments.Length == 1);
diff --git a/Source/GPUVerify/VariableDualiser.cs b/Source/GPUVerify/VariableDualiser.cs index d5d9917a..ce5f78ee 100644 --- a/Source/GPUVerify/VariableDualiser.cs +++ b/Source/GPUVerify/VariableDualiser.cs @@ -54,13 +54,18 @@ namespace GPUVerify private TypedIdent DualiseTypedIdent(Variable v)
{
+ if (QKeyValue.FindBoolAttribute(v.Attributes, "global") ||
+ QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
+ return new TypedIdent(v.tok, v.Name, v.TypedIdent.Type);
+ }
- if (uniformityAnalyser == null || !uniformityAnalyser.IsUniform(procName, v.Name))
- {
- return new TypedIdent(v.tok, v.Name + "$" + id, v.TypedIdent.Type);
- }
-
+ if (uniformityAnalyser != null && uniformityAnalyser.IsUniform(procName, v.Name))
+ {
return new TypedIdent(v.tok, v.Name, v.TypedIdent.Type);
+ }
+
+ return new TypedIdent(v.tok, v.Name + "$" + id, v.TypedIdent.Type);
+
}
public override Variable VisitVariable(Variable node)
@@ -79,26 +84,50 @@ namespace GPUVerify public override Expr VisitNAryExpr(NAryExpr node)
{
- // The point of this override is to avoid dualisation of certain special
- // intrinsics that are cross-thread
+ if (node.Fun is MapSelect) {
+ Debug.Assert((node.Fun as MapSelect).Arity == 1);
+ Debug.Assert(node.Args[0] is IdentifierExpr);
+ var v = (node.Args[0] as IdentifierExpr).Decl;
+ if (QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
+ return new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new Expr[] { new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new Expr[] { node.Args[0], GroupSharedIndexingExpr() })), VisitExpr(node.Args[1]) }));
+ }
+ }
- if (node.Fun is FunctionCall)
+ // Avoid dualisation of certain special builtin functions that are cross-thread
+ if (node.Fun is FunctionCall)
+ {
+ FunctionCall call = node.Fun as FunctionCall;
+
+ if (otherFunctionNames.Contains(call.Func.Name))
{
- FunctionCall call = node.Fun as FunctionCall;
+ Debug.Assert(id == 1 || id == 2);
+ int otherId = id == 1 ? 2 : 1;
+ return new VariableDualiser(otherId, uniformityAnalyser, procName).VisitExpr(
+ node.Args[0]);
+ }
- if (otherFunctionNames.Contains(call.Func.Name))
- {
- Debug.Assert(id == 1 || id == 2);
- int otherId = id == 1 ? 2 : 1;
- return new VariableDualiser(otherId, uniformityAnalyser, procName).VisitExpr(
- node.Args[0]);
- }
+ }
- }
+ return base.VisitNAryExpr(node);
+ }
- return base.VisitNAryExpr(node);
+
+ public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) {
+
+ var v = node.DeepAssignedVariable;
+ if(QKeyValue.FindBoolAttribute(v.Attributes, "group_shared")) {
+ return new MapAssignLhs(Token.NoToken, new MapAssignLhs(Token.NoToken, node.Map,
+ new List<Expr>(new Expr[] { GroupSharedIndexingExpr() })), node.Indexes.Select(idx => this.VisitExpr(idx)).ToList());
+
+ }
+ return base.VisitMapAssignLhs(node);
}
+ private Expr GroupSharedIndexingExpr() {
+ return id == 1 ? Expr.True : GPUVerifier.ThreadsInSameGroup();
+ }
}
|