summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/GPUVerify/ArrayControlFlowAnalyser.cs4
-rw-r--r--Source/GPUVerify/GPUVerifier.cs120
-rw-r--r--Source/GPUVerify/IRaceInstrumenter.cs2
-rw-r--r--Source/GPUVerify/NonLocalAccessCollector.cs1
-rw-r--r--Source/GPUVerify/NullRaceInstrumenter.cs2
-rw-r--r--Source/GPUVerify/RaceInstrumenter.cs17
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs4
7 files changed, 107 insertions, 43 deletions
diff --git a/Source/GPUVerify/ArrayControlFlowAnalyser.cs b/Source/GPUVerify/ArrayControlFlowAnalyser.cs
index d7841f0e..649d76d7 100644
--- a/Source/GPUVerify/ArrayControlFlowAnalyser.cs
+++ b/Source/GPUVerify/ArrayControlFlowAnalyser.cs
@@ -172,7 +172,9 @@ namespace GPUVerify
{
CallCmd callCmd = c as CallCmd;
- if (callCmd.callee != verifier.BarrierProcedure.Name)
+ if (callCmd.callee != verifier.BarrierProcedure.Name &&
+ callCmd.callee != verifier.BarrierInvariantProcedure.Name &&
+ callCmd.callee != verifier.BarrierInvariantInstantiationProcedure.Name)
{
Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 868bcaa1..85821da2 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -18,7 +18,9 @@ namespace GPUVerify
public Procedure KernelProcedure;
public Implementation KernelImplementation;
- public Procedure BarrierProcedure;
+ public Procedure BarrierProcedure;
+ public Procedure BarrierInvariantProcedure;
+ public Procedure BarrierInvariantInstantiationProcedure;
public IKernelArrayInfo KernelArrayInfo = new KernelArrayInfoLists();
@@ -128,6 +130,42 @@ namespace GPUVerify
ResContext.AddProcedure(p);
}
return p;
+ }
+
+ private Procedure FindOrCreateBarrierInvariantProcedure() {
+ var p = CheckSingleInstanceOfAttributedProcedure("barrier_invariant");
+ if (p == null) {
+ p = new Procedure(Token.NoToken, "barrier_invariant", new TypeVariableSeq(),
+ new VariableSeq(new Variable[] {
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__cond",
+ Microsoft.Boogie.Type.Bool), true)
+ }),
+ new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(),
+ new EnsuresSeq(),
+ new QKeyValue(Token.NoToken, "barrier_invariant", new List<object>(), null));
+ Program.TopLevelDeclarations.Add(p);
+ ResContext.AddProcedure(p);
+ }
+ return p;
+ }
+
+ private Procedure FindOrCreateBarrierInvariantInstantiationProcedure() {
+ var p = CheckSingleInstanceOfAttributedProcedure("barrier_invariant_instantiation");
+ if (p == null) {
+ p = new Procedure(Token.NoToken, "barrier_invariant_instantiation", new TypeVariableSeq(),
+ new VariableSeq(new Variable[] {
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__t1",
+ new BvType(32)), true),
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__t2",
+ new BvType(32)), true)
+ }),
+ new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(),
+ new EnsuresSeq(),
+ new QKeyValue(Token.NoToken, "barrier_invariant_instantiation", new List<object>(), null));
+ Program.TopLevelDeclarations.Add(p);
+ ResContext.AddProcedure(p);
+ }
+ return p;
}
private Procedure CheckSingleInstanceOfAttributedProcedure(string attribute)
@@ -1376,17 +1414,21 @@ namespace GPUVerify
if(KernelArrayInfo.getGroupSharedArrays().Count > 0) {
- Expr IfGuard1 = Expr.And(P1, LocalFence1);
- Expr IfGuard2 = Expr.And(P2, LocalFence2);
-
- bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
- 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(MakeResetBlocks(2, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),
- null));
-
- bigblocks.AddRange(MakeHavocBlocks(KernelArrayInfo.getGroupSharedArrays()));
+ bigblocks.AddRange(
+ MakeResetBlocks(Expr.And(P1, LocalFence1), KernelArrayInfo.getGroupSharedArrays()));
+
+ // This could be relaxed to take into account whether the threads are in different
+ // groups, but for now we keep it relatively simple
+
+ Expr AtLeastOneEnabledWithLocalFence =
+ Expr.Or(Expr.And(P1, LocalFence1), Expr.And(P2, LocalFence2));
+
+ if (SomeArrayModelledNonAdversarially(KernelArrayInfo.getGroupSharedArrays())) {
+ bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
+ new IfCmd(Token.NoToken,
+ AtLeastOneEnabledWithLocalFence,
+ new StmtList(MakeHavocBlocks(KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null), null));
+ }
}
if (KernelArrayInfo.getGlobalArrays().Count > 0)
@@ -1394,14 +1436,18 @@ namespace GPUVerify
Expr IfGuard1 = Expr.And(P1, GlobalFence1);
Expr IfGuard2 = Expr.And(P2, GlobalFence2);
- bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
- 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(MakeResetBlocks(2, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),
- null));
-
- bigblocks.AddRange(MakeHavocBlocks(KernelArrayInfo.getGlobalArrays()));
+ bigblocks.AddRange(
+ MakeResetBlocks(Expr.And(P1, GlobalFence1), KernelArrayInfo.getGlobalArrays()));
+
+ Expr ThreadsInSameGroup_BothEnabled_AtLeastOneGlobalFence =
+ Expr.And(Expr.And(GPUVerifier.ThreadsInSameGroup(), Expr.And(P1, P2)), Expr.Or(GlobalFence1, GlobalFence2));
+
+ if (SomeArrayModelledNonAdversarially(KernelArrayInfo.getGlobalArrays())) {
+ bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),
+ new IfCmd(Token.NoToken,
+ ThreadsInSameGroup_BothEnabled_AtLeastOneGlobalFence,
+ new StmtList(MakeHavocBlocks(KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null), null));
+ }
}
StmtList statements = new StmtList(bigblocks, BarrierProcedure.tok);
@@ -1432,16 +1478,16 @@ namespace GPUVerify
new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 1));
}
- private List<BigBlock> MakeResetBlocks(int Thread, ICollection<Variable> variables)
+ private List<BigBlock> MakeResetBlocks(Expr ResetCondition, ICollection<Variable> variables)
{
Debug.Assert(variables.Count > 0);
- List<BigBlock> ResetAndHavocBlocks = new List<BigBlock>();
+ List<BigBlock> result = new List<BigBlock>();
foreach (Variable v in variables)
{
- ResetAndHavocBlocks.Add(RaceInstrumenter.MakeResetReadWriteSetStatements(v, Thread));
+ result.Add(RaceInstrumenter.MakeResetReadWriteSetStatements(v, ResetCondition));
}
- Debug.Assert(ResetAndHavocBlocks.Count > 0);
- return ResetAndHavocBlocks;
+ Debug.Assert(result.Count > 0);
+ return result;
}
private List<BigBlock> MakeHavocBlocks(ICollection<Variable> variables) {
@@ -1451,8 +1497,19 @@ namespace GPUVerify
if (!ArrayModelledAdversarially(v)) {
result.Add(HavocSharedArray(v));
}
- }
+ }
+ Debug.Assert(result.Count > 0);
return result;
+ }
+
+ private bool SomeArrayModelledNonAdversarially(ICollection<Variable> variables) {
+ Debug.Assert(variables.Count > 0);
+ foreach (Variable v in variables) {
+ if (!ArrayModelledAdversarially(v)) {
+ return true;
+ }
+ }
+ return false;
}
public static bool HasZDimension(Variable v)
@@ -1765,7 +1822,7 @@ namespace GPUVerify
}
else if (c is AssertCmd)
{
- result.simpleCmds.Add(new AssertCmd(c.tok, PullOutNonLocalAccessesIntoTemps(result, (c as AssertCmd).Expr, impl)));
+ // Do not pull non-local accesses out of assert commands
}
else if (c is AssumeCmd)
{
@@ -1982,7 +2039,9 @@ namespace GPUVerify
private int Check()
{
- BarrierProcedure = FindOrCreateBarrierProcedure();
+ BarrierProcedure = FindOrCreateBarrierProcedure();
+ BarrierInvariantProcedure = FindOrCreateBarrierInvariantProcedure();
+ BarrierInvariantInstantiationProcedure = FindOrCreateBarrierInvariantInstantiationProcedure();
KernelProcedure = CheckExactlyOneKernelProcedure();
if (ErrorCount > 0)
@@ -2039,8 +2098,9 @@ namespace GPUVerify
{
return D as Implementation;
}
- }
- Debug.Assert(false);
+ }
+ Error(Token.NoToken, "No implementation found for procedure \"" + procedureName + "\"");
+ Environment.Exit(1);
return null;
}
diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs
index c85989c9..7f14fcd0 100644
--- a/Source/GPUVerify/IRaceInstrumenter.cs
+++ b/Source/GPUVerify/IRaceInstrumenter.cs
@@ -15,7 +15,7 @@ namespace GPUVerify
void AddRaceCheckingDeclarations();
- BigBlock MakeResetReadWriteSetStatements(Variable v, int thread);
+ BigBlock MakeResetReadWriteSetStatements(Variable v, Expr ResetCondition);
void AddRaceCheckingCandidateRequires(Procedure Proc);
diff --git a/Source/GPUVerify/NonLocalAccessCollector.cs b/Source/GPUVerify/NonLocalAccessCollector.cs
index 6a934899..d1361ff4 100644
--- a/Source/GPUVerify/NonLocalAccessCollector.cs
+++ b/Source/GPUVerify/NonLocalAccessCollector.cs
@@ -70,7 +70,6 @@ namespace GPUVerify
return collector.Accesses.Count > 0;
}
-
public override Expr VisitNAryExpr(NAryExpr node)
{
if (IsNonLocalAccess(node, NonLocalState))
diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs
index fae08aa3..6452331f 100644
--- a/Source/GPUVerify/NullRaceInstrumenter.cs
+++ b/Source/GPUVerify/NullRaceInstrumenter.cs
@@ -24,7 +24,7 @@ namespace GPUVerify
}
- public Microsoft.Boogie.BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread)
+ public Microsoft.Boogie.BigBlock MakeResetReadWriteSetStatements(Variable v, Expr ResetCondition)
{
return new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);
}
diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs
index c73b9b13..71214cb3 100644
--- a/Source/GPUVerify/RaceInstrumenter.cs
+++ b/Source/GPUVerify/RaceInstrumenter.cs
@@ -473,16 +473,17 @@ namespace GPUVerify {
}
- public BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread) {
+ public BigBlock MakeResetReadWriteSetStatements(Variable v, Expr ResetCondition) {
BigBlock result = new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);
- if (Thread == 2) {
- return result;
- }
- Expr ResetReadAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,
- new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ"))));
- Expr ResetWriteAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,
- new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE"))));
+ Expr ResetReadAssumeGuard = Expr.Imp(ResetCondition,
+ Expr.Not(new IdentifierExpr(Token.NoToken,
+ new VariableDualiser(1, null, null).VisitVariable(
+ GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ")))));
+ Expr ResetWriteAssumeGuard = Expr.Imp(ResetCondition,
+ Expr.Not(new IdentifierExpr(Token.NoToken,
+ new VariableDualiser(1, null, null).VisitVariable(
+ GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE")))));
if (verifier.KernelArrayInfo.getGlobalArrays().Contains(v)) {
ResetReadAssumeGuard = Expr.Imp(GPUVerifier.ThreadsInSameGroup(), ResetReadAssumeGuard);
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 19f98ff7..ec1514ae 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -227,6 +227,7 @@ namespace DafnyLanguage
#region keywords
case "allocated":
case "array":
+ case "as":
case "assert":
case "assume":
case "bool":
@@ -250,7 +251,7 @@ namespace DafnyLanguage
case "function":
case "ghost":
case "if":
- case "imports":
+ case "import":
case "in":
case "int":
case "invariant":
@@ -265,6 +266,7 @@ namespace DafnyLanguage
case "null":
case "object":
case "old":
+ case "opened":
case "parallel":
case "predicate":
case "print":
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 23:03:03 +0000