diff options
| author |  qadeer <unknown> | 2014-02-07 22:36:45 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-02-07 22:36:45 -0800 |
| commit | a6642da2e55119f78539926112f368bfa9e88289 (patch) | |
| tree | 7538752b6ffb06cc2531787b768f848cf662620d /Source/Concurrency | |
| parent | 1f0945b2744ff44091f8574237324506764cfe37 (diff) | |
added nonblocking checker for left movers
Diffstat (limited to 'Source/Concurrency')
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 48 |
1 files changed, 43 insertions, 5 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index f30213a0..fc300444 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -86,6 +86,7 @@ namespace Microsoft.Boogie moverChecking.CreateCommutativityChecker(program, second, first);
moverChecking.CreateGatePreservationChecker(program, first, second);
moverChecking.CreateFailurePreservationChecker(program, second, first);
+ moverChecking.CreateNonBlockingChecker(program, first);
}
}
}
@@ -446,12 +447,15 @@ namespace Microsoft.Boogie if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
domainNameToScope[domainName].Add(v);
}
- foreach (Variable v in first.thatInParams)
+ if (first != null)
{
- var domainName = linearTypeChecker.FindDomainName(v);
- if (domainName == null) continue;
- if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
- domainNameToScope[domainName].Add(v);
+ foreach (Variable v in first.thatInParams)
+ {
+ var domainName = linearTypeChecker.FindDomainName(v);
+ if (domainName == null) continue;
+ if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
+ domainNameToScope[domainName].Add(v);
+ }
}
foreach (Variable v in second.thisInParams)
{
@@ -600,5 +604,39 @@ namespace Microsoft.Boogie this.decls.Add(impl);
this.decls.Add(proc);
}
+
+ private void CreateNonBlockingChecker(Program program, ActionInfo second)
+ {
+ if (second.isNonBlocking)
+ return;
+
+ List<Variable> inputs = new List<Variable>();
+ inputs.AddRange(second.thisInParams);
+
+ Expr failureExpr = Expr.True;
+ List<Requires> requires = DisjointnessRequires(program, null, second);
+ requires.Add(new Requires(false, failureExpr));
+ foreach (AssertCmd assertCmd in second.thisGate)
+ {
+ requires.Add(new Requires(false, assertCmd.Expr));
+ }
+
+ Expr ensuresExpr = (new TransitionRelationComputation(program, second)).LeftMoverCompute(failureExpr);
+ List<Ensures> ensures = new List<Ensures>();
+ Ensures ensureCheck = new Ensures(false, ensuresExpr);
+ ensureCheck.ErrorData = string.Format("{0} is blocking", second.proc.Name);
+ ensures.Add(ensureCheck);
+
+ List<Block> blocks = new List<Block>();
+ blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));
+ string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name);
+ List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
+ program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));
+ Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);
+ Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
+ impl.Proc = proc;
+ this.decls.Add(impl);
+ this.decls.Add(proc);
+ }
}
}
\ No newline at end of file |