Maintain order of logging that results from use the -traceCaching option when using parallel Boogie (boogie-org#531)

### Changes
- Maintain order of logging that results from use the `-traceCaching` option when using parallel Boogie
- Replace `OutputCollector` with `ConcurrentToSequentialWriteManager` that allows writing to the final TextWriter immediately when child TextWriters are written to, instead of only after calls to `WriteMoreOutput`.

### Testing
- Use `%parallel-boogie` in `runtest.snapshot` which already uses `-traceCaching`
- Add a test for `ConcurrentToSequentialWriteManager`
- Tweak `test0/SplitOnEveryAssert.bpl` and `commandline/SplitOnEveryAssert.bpl` because the output order has improved slightly

Author: keyboardDrummer

Source/ExecutionEngine/ConcurrentToSequentialWriteManager.cs

@@ -0,0 +1,64 @@
+using System.Collections.Generic;
+using System.IO;
+
+namespace Microsoft.Boogie;
+
+/// <summary>
+/// Allows grouping writes from concurrent sources before sending them to a single TextWriter.
+/// For each concurrent source, a TextWriter can be spawned using AppendWriter.
+/// </summary>
+public class ConcurrentToSequentialWriteManager
+{
+  public TextWriter Writer { get; }
+  private readonly Queue<SubWriter> writers = new();
+
+  public ConcurrentToSequentialWriteManager(TextWriter writer) {
+    Writer = writer;
+  }
+
+  private readonly object myLock = new();
+
+  private void Disposed() {
+    lock (myLock) {
+      while (writers.Count > 0 && writers.Peek().Disposed) {
+        var disposedWriter = writers.Dequeue();
+        Writer.Write(disposedWriter.SetTargetAndGetBuffer(null));
+      }
+      if (writers.Count > 0) {
+        Writer.Write(writers.Peek().SetTargetAndGetBuffer(Writer));
+      }
+    }
+  }
+
+  public TextWriter AppendWriter() {
+    lock (myLock) {
+      var target = writers.Count == 0 ? Writer : null;
+      var result = new SubWriter(this, target);
+      writers.Enqueue(result);
+      return result;
+    }
+  }
+
+  class SubWriter : WriterWrapper {
+    private readonly ConcurrentToSequentialWriteManager collector;
+    private bool buffering;
+    public bool Disposed { get; private set; }
+
+    public SubWriter(ConcurrentToSequentialWriteManager collector, TextWriter target) : base(target ?? new StringWriter()) {
+      this.collector = collector;
+      buffering = target == null;
+    }
+
+    public string SetTargetAndGetBuffer(TextWriter newTarget) {
+      var result = buffering ? ((StringWriter)target).ToString() : "";
+      buffering = false;
+      target = newTarget;
+      return result;
+    }
+
+    protected override void Dispose(bool disposing) {
+      Disposed = true;
+      collector.Disposed();
+    }
+  }
+}

Source/ExecutionEngine/ExecutionEngine.cs

@@ -10,6 +10,7 @@
 using BoogiePL = Microsoft.Boogie;
 using System.Runtime.Caching;
 using System.Diagnostics;
+using System.Net.Mime;
 
 namespace Microsoft.Boogie
 {
@@ -797,7 +798,7 @@ private PipelineOutcome VerifyEachImplementation(Program program, PipelineStatis
       Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
     {
       program.DeclarationDependencies = Prune.ComputeDeclarationDependencies(Options, program);
-      var outputCollector = new OutputCollector(stablePrioritizedImpls);
+      var outputCollector = new ConcurrentToSequentialWriteManager(Console.Out);
       var outcome = PipelineOutcome.VerificationCompleted;
 
       try {
@@ -830,8 +831,9 @@ private PipelineOutcome VerifyEachImplementation(Program program, PipelineStatis
                 cts.Token.ThrowIfCancellationRequested();
               }
 
+              using var implementationWriter = outputCollector.AppendWriter();
               VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls,
-                taskIndex, outputCollector, programId);
+                taskIndex, implementationWriter, programId);
               ImplIdToCancellationTokenSource.TryRemove(id, out old);
             }
             finally {
@@ -885,7 +887,6 @@ private PipelineOutcome VerifyEachImplementation(Program program, PipelineStatis
 
       cce.NonNull(Options.TheProverFactory).Close();
 
-      outputCollector.WriteMoreOutput();
       return outcome;
     }
 
@@ -951,9 +952,8 @@ private static void CleanupRequest(string requestId)
 
     private void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er,
       string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo,
-      Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector, string programId)
+      Implementation[] stablePrioritizedImpls, int index, TextWriter output, string programId)
     {
-      var output = new StringWriter();
       Implementation impl = stablePrioritizedImpls[index];
 
       printer.Inform("", output); // newline
@@ -971,7 +971,11 @@ private void VerifyImplementation(Program program, PipelineStatistics stats, Err
           Cache.Insert(impl, verificationResult);
         }
       }
-      verificationResult.Emit(this, stats, er, index, outputCollector, output, impl, wasCached);
+      verificationResult.Emit(this, stats, er, output, impl, wasCached);
+
+      if (verificationResult.Outcome == VCGen.Outcome.Errors || Options.Trace) {
+        output.Flush();
+      }
     }
 
     private VerificationResult GetCachedVerificationResult(Implementation impl, TextWriter output)
@@ -1007,11 +1011,10 @@ private VerificationResult VerifyImplementationWithoutCaching(Program program, P
         try {
           var cancellationToken = RequestIdToCancellationTokenSource[requestId].Token;
           verificationResult.Outcome =
-            vcgen.VerifyImplementation(impl, out verificationResult.Errors,
+            vcgen.VerifyImplementation(new ImplementationRun(impl, output), out verificationResult.Errors,
               out verificationResult.VCResults, requestId, cancellationToken);
           if (Options.ExtractLoops && verificationResult.Errors != null) {
-            var vcg = vcgen as VCGen;
-            if (vcg != null) {
+            if (vcgen is VCGen vcg) {
               for (int i = 0; i < verificationResult.Errors.Count; i++) {
                 verificationResult.Errors[i] = vcg.extractLoopTrace(verificationResult.Errors[i], impl.Name,
                   program, extractLoopMappingInfo);
@@ -1023,13 +1026,13 @@ private VerificationResult VerifyImplementationWithoutCaching(Program program, P
           var errorInfo = errorInformationFactory.CreateErrorInformation(impl.tok,
             String.Format("{0} (encountered in implementation {1}).", e.Message, impl.Name), requestId, "Error");
           errorInfo.ImplementationName = impl.Name;
-          printer.WriteErrorInformation(errorInfo, output);
           if (er != null) {
             lock (er) {
               er(errorInfo);
             }
           }
 
+          verificationResult.ErrorBeforeVerification = errorInfo;
           verificationResult.Errors = null;
           verificationResult.Outcome = VCGen.Outcome.Inconclusive;
         }
@@ -1082,7 +1085,7 @@ private PipelineOutcome RunHoudini(Program program, PipelineStatistics stats, Er
       }
 
       Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics();
-      Houdini.Houdini houdini = new Houdini.Houdini(Options, program, houdiniStats);
+      Houdini.Houdini houdini = new Houdini.Houdini(Console.Out, Options, program, houdiniStats);
       Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
       houdini.Close();
 
@@ -1136,7 +1139,7 @@ public Program ProgramFromFile(string filename)
     private PipelineOutcome RunStagedHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)
     {
       Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics();
-      var stagedHoudini = new Houdini.StagedHoudini(Options, program, houdiniStats, ProgramFromFile);
+      var stagedHoudini = new Houdini.StagedHoudini(Console.Out, Options, program, houdiniStats, ProgramFromFile);
       Houdini.HoudiniOutcome outcome = stagedHoudini.PerformStagedHoudiniInference();
 
       if (Options.PrintAssignment)

Source/ExecutionEngine/OutputCollector.cs

@@ -33,7 +33,8 @@ public int ProofObligationCount
   public List<Counterexample> Errors;
   public List<VCResult> VCResults;
 
-  public ISet<byte[]> AssertionChecksums { get; private set; }
+  public ISet<byte[]> AssertionChecksums { get; }
+  public ErrorInformation ErrorBeforeVerification { get; set; }
 
   public VerificationResult(string requestId, Implementation implementation, string programId = null)
   {
@@ -47,9 +48,13 @@ public VerificationResult(string requestId, Implementation implementation, strin
     MessageIfVerifies = implementation.FindStringAttribute("msg_if_verifies");
   }
 
-  public void Emit(ExecutionEngine engine, PipelineStatistics stats, ErrorReporterDelegate er, int index,
-    OutputCollector outputCollector, StringWriter output, Implementation impl, bool wasCached)
+  public void Emit(ExecutionEngine engine, PipelineStatistics stats, ErrorReporterDelegate er, TextWriter output,
+    Implementation impl, bool wasCached)
   {
+    if (ErrorBeforeVerification != null) {
+      ExecutionEngine.printer.WriteErrorInformation(ErrorBeforeVerification, output);
+    }
+
     engine.ProcessOutcome(Outcome, Errors, engine.TimeIndication(this), stats,
       output, impl.GetTimeLimit(engine.Options), er, ImplementationName,
       ImplementationToken,
@@ -71,13 +76,5 @@ public void Emit(ExecutionEngine engine, PipelineStatistics stats, ErrorReporter
           ResourceCount);
       }
     }
-
-    outputCollector.Add(index, output);
-
-    outputCollector.WriteMoreOutput();
-
-    if (Outcome == VCGen.Outcome.Errors || engine.Options.Trace) {
-      Console.Out.Flush();
-    }
   }
 }

Source/ExecutionEngine/VerificationResult.cs

@@ -0,0 +1,88 @@
+using System;
+using System.IO;
+using System.Text;
+using System.Threading;
+using System.Threading.Tasks;
+
+namespace Microsoft.Boogie;
+
+class WriterWrapper : TextWriter {
+  protected TextWriter target;
+  public override Encoding Encoding => target.Encoding;
+
+  protected WriterWrapper(TextWriter target) {
+    this.target = target;
+  }
+
+  public override void Write(char value) {
+    target.Write(value);
+  }
+
+  public override void Write(char[] buffer, int index, int count) {
+    target.Write(buffer, index, count);
+  }
+
+  public override void Write(ReadOnlySpan<char> buffer) {
+    target.Write(buffer);
+  }
+
+  public override void Write(string value) {
+    target.Write(value);
+  }
+
+  public override void WriteLine(char[] buffer, int index, int count) {
+    target.WriteLine(buffer, index, count);
+  }
+
+  public override void WriteLine(ReadOnlySpan<char> buffer) {
+    target.WriteLine(buffer);
+  }
+
+  public override void WriteLine(StringBuilder value) {
+    target.WriteLine(value);
+  }
+
+  public override void Write(StringBuilder value) {
+    target.Write(value);
+  }
+
+  public override Task WriteAsync(char value) {
+    return target.WriteAsync(value);
+  }
+
+  public override Task WriteAsync(char[] buffer, int index, int count) {
+    return target.WriteAsync(buffer, index, count);
+  }
+
+  public override Task WriteAsync(ReadOnlyMemory<char> buffer, CancellationToken cancellationToken = new()) {
+    return target.WriteAsync(buffer, cancellationToken);
+  }
+
+  public override Task WriteAsync(string value) {
+    return target.WriteAsync(value);
+  }
+
+  public override Task WriteAsync(StringBuilder value, CancellationToken cancellationToken = new()) {
+    return target.WriteAsync(value, cancellationToken);
+  }
+
+  public override Task WriteLineAsync(char value) {
+    return target.WriteLineAsync(value);
+  }
+
+  public override Task WriteLineAsync(char[] buffer, int index, int count) {
+    return target.WriteLineAsync(buffer, index, count);
+  }
+
+  public override Task WriteLineAsync(ReadOnlyMemory<char> buffer, CancellationToken cancellationToken = new()) {
+    return target.WriteLineAsync(buffer, cancellationToken);
+  }
+
+  public override Task WriteLineAsync(string value) {
+    return target.WriteLineAsync(value);
+  }
+
+  public override Task WriteLineAsync(StringBuilder value, CancellationToken cancellationToken = new()) {
+    return target.WriteLineAsync(value, cancellationToken);
+  }
+}

Source/ExecutionEngine/WriterWrapper.cs

@@ -3,6 +3,7 @@
 using System.Collections.Concurrent;
 using System.Diagnostics;
 using System.Diagnostics.Contracts;
+using System.IO;
 using System.Linq;
 
 namespace Microsoft.Boogie.Houdini
@@ -18,14 +19,14 @@ public static ConcurrentDictionary<string, RefutedAnnotation> RefutedSharedAnnot
       get { return refutedSharedAnnotations; }
     }
 
-    public ConcurrentHoudini(HoudiniOptions options, int taskId, Program program, HoudiniSession.HoudiniStatistics stats,
+    public ConcurrentHoudini(TextWriter traceWriter, HoudiniOptions options, int taskId, Program program, HoudiniSession.HoudiniStatistics stats,
       string cexTraceFile = "houdiniCexTrace.txt") : base(options)
     {
       Contract.Assert(taskId >= 0);
       this.program = program;
       this.cexTraceFile = cexTraceFile;
       this.taskID = taskId;
-      Initialize(program, stats);
+      Initialize(traceWriter, program, stats);
     }
 
     static ConcurrentHoudini()

Source/Houdini/ConcurrentHoudini.cs

@@ -416,15 +416,15 @@ protected Houdini(HoudiniOptions options)
       this.Options = options;
     }
 
-    public Houdini(HoudiniOptions options, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.txt")
+    public Houdini(TextWriter traceWriter, HoudiniOptions options, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.txt")
     {
       this.Options = options;
       this.program = program;
       this.cexTraceFile = cexTraceFile;
-      Initialize(program, stats);
+      Initialize(traceWriter, program, stats);
     }
 
-    protected void Initialize(Program program, HoudiniSession.HoudiniStatistics stats)
+    protected void Initialize(TextWriter traceWriter, Program program, HoudiniSession.HoudiniStatistics stats)
     {
       if (Options.Trace)
       {
@@ -490,7 +490,7 @@ protected void Initialize(Program program, HoudiniSession.HoudiniStatistics stat
           }
 
           HoudiniSession session =
-            new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, taskID: GetTaskID());
+            new HoudiniSession(traceWriter, this, vcgen, proverInterface, program, impl, stats, taskID: GetTaskID());
           houdiniSessions.Add(impl, session);
         }
         catch (VCGenException)