Asynchronous Logger

Source/Core/Core.csproj

@@ -13,4 +13,7 @@
   <PropertyGroup>
     <OutputPath>..\..\bin\</OutputPath>
   </PropertyGroup>
+  <ItemGroup>
+    <PackageReference Include="Microsoft.Tpl.Dataflow" Version="4.5.24" />
+  </ItemGroup>
 </Project>

Source/Core/IO/Logging/AsyncLogger.cs

@@ -0,0 +1,128 @@
+//-----------------------------------------------------------------------
+// <copyright file="AsyncLogger.cs">
+//      Copyright (c) Microsoft Corporation. All rights reserved.
+// 
+//      THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+//      EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+//      MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+//      IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+//      CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+//      TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+//      SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+// </copyright>
+//-----------------------------------------------------------------------
+
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+using System.Threading.Tasks.Dataflow;
+
+namespace Microsoft.PSharp.IO
+{
+    /// <summary>
+    /// The logger maintains a queue of log items,
+    /// and dequeues and writes them to a text writer
+    /// in a background thread
+    /// </summary>
+    internal sealed class AsyncLogger : StateMachineLogger
+    {
+
+        /// <summary>
+        /// Messages are tagged with this enum. The tag says how to log them
+        /// Write(Line) => Use the Write(Line) method of the underlying Writer
+        /// Wake => This is an internal message generated when the logger is being
+        /// disposed - it wakes up the dequeuing thread if it is suspended at an await
+        /// and causes it to flush all remaining messages
+        /// </summary>
+        enum ProcessingOption { Write, WriteLine, Wake };
+
+        /// <summary>
+        /// An item in the queue is the string to be logged,
+        /// and a ProcessingOption that tells what to do with the message         
+        /// </summary>
+        BufferBlock<Tuple<string, ProcessingOption>> queue;
+
+        TaskCompletionSource<bool> finished;
+        public volatile bool IsRunning;        
+        TextWriter writer;
+
+
+        public AsyncLogger(TextWriter t)
+        {
+            queue = new BufferBlock<Tuple<string, ProcessingOption>>();
+            this.IsRunning = true;
+            writer = t ?? TextWriter.Null;
+            finished = new TaskCompletionSource<bool>();
+
+            Task.Run(async () => {
+                while (this.IsRunning)
+                {
+                    var current = await queue.ReceiveAsync().ConfigureAwait(false);
+                    ProcessItem(current);
+                }
+
+                // flush the queue
+                Tuple<string, ProcessingOption> message;
+                while (queue.TryReceive(out message))
+                {                    
+                    ProcessItem(message);
+                }
+
+                finished.SetResult(true);
+            });            
+        }
+
+        private void ProcessItem(Tuple<string, ProcessingOption> current)
+        {
+            var message = current.Item1;
+            switch (current.Item2)
+            {
+                case ProcessingOption.Write:     this.writer.Write(message);
+                                                 break;
+                case ProcessingOption.WriteLine: this.writer.WriteLine(message);
+                                                 break;
+                case ProcessingOption.Wake:      break;    
+            }            
+        }
+
+        public override void Dispose()
+        {
+
+            this.IsRunning = false;
+
+            // The dequeueing task might be suspended at the await.
+            // this message will wake it up and cause it to flush
+            queue.Post(new Tuple<string, ProcessingOption>("", ProcessingOption.Wake));
+
+            finished.Task.Wait();
+
+            // mark the queue as complete
+            queue.Complete();            
+        }
+
+        public override void Write(string value)
+        {
+            queue.Post(new Tuple<string,ProcessingOption>(value, ProcessingOption.Write));
+        }
+
+        public override void Write(string format, params object[] args)
+        {
+            var value = IO.Utilities.Format(format, args);
+            queue.Post(new Tuple<string, ProcessingOption>(value, ProcessingOption.Write));
+        }
+
+        public override void WriteLine(string value)
+        {
+            queue.Post(new Tuple<string, ProcessingOption>(value, ProcessingOption.WriteLine));
+        }
+
+        public override void WriteLine(string format, params object[] args)
+        {
+            var value = IO.Utilities.Format(format, args);
+            queue.Post(new Tuple<string, ProcessingOption>(value, ProcessingOption.WriteLine));
+        }
+    }
+}

Source/Core/IO/Logging/SyncWriterLogger.cs

@@ -0,0 +1,74 @@
+//-----------------------------------------------------------------------
+// <copyright file="SyncWriterLogger.cs">
+//      Copyright (c) Microsoft Corporation. All rights reserved.
+// 
+//      THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+//      EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+//      MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+//      IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+//      CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+//      TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+//      SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+// </copyright>
+//-----------------------------------------------------------------------
+
+using System;
+using System.IO;
+
+namespace Microsoft.PSharp.IO
+{
+    /// <summary>
+    /// Logger that wraps the TextWriter passed in a thread-safe wrapper
+    /// </summary>
+    internal sealed class SyncWriterLogger : StateMachineLogger
+    {
+
+        TextWriter writer;
+
+
+        public SyncWriterLogger(TextWriter t)
+        {            
+            writer = t?? TextWriter.Null;
+        }
+
+        public override void Write(string value)
+        {
+            lock (writer)
+            {
+                writer.Write(value);
+            }
+        }
+
+
+        public override void Write(string format, params object[] args)
+        {
+            lock (writer)
+            {
+                writer.Write(format, args);
+            }
+        }
+
+
+        public override void WriteLine(string value)
+        {
+            lock (writer)
+            {
+                writer.WriteLine(value);
+            }
+        }
+
+
+        public override void WriteLine(string format, params object[] args)
+        {
+            lock (writer)
+            {
+                writer.WriteLine(format, args);
+            }
+        }
+
+        public override void Dispose()
+        {
+
+        }
+    }
+}

Tests/Core.Tests.Performance/Configuration.cs

@@ -15,6 +15,8 @@
 using BenchmarkDotNet.Columns;
 using BenchmarkDotNet.Configs;
 using BenchmarkDotNet.Diagnosers;
+using BenchmarkDotNet.Exporters;
+using BenchmarkDotNet.Exporters.Csv;
 
 namespace Microsoft.PSharp.Core.Tests.Performance
 {
@@ -24,6 +26,9 @@ public Configuration()
         {
             Add(MemoryDiagnoser.Default);
             //Add(StatisticColumn.OperationsPerSecond);
+            Add(StatisticColumn.Mean, StatisticColumn.Median, StatisticColumn.P95);
+            Add(RPlotExporter.Default);
+            Add(CsvMeasurementsExporter.Default);
         }
     }
 }

Tests/Core.Tests.Performance/Core.Tests.Performance.csproj

@@ -15,6 +15,6 @@
     <ProjectReference Include="..\..\Source\Core\Core.csproj" />
   </ItemGroup>
   <ItemGroup>
-    <PackageReference Include="BenchmarkDotNet" Version="0.10.3" />
+    <PackageReference Include="BenchmarkDotNet" Version="0.10.9" />
   </ItemGroup>
 </Project>