diff options
| author |  wuestholz <unknown> | 2013-12-12 00:17:43 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-12-12 00:17:43 +0100 |
| commit | 9427726a6c8454c06934974262917a33cdf5f9f5 (patch) | |
| tree | 5b3f7c68d7486298552317d1bf60c6fa5f592eab /Source/VCGeneration/VC.cs | |
| parent | 42b80a61e83e8d569700340ee9ad8f8aa3a270a8 (diff) | |
Resolve a concurrency issue (reported by Alex Summers).
Diffstat (limited to 'Source/VCGeneration/VC.cs')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 54 |
1 files changed, 31 insertions, 23 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index aaf4a014..f2df1ab0 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1658,33 +1658,41 @@ namespace VC { keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
impl.TimeLimit;
- var checker = s.parent.FindCheckerFor(timeout, false);
- if (checker == null)
- {
- isWaiting = true;
- goto waiting;
- }
- else
- {
- s = work.Pop();
- }
-
- if (CommandLineOptions.Clo.Trace && no >= 0)
+ var checker = s.parent.FindCheckerFor(timeout, false);
+ try
{
- System.Console.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...",
- s.Stats, no + 1, total, 100 * proven_cost / (proven_cost + remaining_cost));
+ if (checker == null)
+ {
+ isWaiting = true;
+ goto waiting;
+ }
+ else
+ {
+ s = work.Pop();
+ }
+
+ if (CommandLineOptions.Clo.Trace && no >= 0)
+ {
+ System.Console.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...",
+ s.Stats, no + 1, total, 100 * proven_cost / (proven_cost + remaining_cost));
+ }
+ callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
+
+ Contract.Assert(s.parent == this);
+ lock (checker)
+ {
+ s.BeginCheck(checker, callback, mvInfo, no, timeout);
+ }
+
+ no++;
+
+ currently_running.Add(s);
}
- callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
-
- Contract.Assert(s.parent == this);
- lock (checker)
+ catch (Exception)
{
- s.BeginCheck(checker, callback, mvInfo, no, timeout);
+ checker.GoBackToIdle();
+ throw;
}
-
- no++;
-
- currently_running.Add(s);
}
}
|