support optional fine-grained race-checking at memory accesses (#472)

Source/Core/Configuration.cs

@@ -146,6 +146,18 @@ public class Configuration
  [DataMember]
  internal bool IsVolatileOperationRaceCheckingEnabled;
 
+ /// <summary>
+ /// If enabled, checking races at memory-access locations is enabled during systematic testing.
+ /// </summary>
+ [DataMember]
+ internal bool IsMemoryAccessRaceCheckingEnabled;
+
+ /// <summary>
+ /// If enabled, checking races at control-flow branching locations is enabled during systematic testing.
+ /// </summary>
+ [DataMember]
+ internal bool IsControlFlowRaceCheckingEnabled;
+
  /// <summary>
  /// If enabled, execution trace cycle reduction is enabled during systematic testing.
  /// </summary>
@@ -349,6 +361,8 @@ protected Configuration()
  this.IsLockAccessRaceCheckingEnabled = true;
  this.IsAtomicOperationRaceCheckingEnabled = true;
  this.IsVolatileOperationRaceCheckingEnabled = true;
+ this.IsMemoryAccessRaceCheckingEnabled = false;
+ this.IsControlFlowRaceCheckingEnabled = false;
  this.IsExecutionTraceCycleReductionEnabled = false;
  this.IsPartialOrderSamplingEnabled = false;
  this.RunTestIterationsToCompletion = false;
@@ -667,6 +681,30 @@ public Configuration WithVolatileOperationRaceCheckingEnabled(bool isEnabled = t
  return this;
  }
 
+ /// <summary>
+ /// Updates the configuration with race checking at memory-access locations enabled or disabled.
+ /// If this race checking strategy is enabled, then the runtime will explore interleavings at
+ /// memory-access locations.
+ /// </summary>
+ /// <param name="isEnabled">If true, then checking races at memory-access locations is enabled.</param>
+ public Configuration WithMemoryAccessRaceCheckingEnabled(bool isEnabled = true)
+ {
+ this.IsMemoryAccessRaceCheckingEnabled = isEnabled;
+ return this;
+ }
+
+ /// <summary>
+ /// Updates the configuration with race checking at control-flow branching locations enabled
+ /// or disabled. If this race checking strategy is enabled, then the runtime will explore
+ /// interleavings at control-flow branching locations.
+ /// </summary>
+ /// <param name="isEnabled">If true, then checking races at control-flow branching locations is enabled.</param>
+ public Configuration WithControlFlowRaceCheckingEnabled(bool isEnabled = true)
+ {
+ this.IsControlFlowRaceCheckingEnabled = isEnabled;
+ return this;
+ }
+
  /// <summary>
  /// Updates the configuration with execution trace reduction enabled or disabled. If this
  /// reduction strategy is enabled, then the runtime will attempt to reduce the schedule

Source/Core/Runtime/Scheduling/SchedulingPoint.cs

@@ -36,6 +36,55 @@ public static void Interleave()
  }
  }
 
+ /// <summary>
+ /// Explores a possible interleaving with another controlled operation
+ /// at the currently executing memory-access location.
+ /// </summary>
+ /// <remarks>This type is intended for compiler use rather than use directly in code.</remarks>
+ [System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
+ public static void InterleaveMemoryAccess()
+ {
+ var runtime = CoyoteRuntime.Current;
+ if (runtime.SchedulingPolicy != SchedulingPolicy.None &&
+ runtime.Configuration.IsMemoryAccessRaceCheckingEnabled &&
+ runtime.TryGetExecutingOperation(out ControlledOperation current))
+ {
+ if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving)
+ {
+ runtime.ScheduleNextOperation(current, SchedulingPointType.Interleave, isSuppressible: false);
+ }
+ else if (runtime.SchedulingPolicy is SchedulingPolicy.Fuzzing)
+ {
+ runtime.DelayOperation(current);
+ }
+ }
+ }
+
+ /// <summary>
+ /// Explores a possible interleaving with another controlled operation
+ /// at the currently executing control-flow branching location.
+ /// </summary>
+ /// <remarks>This type is intended for compiler use rather than use directly in code.</remarks>
+ [System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)]
+ public static void InterleaveControlFlow()
+ {
+ var runtime = CoyoteRuntime.Current;
+ if (runtime.SchedulingPolicy != SchedulingPolicy.None &&
+ runtime.Configuration.IsControlFlowRaceCheckingEnabled &&
+ !runtime.Configuration.IsMemoryAccessRaceCheckingEnabled &&
+ runtime.TryGetExecutingOperation(out ControlledOperation current))
+ {
+ if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving)
+ {
+ runtime.ScheduleNextOperation(current, SchedulingPointType.Interleave, isSuppressible: false);
+ }
+ else if (runtime.SchedulingPolicy is SchedulingPolicy.Fuzzing)
+ {
+ runtime.DelayOperation(current);
+ }
+ }
+ }
+
  /// <summary>
  /// Attempts to yield execution to another controlled operation.
  /// </summary>

Source/Test/Rewriting/AssemblySignature.cs

@@ -36,6 +36,12 @@ internal class AssemblySignature
  [DataMember]
  internal readonly IList<string> Dependencies;
 
+ /// <summary>
+ /// True if rewriting for memory locations is enabled, else false.
+ /// </summary>
+ [DataMember]
+ internal readonly bool IsRewritingMemoryLocations;
+
  /// <summary>
  /// True if rewriting for concurrent collections is enabled, else false.
  /// </summary>
@@ -60,12 +66,6 @@ internal class AssemblySignature
  [DataMember]
  internal readonly bool IsRewritingUnitTests;
 
- /// <summary>
- /// True if rewriting threads as controlled tasks.
- /// </summary>
- [DataMember]
- internal readonly bool IsRewritingThreads;
-
  /// <summary>
  /// Initializes a new instance of the <see cref="AssemblySignature"/> class.
  /// </summary>
@@ -75,11 +75,11 @@ internal AssemblySignature(AssemblyInfo assembly, HashSet<AssemblyInfo> dependen
  this.FullName = assembly.FullName;
  this.Version = rewriterVersion.ToString();
  this.Dependencies = new List<string>(dependencies.Select(dependency => dependency.FullName));
+ this.IsRewritingMemoryLocations = options.IsRewritingMemoryLocations;
  this.IsRewritingConcurrentCollections = options.IsRewritingConcurrentCollections;
  this.IsDataRaceCheckingEnabled = options.IsDataRaceCheckingEnabled;
  this.IsRewritingDependencies = options.IsRewritingDependencies;
  this.IsRewritingUnitTests = options.IsRewritingUnitTests;
- this.IsRewritingThreads = options.IsRewritingThreads;
  }
 
  /// <summary>

Source/Test/Rewriting/Passes/Rewriting/CallSiteExtractionRewritingPass.cs

@@ -27,7 +27,8 @@ internal CallSiteExtractionRewritingPass(IEnumerable<AssemblyInfo> visitedAssemb
  protected override void VisitMethodBody(MethodBody body)
  {
  if (this.IsCompilerGeneratedType || this.IsAsyncStateMachineType ||
- this.Method is null || this.Method.IsConstructor || this.Method.IsGetter || this.Method.IsSetter)
+ this.Method is null || this.Method.IsConstructor ||
+ this.Method.IsGetter || this.Method.IsSetter)
  {
  return;
  }

Source/Test/Rewriting/Passes/Rewriting/MemoryAccessRewritingPass.cs

@@ -0,0 +1,89 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System.Collections.Generic;
+using System.Linq;
+using Microsoft.Coyote.Logging;
+using Microsoft.Coyote.Runtime;
+using Mono.Cecil;
+using Mono.Cecil.Cil;
+
+namespace Microsoft.Coyote.Rewriting
+{
+ /// <summary>
+ /// Rewriting pass that adds scheduling points at memory-access locations.
+ /// </summary>
+ internal class MemoryAccessRewritingPass : RewritingPass
+ {
+ /// <summary>
+ /// Initializes a new instance of the <see cref="MemoryAccessRewritingPass"/> class.
+ /// </summary>
+ internal MemoryAccessRewritingPass(IEnumerable<AssemblyInfo> visitedAssemblies, LogWriter logWriter)
+ : base(visitedAssemblies, logWriter)
+ {
+ }
+
+ /// <inheritdoc/>
+ protected internal override void VisitMethod(MethodDefinition method)
+ {
+ if (this.IsAsyncStateMachineType ||
+ method is null || method.IsConstructor ||
+ method.IsGetter || method.IsSetter)
+ {
+ return;
+ }
+
+ base.VisitMethod(method);
+ }
+
+ /// <inheritdoc/>
+ protected override Instruction VisitInstruction(Instruction instruction)
+ {
+ if (this.Method is null)
+ {
+ return instruction;
+ }
+
+ try
+ {
+ if (instruction.OpCode == OpCodes.Ldfld || instruction.OpCode == OpCodes.Stfld)
+ {
+ this.LogWriter.LogDebug("............. [+] injected scheduling point at field-access instruction");
+
+ TypeDefinition providerType = this.Method.Module.ImportReference(typeof(SchedulingPoint)).Resolve();
+ MethodReference providerMethod = providerType.Methods.FirstOrDefault(m => m.Name is nameof(SchedulingPoint.InterleaveMemoryAccess));
+ providerMethod = this.Method.Module.ImportReference(providerMethod);
+
+ if (instruction.Previous != null && instruction.Previous.OpCode == OpCodes.Volatile)
+ {
+ this.Processor.InsertBefore(instruction.Previous, Instruction.Create(OpCodes.Call, providerMethod));
+ }
+ else
+ {
+ this.Processor.InsertBefore(instruction, Instruction.Create(OpCodes.Call, providerMethod));
+ }
+
+ this.IsMethodBodyModified = true;
+ }
+ else if (instruction.OpCode == OpCodes.Brfalse || instruction.OpCode == OpCodes.Brfalse_S ||
+ instruction.OpCode == OpCodes.Brtrue || instruction.OpCode == OpCodes.Brtrue_S)
+ {
+ this.LogWriter.LogDebug("............. [+] injected scheduling point at branching instruction");
+
+ TypeDefinition providerType = this.Method.Module.ImportReference(typeof(SchedulingPoint)).Resolve();
+ MethodReference providerMethod = providerType.Methods.FirstOrDefault(m => m.Name is nameof(SchedulingPoint.InterleaveControlFlow));
+ providerMethod = this.Method.Module.ImportReference(providerMethod);
+ this.Processor.InsertBefore(instruction, Instruction.Create(OpCodes.Call, providerMethod));
+
+ this.IsMethodBodyModified = true;
+ }
+ }
+ catch (AssemblyResolutionException)
+ {
+ // Skip this instruction, we are only interested in types that can be resolved.
+ }
+
+ return instruction;
+ }
+ }
+}

Source/Test/Rewriting/Passes/Rewriting/UncontrolledInvocationRewritingPass.cs

@@ -59,7 +59,7 @@ protected override Instruction VisitInstruction(Instruction instruction)
  {
  this.LogWriter.LogDebug("............. [+] injected uncontrolled '{0}' invocation exception", invocationName);
 
- var providerType = this.Method.Module.ImportReference(typeof(ExceptionProvider)).Resolve();
+ TypeDefinition providerType = this.Method.Module.ImportReference(typeof(ExceptionProvider)).Resolve();
  MethodReference providerMethod = isDataNondeterministic ?
  providerType.Methods.FirstOrDefault(m => m.Name is nameof(ExceptionProvider.ThrowUncontrolledDataInvocationException)) :
  providerType.Methods.FirstOrDefault(m => m.Name is nameof(ExceptionProvider.ThrowUncontrolledInvocationException));

Source/Test/Rewriting/RewritingEngine.cs

@@ -143,6 +143,12 @@ private void InitializePasses(IEnumerable<AssemblyInfo> assemblies)
  this.Passes.AddLast(new MSTestRewritingPass(this.Configuration, assemblies, this.LogWriter));
  }
 
+ if (this.Options.IsRewritingMemoryLocations)
+ {
+ // Add a pass that rewrites memory-access locations for checking fine-grained races.
+ this.Passes.AddLast(new MemoryAccessRewritingPass(assemblies, this.LogWriter));
+ }
+
  this.Passes.AddLast(new InterAssemblyInvocationRewritingPass(assemblies, this.LogWriter));
  this.Passes.AddLast(new UncontrolledInvocationRewritingPass(assemblies, this.LogWriter));
 

Source/Test/Rewriting/RewritingOptions.cs

@@ -60,6 +60,11 @@ internal class RewritingOptions
  /// </remarks>
  private Regex IgnoredAssembliesPattern { get; set; }
 
+ /// <summary>
+ /// True if rewriting for memory locations is enabled, else false.
+ /// </summary>
+ internal bool IsRewritingMemoryLocations { get; set; }
+
  /// <summary>
  /// True if rewriting for concurrent collections is enabled, else false.
  /// </summary>
@@ -80,11 +85,6 @@ internal class RewritingOptions
  /// </summary>
  internal bool IsRewritingUnitTests { get; set; }
 
- /// <summary>
- /// True if rewriting threads as controlled tasks.
- /// </summary>
- internal bool IsRewritingThreads { get; set; }
-
  /// <summary>
  /// True if the rewriter should log the IL before and after rewriting.
  /// </summary>
@@ -113,11 +113,11 @@ internal static RewritingOptions Create() =>
  AssemblyPaths = new HashSet<string>(),
  DependencySearchPaths = null,
  IgnoredAssembliesPattern = GetDisallowedAssembliesRegex(new List<string>()),
+ IsRewritingMemoryLocations = true,
  IsRewritingConcurrentCollections = true,
  IsDataRaceCheckingEnabled = false,
  IsRewritingDependencies = false,
  IsRewritingUnitTests = false,
- IsRewritingThreads = false,
  IsLoggingAssemblyContents = false,
  IsDiffingAssemblyContents = false,
  };
@@ -167,11 +167,11 @@ internal static RewritingOptions ParseFromJSON(RewritingOptions options, string
  options.DependencySearchPaths = configuration.DependencySearchPaths;
  options.IgnoredAssembliesPattern = GetDisallowedAssembliesRegex(
  configuration.IgnoredAssemblies ?? Array.Empty<string>());
+ options.IsRewritingMemoryLocations = configuration.IsRewritingMemoryLocations;
  options.IsRewritingConcurrentCollections = configuration.IsRewritingConcurrentCollections;
  options.IsDataRaceCheckingEnabled = configuration.IsDataRaceCheckingEnabled;
  options.IsRewritingDependencies = configuration.IsRewritingDependencies;
  options.IsRewritingUnitTests = configuration.IsRewritingUnitTests;
- options.IsRewritingThreads = configuration.IsRewritingThreads;
  }
  catch (Exception ex)
  {
@@ -360,8 +360,15 @@ private class JsonConfiguration
  [DataMember(Name = "DependencySearchPaths")]
  public IList<string> DependencySearchPaths { get; set; }
 
- [DataMember(Name = "IsDataRaceCheckingEnabled")]
- public bool IsDataRaceCheckingEnabled { get; set; }
+ private bool? isRewritingMemoryLocations;
+
+ [DataMember(Name = "IsRewritingMemoryLocations")]
+ public bool IsRewritingMemoryLocations
+ {
+ // This option defaults to true.
+ get => this.isRewritingMemoryLocations ?? true;
+ set => this.isRewritingMemoryLocations = value;
+ }
 
  private bool? isRewritingConcurrentCollections;
 
@@ -373,14 +380,14 @@ public bool IsRewritingConcurrentCollections
  set => this.isRewritingConcurrentCollections = value;
  }
 
+ [DataMember(Name = "IsDataRaceCheckingEnabled")]
+ public bool IsDataRaceCheckingEnabled { get; set; }
+
  [DataMember(Name = "IsRewritingDependencies")]
  public bool IsRewritingDependencies { get; set; }
 
  [DataMember(Name = "IsRewritingUnitTests")]
  public bool IsRewritingUnitTests { get; set; }
-
- [DataMember(Name = "IsRewritingThreads")]
- public bool IsRewritingThreads { get; set; }
  }
  }
 }