diff options
| author |  wuestholz <unknown> | 2013-07-11 17:25:10 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-07-11 17:25:10 -0700 |
| commit | a7440ccb8d964bb99fd8772550ffd57f34064b1b (patch) | |
| tree | c0593f26d497bde03a35776f83fc6b84498bcde7 /Source/VCGeneration | |
| parent | 17f64e094fc0505e2049d0064883f4cffa2cc11b (diff) | |
Worked on the parallelization.
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 31 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 8 |
2 files changed, 19 insertions, 20 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 62f180d7..d6264c14 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -984,25 +984,32 @@ namespace VC { for (int i = 0; i < checkers.Count; i++)
{
var c = checkers.ElementAt(i);
- lock (c)
+ if (Monitor.TryEnter(c))
{
- if (c.WillingToHandle(timeout, program))
+ try
{
- c.GetReady();
- return c;
- }
- else if (c.IsIdle || c.IsClosed)
- {
- if (c.IsIdle)
+ if (c.WillingToHandle(timeout, program))
{
- c.Retarget(program, c.TheoremProver.Context, timeout);
+ c.GetReady();
return c;
}
- else
+ else if (c.IsIdle || c.IsClosed)
{
- checkers.RemoveAt(i);
+ if (c.IsIdle)
+ {
+ c.Retarget(program, c.TheoremProver.Context, timeout);
+ return c;
+ }
+ else
+ {
+ checkers.RemoveAt(i);
+ }
+ continue;
}
- continue;
+ }
+ finally
+ {
+ Monitor.Exit(c);
}
}
}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index d40b1008..4a89156b 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -317,10 +317,6 @@ namespace VC { ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
ch.ProverTask.Wait();
}
- catch
- {
- throw;
- }
finally
{
ch.GoBackToIdle();
@@ -1568,10 +1564,6 @@ namespace VC { break;
}
}
- catch
- {
- throw;
- }
finally
{
s.Checker.GoBackToIdle();
|