Remove conflict analysis

Src/PChecker/CheckerCore/CheckerConfiguration.cs

@@ -286,11 +286,6 @@ public int MaxSchedulingSteps
         [DataMember]
         public string JvmArgs;
 
-        /// <summary>
-        /// Enable conflict analysis for scheduling optimization.
-        /// </summary>
-        [DataMember]
-        public bool EnableConflictAnalysis;
 
         /// <summary>
         /// Initializes a new instance of the <see cref="CheckerConfiguration"/> class.
@@ -337,7 +332,6 @@ protected CheckerConfiguration()
 
             EnableColoredConsoleOutput = false;
             DisableEnvironmentExit = true;
-            EnableConflictAnalysis = false;
 
             PSymArgs = "";
             JvmArgs = "";

Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Generator/Mutator/POSScheduleMutator.cs

@@ -9,8 +9,6 @@ public POSScheduleGenerator Mutate(POSScheduleGenerator prev)
     {
         return new POSScheduleGenerator(prev.Random,
             Utils.MutateRandomChoices(prev.PriorityChoices, _meanMutationCount, _meanMutationSize, _random),
-            Utils.MutateRandomChoices(prev.SwitchPointChoices, _meanMutationCount, _meanMutationSize, _random),
-            prev.Monitor
-        );
+            Utils.MutateRandomChoices(prev.SwitchPointChoices, _meanMutationCount, _meanMutationSize, _random));
     }
 }

Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Generator/POSScheduleGenerator.cs

@@ -13,25 +13,21 @@ internal class POSScheduleGenerator: POSScheduler, IScheduleGenerator<POSSchedul
     public System.Random Random;
     public RandomChoices<int> PriorityChoices;
     public RandomChoices<double> SwitchPointChoices;
-    public ConflictOpMonitor? Monitor;
 
-    public POSScheduleGenerator(System.Random random, RandomChoices<int>? priorityChoices, RandomChoices<double>? switchPointChoices,
-        ConflictOpMonitor? monitor):
+    public POSScheduleGenerator(System.Random random, RandomChoices<int>? priorityChoices, RandomChoices<double>? switchPointChoices):
         base(new ParametricProvider(
                 priorityChoices != null ? new RandomChoices<int>(priorityChoices) : new RandomChoices<int>(random),
-                switchPointChoices != null ? new RandomChoices<double>(switchPointChoices) : new RandomChoices<double>(random)),
-            monitor)
+                switchPointChoices != null ? new RandomChoices<double>(switchPointChoices) : new RandomChoices<double>(random)))
     {
         Random = random;
         var provider = (ParametricProvider) Provider;
         PriorityChoices = provider.PriorityChoices;
         SwitchPointChoices = provider.SwitchPointChoices;
-        Monitor = monitor;
     }
 
-    public POSScheduleGenerator(CheckerConfiguration checkerConfiguration, ConflictOpMonitor? monitor):
+    public POSScheduleGenerator(CheckerConfiguration checkerConfiguration):
         this(new System.Random((int?)checkerConfiguration.RandomGeneratorSeed ?? Guid.NewGuid().GetHashCode()), null,
-            null, monitor)
+            null)
     {
     }
 
@@ -42,12 +38,12 @@ public POSScheduleGenerator Mutate()
 
     public POSScheduleGenerator New()
     {
-        return new POSScheduleGenerator(Random, null, null, Monitor);
+        return new POSScheduleGenerator(Random, null, null);
     }
 
     public POSScheduleGenerator Copy()
     {
-        return new POSScheduleGenerator(Random, PriorityChoices, SwitchPointChoices, Monitor);
+        return new POSScheduleGenerator(Random, PriorityChoices, SwitchPointChoices);
     }
 
     public AsyncOperation? NextRandomOperation(List<AsyncOperation> enabledOperations, AsyncOperation current)

Src/PChecker/CheckerCore/SystematicTesting/Strategies/Probabilistic/POSScheduler.cs

@@ -15,17 +15,14 @@ internal class POSScheduler: PrioritizedScheduler
     /// List of prioritized operations.
     /// </summary>
     private readonly List<AsyncOperation> PrioritizedOperations;
-
-    public ConflictOpMonitor? ConflictOpMonitor;
-
+
     /// <summary>
     /// Initializes a new instance of the <see cref="PCTStrategy"/> class.
     /// </summary>
-    public POSScheduler(PriorizationProvider provider, ConflictOpMonitor? monitor)
+    public POSScheduler(PriorizationProvider provider)
     {
         Provider = provider;
         PrioritizedOperations = new List<AsyncOperation>();
-        ConflictOpMonitor = monitor;
     }
 
     public bool GetNextOperation(AsyncOperation current, IEnumerable<AsyncOperation> ops, out AsyncOperation next)
@@ -123,11 +120,6 @@ private AsyncOperation GetPrioritizedOperation(List<AsyncOperation> ops, AsyncOp
     private bool FindNonRacingOperation(IEnumerable<AsyncOperation> ops, out AsyncOperation next)
     {
         var nonRacingOps = ops.Where(op => op.Type != AsyncOperationType.Send);
-        if (!nonRacingOps.Any() && ConflictOpMonitor != null)
-        {
-            nonRacingOps = ops.Where(op => !ConflictOpMonitor.IsConflictingOp(op));
-        }
-
         if (!nonRacingOps.Any())
         {
             next = null;

Src/PChecker/CheckerCore/SystematicTesting/Strategies/Probabilistic/PriorizationSchedulingBase.cs

@@ -34,21 +34,19 @@ internal class PriorizationSchedulingBase
     /// </summary>
     private readonly List<AsyncOperation> PrioritizedOperations;
 
-    public ConflictOpMonitor? ConflictOpMonitor;
     private int _nextPriorityChangePoint;
     private int _numSwitchPointsLeft;
 
     /// <summary>
     /// Initializes a new instance of the <see cref="PCTStrategy"/> class.
     /// </summary>
-    public PriorizationSchedulingBase(int maxPrioritySwitchPoints, int scheduleLength, PriorizationProvider provider, ConflictOpMonitor? monitor)
+    public PriorizationSchedulingBase(int maxPrioritySwitchPoints, int scheduleLength, PriorizationProvider provider)
     {
         Provider = provider;
         ScheduledSteps = 0;
         ScheduleLength = scheduleLength;
         MaxPrioritySwitchPoints = maxPrioritySwitchPoints;
         PrioritizedOperations = new List<AsyncOperation>();
-        ConflictOpMonitor = monitor;
         _numSwitchPointsLeft = maxPrioritySwitchPoints;
 
         double switchPointProbability = 0.1;
@@ -66,7 +64,7 @@ public virtual bool GetNextOperation(AsyncOperation current, IEnumerable<AsyncOp
         var enabledOperations = ops.Where(op => op.Status is AsyncOperationStatus.Enabled).ToList();
         if (enabledOperations.Count == 0)
         {
-            if (ConflictOpMonitor == null && _nextPriorityChangePoint == ScheduledSteps)
+            if (_nextPriorityChangePoint == ScheduledSteps)
             {
                 MovePriorityChangePointForward();
             }
@@ -78,25 +76,9 @@ public virtual bool GetNextOperation(AsyncOperation current, IEnumerable<AsyncOp
         {
             next = highestEnabledOp;
         }
-        if (ConflictOpMonitor != null)
-        {
-            ResetPriorities(next, enabledOperations);
-        }
-
         return true;
     }
 
-    public void ResetPriorities(AsyncOperation next, IEnumerable<AsyncOperation> ops)
-    {
-        foreach (var op in ops)
-        {
-            if (op != next && ConflictOpMonitor.IsRacing(next, op))
-            {
-                PrioritizedOperations.Remove(op);
-            }
-        }
-        PrioritizedOperations.Remove(next);
-    }
 
     private void MovePriorityChangePointForward()
     {
@@ -137,13 +119,8 @@ private AsyncOperation GetPrioritizedOperation(List<AsyncOperation> ops, AsyncOp
             Debug.WriteLine("<PCTLog> Detected new operation '{0}' at index '{1}'.", op.Id, mIndex);
         }
 
-        if (ConflictOpMonitor != null && FindNonRacingOperation(ops, out var next))
-        {
-            return next;
-        }
-
         var prioritizedSchedulable = GetHighestPriorityEnabledOperation(ops);
-        if (ConflictOpMonitor == null && _nextPriorityChangePoint == ScheduledSteps)
+        if (_nextPriorityChangePoint == ScheduledSteps)
         {
             if (ops.Count == 1)
             {
@@ -190,32 +167,6 @@ private AsyncOperation GetPrioritizedOperation(List<AsyncOperation> ops, AsyncOp
         return ops.First(op => op.Equals(prioritizedSchedulable));
     }
 
-    private bool FindNonRacingOperation(IEnumerable<AsyncOperation> ops, out AsyncOperation next)
-    {
-        var nonRacingOps = ops.Where(op => op.Type != AsyncOperationType.Send);
-        if (!nonRacingOps.Any())
-        {
-            var sendOps = ops.Where(op => op.Type == AsyncOperationType.Send);
-            nonRacingOps = ops.Where(op => !ConflictOpMonitor.IsConflictingOp(op));
-        }
-
-        if (!nonRacingOps.Any())
-        {
-            next = null;
-            return false;
-        }
-        else if (!nonRacingOps.Skip(1).Any())
-        {
-            next = nonRacingOps.First();
-            return true;
-        }
-        else
-        {
-            next = GetHighestPriorityEnabledOperation(nonRacingOps);
-            return true;
-        }
-
-    }
 
     public void Reset()
     {

Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs

@@ -65,11 +65,6 @@ public class TestingEngine
         /// </summary>
         internal readonly ISchedulingStrategy Strategy;
 
-        /// <summary>
-        /// Monitors conflict operations used by the POS Strategy.
-        /// </summary>
-        private ConflictOpMonitor? _conflictOpObserver;
-
         /// <summary>
         /// Random value generator used by the scheduling strategies.
         /// </summary>
@@ -303,12 +298,6 @@ private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo
             {
                 JsonVerboseLogs = new List<List<LogEntry>>();
             }
-
-            if (checkerConfiguration.EnableConflictAnalysis)
-            {
-                _conflictOpObserver = new ConflictOpMonitor();
-            }
-
             if (checkerConfiguration.SchedulingStrategy is "replay")
             {
                 var scheduleDump = GetScheduleForReplay(out var isFair);
@@ -328,8 +317,7 @@ private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo
             }
             else if (checkerConfiguration.SchedulingStrategy is "pos")
             {
-                var scheduler = new POSScheduler(new RandomPriorizationProvider(RandomValueGenerator),
-                    _conflictOpObserver);
+                var scheduler = new POSScheduler(new RandomPriorizationProvider(RandomValueGenerator));
                 Strategy = new PrioritizedSchedulingStrategy(checkerConfiguration.MaxUnfairSchedulingSteps,
                     RandomValueGenerator, scheduler);
             }
@@ -372,7 +360,7 @@ private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo
                 Strategy = new FeedbackGuidedStrategy<RandomInputGenerator, POSScheduleGenerator>(
                     _checkerConfiguration,
                     new RandomInputGenerator(checkerConfiguration),
-                    new POSScheduleGenerator(_checkerConfiguration, _conflictOpObserver));
+                    new POSScheduleGenerator(_checkerConfiguration));
             }
             else if (checkerConfiguration.SchedulingStrategy is "portfolio")
             {
@@ -568,12 +556,6 @@ private void RegisterObservers(ControlledRuntime runtime)
                 // Always output a json log of the error
                 JsonLogger = new JsonWriter();
                 runtime.SetJsonLogger(JsonLogger);
-
-                if (_conflictOpObserver != null)
-                {
-                    _conflictOpObserver.VectorClockGenerator = JsonLogger.VcGenerator;
-                    runtime.RegisterLog(_conflictOpObserver);
-                }
         }
 
         /// <summary>
@@ -716,7 +698,6 @@ private void RunNextIteration(int schedule)
 
                 runtimeLogger?.Dispose();
                 runtime?.Dispose();
-                _conflictOpObserver?.Reset();
             }
         }