summaryrefslogtreecommitdiff
path: root/Util
diff options
context:
space:
mode:
authorGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-08-17 19:49:12 -0700
committerGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-08-17 19:49:12 -0700
commit357e22b05f9b74a82ee6bac792e6763d96a25e7a (patch)
tree9ed2d5ac0cfa3b8fbdab17ca8bd9c1b656710950 /Util
parenteaa507dad5904016694a0b019d1e2b8c6406c1c7 (diff)
DafnyExtension: improved concurrency behavior
Diffstat (limited to 'Util')
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs178
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs10
2 files changed, 93 insertions, 95 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
index d8a60647..7351ad7d 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs
@@ -1,6 +1,7 @@
using System;
using System.Collections.Generic;
using System.Threading;
+using System.Windows.Threading;
using System.Windows;
using System.Windows.Shapes;
using System.Windows.Media;
@@ -83,26 +84,30 @@ namespace DafnyLanguage
ErrorListProvider _errorProvider;
ITextBuffer _buffer;
+ readonly DispatcherTimer timer;
+
public ProgressTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITagAggregator<DafnyResolverTag> tagAggregator) {
_buffer = buffer;
_errorProvider = new ErrorListProvider(serviceProvider);
- BufferIdleEventUtil.AddBufferIdleEventListener(buffer, DoTheVerification);
+
+ timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle);
+ timer.Interval = TimeSpan.FromMilliseconds(500);
+ timer.Tick += new EventHandler(UponIdle);
+
tagAggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
buffer.Changed += new EventHandler<TextContentChangedEventArgs>(buffer_Changed);
bufferChangesPostVerificationStart.Add(new SnapshotSpan(buffer.CurrentSnapshot, 0, buffer.CurrentSnapshot.Length));
}
public void Dispose() {
- BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, DoTheVerification);
}
- // The next two fields are protected by the lock "this". The lists pointed to by the
- // fields are not to be modified.
+ // The following fields and the contents of the following two lists are protected by the lock "this".
List<SnapshotSpan> bufferChangesPreVerificationStart = new List<SnapshotSpan>(); // buffer changes after the last completed verification and before the currently running verification
List<SnapshotSpan> bufferChangesPostVerificationStart = new List<SnapshotSpan>(); // buffer changes since the start of the currently running verification
+
void buffer_Changed(object sender, TextContentChangedEventArgs e) {
- var chng = TagsChanged;
- if (chng != null) {
+ lock (this) {
foreach (var change in e.Changes) {
var startLine = e.After.GetLineFromPosition(change.NewPosition);
var endLine = e.After.GetLineFromPosition(change.NewEnd);
@@ -111,109 +116,102 @@ namespace DafnyLanguage
}
}
- // Keep track of the most recent resolution results
+ // The next field is protected by "this"
ResolverTagger resolver;
- Dafny.Program latestProgram;
- ITextSnapshot latestSnapshot;
+ // Keep track of the most recent resolution results.
void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {
var r = sender as ResolverTagger;
if (r != null) {
- // If r._program is null, then the current buffer contains a Dafny fragment that does not resolve. If it is non-null,
- // then r._program has been successfully resolved, so when things have been sufficiently idle, we're ready to verify it.
- resolver = r;
- lock (r) {
- latestProgram = r._program;
- latestSnapshot = latestProgram != null ? r._snapshot : null;
+ lock (this) {
+ resolver = r;
}
+ timer.Stop();
+ timer.Start();
}
}
- bool verificationInProgress; // this field is protected by "this"
- bool verificationRequested; // this field is protected by "this". Invariant: verificationRequested ==> verificationInProgress
- public void DoTheVerification(object sender, EventArgs args) {
- var buffer = sender as ITextBuffer;
- if (buffer != null && latestProgram != null && resolver != null) {
- bool tagsChanged = false;
- lock (this) {
- if (verificationInProgress) {
- verificationRequested = true;
- return;
- }
- verificationInProgress = true;
- // In the following, accomplish: pre, post := pre+post, {};
- if (bufferChangesPostVerificationStart.Count != 0) {
- tagsChanged = true;
- if (bufferChangesPreVerificationStart.Count == 0) {
- var empty = bufferChangesPreVerificationStart;
- bufferChangesPreVerificationStart = bufferChangesPostVerificationStart;
- bufferChangesPostVerificationStart = empty;
- } else {
- var all = new List<SnapshotSpan>();
- all.AddRange(bufferChangesPreVerificationStart);
- all.AddRange(bufferChangesPostVerificationStart);
- bufferChangesPreVerificationStart = all;
- bufferChangesPostVerificationStart = new List<SnapshotSpan>();
- }
- }
+ bool verificationInProgress; // this field is protected by "this". Invariant: !verificationInProgress ==> bufferChangesPreVerificationStart.Count == 0
+ /// <summary>
+ /// This method is invoked when the user has been idle for a little while.
+ /// Note, "sender" and "args" are allowed to be passed in as null--they are not used by this method.
+ /// </summary>
+ public void UponIdle(object sender, EventArgs args) {
+ Dafny.Program prog;
+ ITextSnapshot snap;
+ ResolverTagger r;
+ lock (this) {
+ if (verificationInProgress) {
+ // This UponIdle message came at an inopportune time--we've already kicked off a verification.
+ // Just back off.
+ return;
+ }
+
+ if (resolver == null) return;
+ lock (resolver) {
+ prog = resolver._program;
+ snap = resolver._snapshot;
+ }
+ r = resolver;
+ resolver = null;
+ if (prog == null) return;
+ // We have a successfully resolved program to verify
+
+ var resolvedVersion = snap.Version.VersionNumber;
+ if (!bufferChangesPostVerificationStart.TrueForAll(span => span.Snapshot.Version.VersionNumber <= resolvedVersion)) {
+ // There have been buffer changes since the program that was resolved. Do nothing here,
+ // and instead just await the next resolved program.
+ return;
}
- // kick off the verification
- var w = new VerificationWorker(latestProgram, resolver, this, latestSnapshot);
- var thread = new Thread(w.Start);
- thread.Start();
+ // at this time, we're committed to running the verifier
+ verificationInProgress = true;
+ // Change orange progress markers into yellow ones
+ Contract.Assert(bufferChangesPreVerificationStart.Count == 0); // follows from monitor invariant
+ var empty = bufferChangesPreVerificationStart;
+ bufferChangesPreVerificationStart = bufferChangesPostVerificationStart;
+ bufferChangesPostVerificationStart = empty;
+ // Notify to-whom-it-may-concern about the changes we just made
var chng = TagsChanged;
- if (tagsChanged && chng != null) {
- var snap = latestSnapshot;
+ if (chng != null) {
chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snap, 0, snap.Length)));
}
- }
- }
- class VerificationWorker
- {
- readonly Dafny.Program program;
- readonly ResolverTagger resolver;
- readonly ProgressTagger pt;
- readonly ITextSnapshot snapshot;
- public VerificationWorker(Dafny.Program program, ResolverTagger resolver, ProgressTagger pt, ITextSnapshot snapshot) {
- Contract.Requires(program != null);
- Contract.Requires(resolver != null);
- Contract.Requires(pt != null);
- Contract.Requires(snapshot != null);
- this.program = program;
- this.resolver = resolver;
- this.pt = pt;
- this.snapshot = snapshot;
}
+ new Thread(() => VerificationWorker(prog, snap, r)).Start();
+ }
- public void Start() {
- bool verifySomeMore = true;
- while (verifySomeMore) {
- var newErrors = new List<DafnyError>();
- bool success = DafnyDriver.Verify(program, errorInfo => {
- newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg));
- foreach (var aux in errorInfo.Aux) {
- newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg));
- }
- });
-
- lock (pt) {
- verifySomeMore = pt.verificationRequested;
- pt.verificationInProgress = verifySomeMore;
- pt.verificationRequested = false;
- if (pt.bufferChangesPreVerificationStart.Count != 0) {
- pt.bufferChangesPreVerificationStart = new List<SnapshotSpan>();
- }
- resolver.PopulateErrorList(newErrors, true, snapshot); // TODO: is this appropriate to do inside the monitor?
- }
-
- var chng = pt.TagsChanged;
- if (chng != null) {
- chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));
- }
+ /// <summary>
+ /// Thread entry point.
+ /// </summary>
+ void VerificationWorker(Dafny.Program program, ITextSnapshot snapshot, ResolverTagger errorListHolder) {
+ Contract.Requires(program != null);
+ Contract.Requires(snapshot != null);
+ Contract.Requires(errorListHolder != null);
+
+ // Run the verifier
+ var newErrors = new List<DafnyError>();
+ bool success = DafnyDriver.Verify(program, errorInfo => {
+ newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg));
+ foreach (var aux in errorInfo.Aux) {
+ newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg));
}
+ });
+ errorListHolder.PopulateErrorList(newErrors, true, snapshot);
+
+ lock (this) {
+ bufferChangesPreVerificationStart.Clear();
+ verificationInProgress = false;
+ }
+ // Notify to-whom-it-may-concern about the cleared pre-verification changes
+ var chng = TagsChanged;
+ if (chng != null) {
+ chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));
}
+
+ // If new changes took place since we started the verification, we may need to kick off another verification
+ // immediately.
+ UponIdle(null, null);
}
public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
index 398629ab..d1af6878 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
@@ -84,7 +84,7 @@ namespace DafnyLanguage
_snapshot = null; // this makes sure the next snapshot will look different
_errorProvider = new ErrorListProvider(serviceProvider);
- BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ProcessFile);
+ BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ResolveBuffer);
}
public void Dispose() {
@@ -96,7 +96,7 @@ namespace DafnyLanguage
}
_errorProvider.Dispose();
}
- BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ProcessFile);
+ BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);
}
public IEnumerable<DafnyError> AllErrors() {
@@ -154,15 +154,15 @@ namespace DafnyLanguage
public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
/// <summary>
- /// Calls the Dafny parser/resolver/type checker on the program, updates the Error List accordingly.
+ /// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly.
/// </summary>
- void ProcessFile(object sender, EventArgs args) {
+ void ResolveBuffer(object sender, EventArgs args) {
ITextSnapshot snapshot = _buffer.CurrentSnapshot;
if (snapshot == _snapshot)
return; // we've already done this snapshot
NormalizedSnapshotSpanCollection spans = new NormalizedSnapshotSpanCollection(new SnapshotSpan(snapshot, 0, snapshot.Length));
- var driver = new DafnyDriver(_buffer.CurrentSnapshot.GetText(), _document != null ? _document.FilePath : "<program>");
+ var driver = new DafnyDriver(snapshot.GetText(), _document != null ? _document.FilePath : "<program>");
List<DafnyError> newErrors;
Dafny.Program program;
try {