summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-02-10 10:13:53 -0800
committerGravatar qadeer <unknown>2014-02-10 10:13:53 -0800
commitfd9a195a8ba5188a3325ec5ad0d5f62abf5c0a94 (patch)
tree958fef86dfb139ed9a83fd11fc1ebcaf9894d840 /Source
parenta6642da2e55119f78539926112f368bfa9e88289 (diff)
fixed a problem with the nonblocking check
Diffstat (limited to 'Source')
-rw-r--r--Source/Concurrency/MoverCheck.cs13
-rw-r--r--Source/Concurrency/TypeCheck.cs6
2 files changed, 11 insertions, 8 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index fc300444..cde18ba4 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -86,13 +86,19 @@ namespace Microsoft.Boogie
moverChecking.CreateCommutativityChecker(program, second, first);
moverChecking.CreateGatePreservationChecker(program, first, second);
moverChecking.CreateFailurePreservationChecker(program, second, first);
- moverChecking.CreateNonBlockingChecker(program, first);
}
}
}
}
}
}
+ foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values)
+ {
+ if (action.IsLeftMover && action.hasAssumeCmd)
+ {
+ moverChecking.CreateNonBlockingChecker(program, action);
+ }
+ }
}
public sealed class MyDuplicator : Duplicator
@@ -562,7 +568,7 @@ namespace Microsoft.Boogie
private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)
{
- if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0 && second.isNonBlocking)
+ if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)
return;
Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
@@ -607,9 +613,6 @@ namespace Microsoft.Boogie
private void CreateNonBlockingChecker(Program program, ActionInfo second)
{
- if (second.isNonBlocking)
- return;
-
List<Variable> inputs = new List<Variable>();
inputs.AddRange(second.thisInParams);
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index a3e35a70..ce29a700 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -34,7 +34,7 @@ namespace Microsoft.Boogie
public HashSet<Variable> usedGlobalVars;
public HashSet<Variable> modifiedGlobalVars;
public HashSet<Variable> gateUsedGlobalVars;
- public bool isNonBlocking;
+ public bool hasAssumeCmd;
public bool CommutesWith(ActionInfo actionInfo)
{
@@ -68,11 +68,11 @@ namespace Microsoft.Boogie
this.thatGate = new List<AssertCmd>();
this.thatInParams = new List<Variable>();
this.thatOutParams = new List<Variable>();
- this.isNonBlocking = true;
+ this.hasAssumeCmd = false;
foreach (Block block in codeExpr.Blocks)
{
- block.Cmds.ForEach(x => this.isNonBlocking = this.isNonBlocking && !(x is AssumeCmd));
+ block.Cmds.ForEach(x => this.hasAssumeCmd = this.hasAssumeCmd || x is AssumeCmd);
}
var cmds = thisAction.Blocks[0].Cmds;