Resolve potential concurrency bug in TestNotificationReceiver, improv…

…ing test stability (#5310)

I was inspired by this unstable test failure:
#5309 to find and fix this
concurrency issue.

### Description
- Resolve potential concurrency bug in TestNotificationReceiver. 

Here's the code and an explanation of the potential issue:
```
    public TNotification GetLast(Func<TNotification, bool> predicate) {
      var result = History.LastOrDefault(predicate);
// if another threads add an item at this point, then history returns a non-last item, and the queue will be emptied in the next statement, so waiting for a new item, which the consuming code may do because history returned a non-last item, might time out.
      ClearQueue();
      return result;
    }
```

### How has this been tested?
- No idea how to test this

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/Generic/Stringify.cs

@@ -25,7 +25,7 @@ public static class StringifyUtil {
  return overrides.Add(type, (value, writer) => writer.Write(value.ToString()));
  }
 
- public static void Stringify(this object root, TextWriter writer, bool showNullChildren = false,
+ public static void Stringify(this object? root, TextWriter writer, bool showNullChildren = false,
  ImmutableDictionary<System.Type, Action<object, TextWriter>>? overrides = null) {
 
  overrides ??= ImmutableDictionary<System.Type, Action<object, TextWriter>>.Empty;
@@ -115,7 +115,7 @@ public static class StringifyUtil {
  writer.Flush();
  }
 
- public static string Stringify(this object root, bool showNullChildren = false) {
+ public static string Stringify(this object? root, bool showNullChildren = false) {
  var stringWriter = new StringWriter();
  Stringify(root, stringWriter, showNullChildren);
  return stringWriter.ToString();

Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs

@@ -232,7 +232,7 @@ then bullspec(s[1..],u[1..])
  Assert.Equal(PublishedVerificationStatus.Queued, await PopNextStatus());
  Assert.Equal(PublishedVerificationStatus.Running, await PopNextStatus());
  Assert.Equal(PublishedVerificationStatus.Error, await PopNextStatus());
- var diagnostics1 = diagnosticsReceiver.GetLast(documentItem);
+ var diagnostics1 = diagnosticsReceiver.GetLatestAndClearQueue(documentItem);
  Assert.Equal(4, diagnostics1.Length);
  ApplyChange(ref documentItem, ((7, 25), (10, 17)), "");
  var diagnostics2 = await GetNextDiagnostics(documentItem);
@@ -244,7 +244,7 @@ then bullspec(s[1..],u[1..])
  Assert.Equal(PublishedVerificationStatus.Queued, await PopNextStatus());
  Assert.Equal(PublishedVerificationStatus.Running, await PopNextStatus());
  Assert.Equal(PublishedVerificationStatus.Error, await PopNextStatus());
- var diagnostics3 = diagnosticsReceiver.GetLast(documentItem);
+ var diagnostics3 = diagnosticsReceiver.GetLatestAndClearQueue(documentItem);
  Assert.Equal(6, diagnostics3.Length);
  await AssertNoDiagnosticsAreComing(CancellationToken);
  }
@@ -1122,7 +1122,7 @@ method test()
  var documentItem = CreateTestDocument(source, "ApplyChangeBeforeVerificationFinishes.dfy");
  client.OpenDocument(documentItem);
  var status = await WaitForStatus(new Range(0, 7, 0, 11), PublishedVerificationStatus.Error);
- var firstVerificationDiagnostics = diagnosticsReceiver.GetLast(documentItem);
+ var firstVerificationDiagnostics = diagnosticsReceiver.GetLatestAndClearQueue(documentItem);
  Assert.Single(firstVerificationDiagnostics);
 
  // Second verification diagnostics get cancelled.

Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs

@@ -180,7 +180,7 @@ protected ClientBasedLanguageServerTest(ITestOutputHelper output, LogLevel dafny
  return null;
  }
 
- var fileVerificationStatus = verificationStatusReceiver.GetLast(v => v.Uri == documentId.Uri);
+ var fileVerificationStatus = verificationStatusReceiver.GetLatestAndClearQueue(v => v.Uri == documentId.Uri);
  if (fileVerificationStatus != null && fileVerificationStatus.Version == documentId.Version) {
  while (fileVerificationStatus.Uri != documentId.Uri || !fileVerificationStatus.NamedVerifiables.All(FinishedStatus)) {
  fileVerificationStatus = await verificationStatusReceiver.AwaitNextNotificationAsync(cancellationToken.Value);
@@ -201,7 +201,7 @@ protected ClientBasedLanguageServerTest(ITestOutputHelper output, LogLevel dafny
  public async Task<bool> WaitUntilResolutionFinished(TextDocumentItem documentId,
  CancellationToken cancellationToken = default) {
 
- CompilationStatusParams compilationStatusParams = compilationStatusReceiver.GetLast(s => s.Uri == documentId.Uri);
+ CompilationStatusParams compilationStatusParams = compilationStatusReceiver.GetLatestAndClearQueue(s => s.Uri == documentId.Uri);
  while (compilationStatusParams == null || compilationStatusParams.Version != documentId.Version || compilationStatusParams.Uri != documentId.Uri ||
  compilationStatusParams.Status is CompilationStatus.Parsing or CompilationStatus.ResolutionStarted) {
  compilationStatusParams = await compilationStatusReceiver.AwaitNextNotificationAsync(cancellationToken);
@@ -210,22 +210,23 @@ protected ClientBasedLanguageServerTest(ITestOutputHelper output, LogLevel dafny
  return compilationStatusParams.Status == CompilationStatus.ResolutionSucceeded;
  }
 
- public async Task<PublishDiagnosticsParams> GetLastDiagnosticsParams(TextDocumentItem documentItem, CancellationToken cancellationToken, bool allowStale = false) {
+ public async Task<PublishDiagnosticsParams> GetLatestDiagnosticsParams(TextDocumentItem documentItem, CancellationToken cancellationToken, bool allowStale = false) {
  var status = await WaitUntilAllStatusAreCompleted(documentItem, cancellationToken, allowStale);
- var result = diagnosticsReceiver.History.LastOrDefault(d => d.Uri == documentItem.Uri);
+ var result = diagnosticsReceiver.GetLatestAndClearQueue(d => d.Uri == documentItem.Uri);
  while (result == null) {
- var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken);
- result = diagnosticsReceiver.History.LastOrDefault(d => d.Uri == documentItem.Uri);
+ var diagnostics = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken);
+ if (diagnostics.Uri == documentItem.Uri) {
+ result = diagnostics;
+ }
  logger.LogInformation(
  $"GetLastDiagnosticsParams didn't find the right diagnostics after getting status {status}. Waited to get these diagnostics: {diagnostics.Stringify()}");
  }
- diagnosticsReceiver.ClearQueue();
  return result;
  }
 
  public async Task<Diagnostic[]> GetLastDiagnostics(TextDocumentItem documentItem, DiagnosticSeverity minimumSeverity = DiagnosticSeverity.Warning,
  CancellationToken? cancellationToken = null, bool allowStale = false) {
- var paramsResult = await GetLastDiagnosticsParams(documentItem, cancellationToken ?? CancellationToken, allowStale);
+ var paramsResult = await GetLatestDiagnosticsParams(documentItem, cancellationToken ?? CancellationToken, allowStale);
  return paramsResult.Diagnostics.Where(d => d.Severity <= minimumSeverity).ToArray();
  }
 

Source/DafnyLanguageServer.Test/Util/DiagnosticsReceiver.cs

@@ -30,8 +30,8 @@ public class DiagnosticsReceiver : TestNotificationReceiver<PublishDiagnosticsPa
  return result.Where(d => d.Severity <= DiagnosticSeverity.Warning).ToArray();
  }
 
- public Diagnostic[] GetLast(TextDocumentIdentifier document, DiagnosticSeverity minimumSeverity = DiagnosticSeverity.Warning) {
- var last = GetLast(d => d.Uri == document.Uri);
+ public Diagnostic[] GetLatestAndClearQueue(TextDocumentIdentifier document, DiagnosticSeverity minimumSeverity = DiagnosticSeverity.Warning) {
+ var last = GetLatestAndClearQueue(d => d.Uri == document.Uri);
  return last.Diagnostics.Where(d => d.Severity <= minimumSeverity).ToArray();
  }
 

Source/DafnyLanguageServer.Test/Util/TestNotificationReceiver.cs

@@ -1,11 +1,11 @@
-using System;
-using System.Collections.Concurrent;
+#nullable enable
+using System;
 using System.Collections.Generic;
 using System.Linq;
 using System.Threading;
 using System.Threading.Tasks;
+using Microsoft.Boogie;
 using Microsoft.Extensions.Logging;
-using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using Xunit;
 
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Util {
@@ -16,8 +16,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Util {
  /// <typeparam name="TNotification">The type of the notifications sent by the language server.</typeparam>
  public class TestNotificationReceiver<TNotification> {
 
- private SemaphoreSlim availableNotifications = new(0);
- private readonly ConcurrentQueue<TNotification> notifications = new();
+ private readonly AsyncQueue<TNotification> notifications = new();
  private readonly List<TNotification> notificationHistory = new();
  private readonly ILogger logger;
 
@@ -26,46 +25,43 @@ public class TestNotificationReceiver<TNotification> {
  }
 
  public void NotificationReceived(TNotification request) {
- logger.LogTrace($"Received {request.Stringify()}");
  Assert.NotNull(request);
- notifications.Enqueue(request);
- notificationHistory.Add(request);
- availableNotifications.Release();
+ logger.LogTrace($"Received {request.Stringify()}");
+
+ lock (this) {
+ notificationHistory.Add(request);
+ notifications.Enqueue(request);
+ }
  }
 
- public bool HasPendingNotifications => !notifications.IsEmpty;
+ public bool HasPendingNotifications => notifications.Size != 0;
 
  public IReadOnlyList<TNotification> History => notificationHistory;
 
  public void ClearHistory() {
  notificationHistory.Clear();
  }
 
- public TNotification GetLast(Func<TNotification, bool> predicate) {
- var result = History.LastOrDefault(predicate);
- ClearQueue();
- return result;
- }
+ public TNotification? GetLatestAndClearQueue(Func<TNotification, bool> predicate) {
+ lock (this) {
+  while (notifications.Size > 0) {
+  _ = notifications.Dequeue(CancellationToken.None);
+  }
 
- public void ClearQueue() {
- notifications.Clear();
- availableNotifications = new(0);
+ return History.LastOrDefault(predicate);
+ }
  }
 
- public async Task<TNotification> AwaitNextNotificationAsync(CancellationToken cancellationToken) {
+ public Task<TNotification> AwaitNextNotificationAsync(CancellationToken cancellationToken) {
  var start = DateTime.Now;
  try {
- await availableNotifications.WaitAsync(cancellationToken);
+ return notifications.Dequeue(cancellationToken);
  } catch (OperationCanceledException) {
  var last = History.Any() ? History[^1].Stringify() : "none";
  logger.LogInformation($"Waited for {(DateTime.Now - start).Seconds} seconds for new notification.\n" +
  $"Last received notification was {last}");
  throw;
  }
- if (notifications.TryDequeue(out var notification)) {
- return notification;
- }
- throw new InvalidOperationException("got a signal for a received notification but it was not present in the queue");
  }
  }
 }

Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs

@@ -104,7 +104,7 @@ decreases y
  // Save and wait for the final result
  await client.SaveDocumentAndWaitAsync(documentItem, CancellationTokenWithHighTimeout);
 
- var diagnostics = await GetLastDiagnosticsParams(documentItem, CancellationToken);
+ var diagnostics = await GetLatestDiagnosticsParams(documentItem, CancellationToken);
  Assert.Equal(documentItem.Version, diagnostics.Version);
  Assert.Single(diagnostics.Diagnostics);
  Assert.Equal("assertion might not hold", diagnostics.Diagnostics.First().Message);