Updates to operation group id and hardening of scheduler against hand…

…ler task changes (#434)
p-org · Jun 11, 2019 · da2a777 · da2a777
1 parent a093861
commit da2a777
Show file tree

Hide file tree

Showing 37 changed files with 953 additions and 675 deletions.
diff --git a/Common/version.props b/Common/version.props
@@ -1,7 +1,7 @@
 <!-- This file may be overwritten by automation. Only values allowed here are VersionPrefix and VersionSuffix.  -->
 <Project>
   <PropertyGroup>
-    <VersionPrefix>1.6.1</VersionPrefix>
+    <VersionPrefix>1.6.2</VersionPrefix>
     <VersionSuffix></VersionSuffix>
   </PropertyGroup>
 </Project>
diff --git a/Samples/Framework/build.props b/Samples/Framework/build.props
@@ -12,6 +12,6 @@
     <OutputPath>..\bin\</OutputPath>
   </PropertyGroup>
   <ItemGroup>
-    <PackageReference Include="Microsoft.PSharp" Version="1.6.1" />
+    <PackageReference Include="Microsoft.PSharp" Version="1.6.2" />
   </ItemGroup>
 </Project>
diff --git a/Samples/Language/build.props b/Samples/Language/build.props
@@ -10,6 +10,6 @@
     <OutputPath>..\bin\</OutputPath>
   </PropertyGroup>
   <ItemGroup>
-    <PackageReference Include="Microsoft.PSharp" Version="1.6.1" />
+    <PackageReference Include="Microsoft.PSharp" Version="1.6.2" />
   </ItemGroup>
 </Project>
diff --git a/Scripts/NuGet/PSharp.nuspec b/Scripts/NuGet/PSharp.nuspec
@@ -2,13 +2,13 @@
 <package >
   <metadata>
     <id>Microsoft.PSharp</id>
-    <version>1.6.1</version>
+    <version>1.6.2</version>
     <authors>Microsoft</authors>
     <projectUrl>https://github.com/p-org/PSharp</projectUrl>
     <license type="expression">MIT</license>
     <requireLicenseAcceptance>false</requireLicenseAcceptance>
     <description>P# is a framework for rapid development of reliable asynchronous software.</description>
-    <releaseNotes>This release contains the 1.6.1 version of the P# framework.</releaseNotes>
+    <releaseNotes>This release contains the 1.6.2 version of the P# framework.</releaseNotes>
     <copyright>© Microsoft Corporation. All rights reserved.</copyright>
     <tags>asynchrony reliability specifications reactive state-machines testing</tags>
   </metadata>

diff --git a/Source/Core/IMachineRuntime.cs b/Source/Core/IMachineRuntime.cs
@@ -60,9 +60,9 @@ public interface IMachineRuntime : IDisposable
         /// </summary>
         /// <param name="type">Type of the machine.</param>
         /// <param name="e">Optional event used during initialization.</param>
-        /// <param name="operationGroupId">Optional operation group id.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <returns>The result is the machine id.</returns>
-        MachineId CreateMachine(Type type, Event e = null, Guid operationGroupId = default);
+        MachineId CreateMachine(Type type, Event e = null, Guid opGroupId = default);
 
         /// <summary>
         /// Creates a new machine of the specified <see cref="Type"/> and name, and
@@ -72,9 +72,9 @@ public interface IMachineRuntime : IDisposable
         /// <param name="type">Type of the machine.</param>
         /// <param name="machineName">Optional machine name used for logging.</param>
         /// <param name="e">Optional event used during initialization.</param>
-        /// <param name="operationGroupId">Optional operation group id.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <returns>The result is the machine id.</returns>
-        MachineId CreateMachine(Type type, string machineName, Event e = null, Guid operationGroupId = default);
+        MachineId CreateMachine(Type type, string machineName, Event e = null, Guid opGroupId = default);
 
         /// <summary>
         /// Creates a new machine of the specified type, using the specified <see cref="MachineId"/>.
@@ -84,9 +84,9 @@ public interface IMachineRuntime : IDisposable
         /// <param name="mid">Unbound machine id.</param>
         /// <param name="type">Type of the machine.</param>
         /// <param name="e">Optional event used during initialization.</param>
-        /// <param name="operationGroupId">Optional operation group id.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <returns>The result is the machine id.</returns>
-        MachineId CreateMachine(MachineId mid, Type type, Event e = null, Guid operationGroupId = default);
+        MachineId CreateMachine(MachineId mid, Type type, Event e = null, Guid opGroupId = default);
 
         /// <summary>
         /// Creates a new machine of the specified <see cref="Type"/> and with the
@@ -96,9 +96,9 @@ public interface IMachineRuntime : IDisposable
         /// </summary>
         /// <param name="type">Type of the machine.</param>
         /// <param name="e">Optional event used during initialization.</param>
-        /// <param name="operationGroupId">Optional operation group id.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <returns>Task that represents the asynchronous operation. The task result is the machine id.</returns>
-        Task<MachineId> CreateMachineAndExecuteAsync(Type type, Event e = null, Guid operationGroupId = default);
+        Task<MachineId> CreateMachineAndExecuteAsync(Type type, Event e = null, Guid opGroupId = default);
 
         /// <summary>
         /// Creates a new machine of the specified <see cref="Type"/> and name, and with
@@ -109,9 +109,9 @@ public interface IMachineRuntime : IDisposable
         /// <param name="type">Type of the machine.</param>
         /// <param name="machineName">Optional machine name used for logging.</param>
         /// <param name="e">Optional event used during initialization.</param>
-        /// <param name="operationGroupId">Optional operation group id.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <returns>Task that represents the asynchronous operation. The task result is the machine id.</returns>
-        Task<MachineId> CreateMachineAndExecuteAsync(Type type, string machineName, Event e = null, Guid operationGroupId = default);
+        Task<MachineId> CreateMachineAndExecuteAsync(Type type, string machineName, Event e = null, Guid opGroupId = default);
 
         /// <summary>
         /// Creates a new machine of the specified <see cref="Type"/>, using the specified
@@ -123,9 +123,9 @@ public interface IMachineRuntime : IDisposable
         /// <param name="mid">Unbound machine id.</param>
         /// <param name="type">Type of the machine.</param>
         /// <param name="e">Optional event used during initialization.</param>
-        /// <param name="operationGroupId">Optional operation group id.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <returns>Task that represents the asynchronous operation. The task result is the machine id.</returns>
-        Task<MachineId> CreateMachineAndExecuteAsync(MachineId mid, Type type, Event e = null, Guid operationGroupId = default);
+        Task<MachineId> CreateMachineAndExecuteAsync(MachineId mid, Type type, Event e = null, Guid opGroupId = default);
 
         /// <summary>
         /// Creates a new machine of the specified <see cref="Type"/> and with the
@@ -135,10 +135,10 @@ public interface IMachineRuntime : IDisposable
         /// </summary>
         /// <param name="type">Type of the machine.</param>
         /// <param name="e">Optional event used during initialization.</param>
-        /// <param name="operationGroupId">Optional operation group id.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <returns>Task that represents the asynchronous operation. The task result is the machine id.</returns>
         [Obsolete("Please use IMachineRuntime.CreateMachineAndExecuteAsync(...) instead.")]
-        Task<MachineId> CreateMachineAndExecute(Type type, Event e = null, Guid operationGroupId = default);
+        Task<MachineId> CreateMachineAndExecute(Type type, Event e = null, Guid opGroupId = default);
 
         /// <summary>
         /// Creates a new machine of the specified <see cref="Type"/> and name, and with
@@ -149,10 +149,10 @@ public interface IMachineRuntime : IDisposable
         /// <param name="type">Type of the machine.</param>
         /// <param name="machineName">Optional machine name used for logging.</param>
         /// <param name="e">Optional event used during initialization.</param>
-        /// <param name="operationGroupId">Optional operation group id.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <returns>Task that represents the asynchronous operation. The task result is the machine id.</returns>
         [Obsolete("Please use IMachineRuntime.CreateMachineAndExecuteAsync(...) instead.")]
-        Task<MachineId> CreateMachineAndExecute(Type type, string machineName, Event e = null, Guid operationGroupId = default);
+        Task<MachineId> CreateMachineAndExecute(Type type, string machineName, Event e = null, Guid opGroupId = default);
 
         /// <summary>
         /// Creates a new machine of the specified <see cref="Type"/>, using the specified
@@ -164,44 +164,44 @@ public interface IMachineRuntime : IDisposable
         /// <param name="mid">Unbound machine id.</param>
         /// <param name="type">Type of the machine.</param>
         /// <param name="e">Optional event used during initialization.</param>
-        /// <param name="operationGroupId">Optional operation group id.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <returns>Task that represents the asynchronous operation. The task result is the machine id.</returns>
         [Obsolete("Please use IMachineRuntime.CreateMachineAndExecuteAsync(...) instead.")]
-        Task<MachineId> CreateMachineAndExecute(MachineId mid, Type type, Event e = null, Guid operationGroupId = default);
+        Task<MachineId> CreateMachineAndExecute(MachineId mid, Type type, Event e = null, Guid opGroupId = default);
 
         /// <summary>
         /// Sends an asynchronous <see cref="Event"/> to a machine.
         /// </summary>
         /// <param name="target">The id of the target machine.</param>
         /// <param name="e">The event to send.</param>
-        /// <param name="operationGroupId">Optional operation group id.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <param name="options">Optional configuration of a send operation.</param>
-        void SendEvent(MachineId target, Event e, Guid operationGroupId = default, SendOptions options = null);
+        void SendEvent(MachineId target, Event e, Guid opGroupId = default, SendOptions options = null);
 
         /// <summary>
         /// Sends an <see cref="Event"/> to a machine. Returns immediately if the target machine was already
         /// running. Otherwise blocks until the machine handles the event and reaches quiescense.
         /// </summary>
         /// <param name="target">The id of the target machine.</param>
         /// <param name="e">The event to send.</param>
-        /// <param name="operationGroupId">Optional operation group id.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <param name="options">Optional configuration of a send operation.</param>
         /// <returns>Task that represents the asynchronous operation. The task result is true if
         /// the event was handled, false if the event was only enqueued.</returns>
-        Task<bool> SendEventAndExecuteAsync(MachineId target, Event e, Guid operationGroupId = default, SendOptions options = null);
+        Task<bool> SendEventAndExecuteAsync(MachineId target, Event e, Guid opGroupId = default, SendOptions options = null);
 
         /// <summary>
         /// Sends an <see cref="Event"/> to a machine. Returns immediately if the target machine was already
         /// running. Otherwise blocks until the machine handles the event and reaches quiescense.
         /// </summary>
         /// <param name="target">The id of the target machine.</param>
         /// <param name="e">The event to send.</param>
-        /// <param name="operationGroupId">Optional operation group id.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <param name="options">Optional configuration of a send operation.</param>
         /// <returns>Task that represents the asynchronous operation. The task result is true if
         /// the event was handled, false if the event was only enqueued.</returns>
         [Obsolete("Please use IMachineRuntime.SendEventAndExecuteAsync(...) instead.")]
-        Task<bool> SendEventAndExecute(MachineId target, Event e, Guid operationGroupId = default, SendOptions options = null);
+        Task<bool> SendEventAndExecute(MachineId target, Event e, Guid opGroupId = default, SendOptions options = null);
 
         /// <summary>
         /// Registers a new specification monitor of the specified <see cref="Type"/>.

diff --git a/Source/Core/IO/Logging/DisposingLogger.cs b/Source/Core/IO/Logging/DisposingLogger.cs
@@ -207,10 +207,10 @@ public void OnWait(MachineId machineId, string currStateName, params Type[] even
         /// <param name="senderId">The machine that sent the event, if any.</param>
         /// <param name="senderStateName">The name of the current state of the sender machine, if any.</param>
         /// <param name="eventName">The event being sent.</param>
-        /// <param name="operationGroupId">The operation group id.</param>
+        /// <param name="opGroupId">Id used to identify the send operation.</param>
         /// <param name="isTargetHalted">Is the target machine halted.</param>
         public void OnSend(MachineId targetMachineId, MachineId senderId, string senderStateName, string eventName,
-            Guid operationGroupId, bool isTargetHalted)
+            Guid opGroupId, bool isTargetHalted)
         {
         }
 

diff --git a/Source/Core/IO/Logging/ILogger.cs b/Source/Core/IO/Logging/ILogger.cs
@@ -163,10 +163,10 @@ public interface ILogger : IDisposable
         /// <param name="senderId">The id of the machine that sent the event, if any.</param>
         /// <param name="senderStateName">The name of the current state of the sender machine, if any.</param>
         /// <param name="eventName">The event being sent.</param>
-        /// <param name="operationGroupId">The operation group id.</param>
+        /// <param name="opGroupId">Id used to identify the send operation.</param>
         /// <param name="isTargetHalted">Is the target machine halted.</param>
         void OnSend(MachineId targetMachineId, MachineId senderId, string senderStateName, string eventName,
-            Guid operationGroupId, bool isTargetHalted);
+            Guid opGroupId, bool isTargetHalted);
 
         /// <summary>
         /// Called when a machine has been created.

diff --git a/Source/Core/IO/Logging/MachineLogger.cs b/Source/Core/IO/Logging/MachineLogger.cs
@@ -379,14 +379,14 @@ public virtual string FormatOnWaitString(MachineId machineId, string currStateNa
         /// <param name="senderId">The id of the machine that sent the event, if any.</param>
         /// <param name="senderStateName">The name of the current state of the sender machine, if any.</param>
         /// <param name="eventName">The event being sent.</param>
-        /// <param name="operationGroupId">The operation group id.</param>
+        /// <param name="opGroupId">Id used to identify the send operation.</param>
         /// <param name="isTargetHalted">Is the target machine halted.</param>
         public virtual void OnSend(MachineId targetMachineId, MachineId senderId, string senderStateName, string eventName,
-            Guid operationGroupId, bool isTargetHalted)
+            Guid opGroupId, bool isTargetHalted)
         {
             if (this.IsVerbose)
             {
-                this.WriteLine(this.FormatOnSendString(targetMachineId, senderId, senderStateName, eventName, operationGroupId, isTargetHalted));
+                this.WriteLine(this.FormatOnSendString(targetMachineId, senderId, senderStateName, eventName, opGroupId, isTargetHalted));
             }
         }
 
@@ -397,15 +397,15 @@ public virtual string FormatOnWaitString(MachineId machineId, string currStateNa
         /// <param name="senderId">The id of the machine that sent the event, if any.</param>
         /// <param name="senderStateName">The name of the current state of the sender machine, if any.</param>
         /// <param name="eventName">The event being sent.</param>
-        /// <param name="operationGroupId">The operation group id.</param>
+        /// <param name="opGroupId">Id used to identify the send operation.</param>
         /// <param name="isTargetHalted">Is the target machine halted.</param>
-        public virtual string FormatOnSendString(MachineId targetMachineId, MachineId senderId, string senderStateName, string eventName,
-            Guid operationGroupId, bool isTargetHalted)
+        public virtual string FormatOnSendString(MachineId targetMachineId, MachineId senderId, string senderStateName,
+            string eventName, Guid opGroupId, bool isTargetHalted)
         {
-            var operationGroupIdMsg = operationGroupId != Guid.Empty ? $" (operation group '{operationGroupId}')" : string.Empty;
+            var opGroupIdMsg = opGroupId != Guid.Empty ? $" (operation group '{opGroupId}')" : string.Empty;
             var target = isTargetHalted ? $"halted machine '{targetMachineId}'" : $"machine '{targetMachineId}'";
             var sender = senderId != null ? $"Machine '{senderId}' in state '{senderStateName}'" : $"The runtime";
-            return $"<SendLog> {sender} sent event '{eventName}' to {target}{operationGroupIdMsg}.";
+            return $"<SendLog> {sender} sent event '{eventName}' to {target}{opGroupIdMsg}.";
         }
 
         /// <summary>