From 82375bbf46b54207fc2efcc2ac42bace5fc5e92d Mon Sep 17 00:00:00 2001 From: wuestholz Date: Sat, 28 Jun 2014 17:55:20 +0200 Subject: Changed the verification result cache to use the built-in 'MemoryCache' class. --- Source/ExecutionEngine/ExecutionEngine.cs | 7 +- Source/ExecutionEngine/ExecutionEngine.csproj | 7 +- Source/ExecutionEngine/VerificationResultCache.cs | 89 +++++++++++------------ 3 files changed, 51 insertions(+), 52 deletions(-) (limited to 'Source/ExecutionEngine') diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index cac56c4b..2b122f8f 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1001,12 +1001,13 @@ namespace Microsoft.Boogie printer.Inform("", output); // newline printer.Inform(string.Format("Verifying {0} ...", impl.Name), output); + int priority = 0; if (0 < CommandLineOptions.Clo.VerifySnapshots) { - verificationResult = Cache.Lookup(impl); + verificationResult = Cache.Lookup(impl, out priority); } - if (verificationResult != null) + if (verificationResult != null && priority == Priority.SKIP) { if (CommandLineOptions.Clo.XmlSink != null) { @@ -1096,7 +1097,7 @@ namespace Microsoft.Boogie if (0 < CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum)) { - Cache.Insert(impl.Id, verificationResult); + Cache.Insert(impl, verificationResult); } #endregion diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj index 5b854a40..84aa64d5 100644 --- a/Source/ExecutionEngine/ExecutionEngine.csproj +++ b/Source/ExecutionEngine/ExecutionEngine.csproj @@ -1,4 +1,4 @@ - + @@ -11,7 +11,7 @@ ExecutionEngine v4.0 512 - Client + true ..\InterimKey.snk 12.0.0 @@ -81,6 +81,7 @@ + @@ -146,4 +147,4 @@ --> - \ No newline at end of file + diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index 8578f144..6833f869 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -3,6 +3,7 @@ using System.Collections.Concurrent; using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using System.Runtime.Caching; using System.Text; using System.Text.RegularExpressions; using VC; @@ -61,11 +62,12 @@ namespace Microsoft.Boogie foreach (var impl in implementations) { - if (ExecutionEngine.Cache.VerificationPriority(impl) == Priority.LOW) + int priority; + var vr = ExecutionEngine.Cache.Lookup(impl, out priority); + if (vr != null && priority == Priority.LOW) { - var vr = ExecutionEngine.Cache.Lookup(impl.Id); // TODO(wuestholz): We should probably increase the threshold to something like 2 seconds. - if (vr != null && 0.0 < vr.End.Subtract(vr.Start).TotalMilliseconds) + if (0.0 < vr.End.Subtract(vr.Start).TotalMilliseconds) { if (vr.Errors != null) { @@ -275,91 +277,86 @@ namespace Microsoft.Boogie static internal class Priority { - public static int LOW = 1; - public static int MEDIUM = 2; - public static int HIGH = 3; - public static int SKIP = int.MaxValue; + public static readonly int LOW = 1; + public static readonly int MEDIUM = 2; + public static readonly int HIGH = 3; + public static readonly int SKIP = int.MaxValue; } public class VerificationResultCache { - private readonly ConcurrentDictionary Cache = new ConcurrentDictionary(); + private readonly MemoryCache Cache = new MemoryCache("VerificationResultCache"); + private readonly CacheItemPolicy Policy = new CacheItemPolicy(); - public void Insert(string key, VerificationResult result) + public VerificationResultCache() { - Contract.Requires(key != null); - Contract.Requires(result != null); - - Cache[key] = result; + Policy.SlidingExpiration = new TimeSpan(0, 5, 0); } - public VerificationResult Lookup(string key) + public void Insert(Implementation impl, VerificationResult result) { - VerificationResult result; - var success = Cache.TryGetValue(key, out result); - return success ? result : null; + Contract.Requires(impl != null); + Contract.Requires(result != null); + + Cache.Set(impl.Id, result, Policy); } - public VerificationResult Lookup(Implementation impl) + public VerificationResult Lookup(Implementation impl, out int priority) { - if (!NeedsToBeVerified(impl)) + Contract.Requires(impl != null); + + var result = Cache.Get(impl.Id) as VerificationResult; + if (result == null) + { + priority = Priority.HIGH; // high priority (has been never verified before) + } + else if (result.Checksum != impl.Checksum) { - return Lookup(impl.Id); + priority = Priority.MEDIUM; // medium priority (old snapshot has been verified before) + } + else if (impl.DependenciesChecksum == null || result.DependeciesChecksum != impl.DependenciesChecksum) + { + priority = Priority.LOW; // low priority (the same snapshot has been verified before, but a callee has changed) } else { - return null; + priority = Priority.SKIP; // skip verification (highest priority to get them done as soon as possible) } + return result; } public void Clear() { - Cache.Clear(); + Cache.Trim(100); } public void RemoveMatchingKeys(Regex keyRegexp) { + Contract.Requires(keyRegexp != null); + foreach (var kv in Cache) { if (keyRegexp.IsMatch(kv.Key)) { - VerificationResult res; - Cache.TryRemove(kv.Key, out res); + Cache.Remove(kv.Key); } } } - public bool NeedsToBeVerified(Implementation impl) - { - return VerificationPriority(impl) < Priority.SKIP; - } - - public int VerificationPriority(Implementation impl) { - if (!Cache.ContainsKey(impl.Id)) - { - return Priority.HIGH; // high priority (has been never verified before) - } - else if (Cache[impl.Id].Checksum != impl.Checksum) - { - return Priority.MEDIUM; // medium priority (old snapshot has been verified before) - } - else if (impl.DependenciesChecksum == null || Cache[impl.Id].DependeciesChecksum != impl.DependenciesChecksum) - { - return Priority.LOW; // low priority (the same snapshot has been verified before, but a callee has changed) - } - else - { - return Priority.SKIP; // skip verification (highest priority to get them done as soon as possible) - } + Contract.Requires(impl != null); + + int priority; + Lookup(impl, out priority); + return priority; } } -- cgit v1.2.3