Implement SURW algorithm

Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs

@@ -53,6 +53,11 @@ public abstract class StateMachine
         /// Events are dequeued to be processed.
         /// </summary>
         private protected IEventQueue Inbox;
+
+        /// <summary>
+        /// The creator of this state machine. null if the `main` state machine.
+        /// </summary>
+        public StateMachine Creator;
 
         /// <summary>
         /// Keeps track of state machine's current vector time.
@@ -294,13 +299,14 @@ protected StateMachine()
         /// <summary>
         /// Configures the state machine.
         /// </summary>
-        internal void Configure(ControlledRuntime runtime, StateMachineId id, IStateMachineManager manager, IEventQueue inbox)
+        internal void Configure(ControlledRuntime runtime, StateMachineId id, IStateMachineManager manager, IEventQueue inbox, StateMachine creator)
         {
             Runtime = runtime;
             Id = id;
             Manager = manager;
             Inbox = inbox;
             VectorTime = new VectorTime(Id);
+            Creator = creator;
         }
 
         /// <summary>

Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs

@@ -505,7 +505,7 @@ private StateMachine CreateStateMachine(StateMachineId id, Type type, string nam
             IStateMachineManager stateMachineManager = new StateMachineManager(this, stateMachine);
 
             IEventQueue eventQueue = new EventQueue(stateMachineManager, stateMachine);
-            stateMachine.Configure(this, id, stateMachineManager, eventQueue);
+            stateMachine.Configure(this, id, stateMachineManager, eventQueue, creator);
             stateMachine.SetupEventHandlers();
             stateMachine.self = new PMachineValue(id, stateMachine.receives.ToList());
             stateMachine.interfaceName = "I_" + name;
@@ -616,7 +616,7 @@ private EnqueueStatus EnqueueEvent(StateMachineId targetId, Event e, StateMachin
                 "Cannot send event '{0}' to state machine id '{1}' that is not bound to an state machine instance.",
                 e.GetType().FullName, targetId.Value);
 
-            Scheduler.ScheduledOperation.MessageReceiver = targetId.ToString();
+            Scheduler.ScheduledOperation.MessageReceiver = targetId.Value;
 
             Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Send);
             ResetProgramCounter(sender);

Src/PChecker/CheckerCore/SystematicTesting/Operations/AsyncOperation.cs

@@ -53,7 +53,7 @@ internal abstract class AsyncOperation : IAsyncOperation
         /// <summary>
         /// The receiver if the operation is Send.
         /// </summary>
-        public string MessageReceiver = "";
+        public ulong MessageReceiver = 0;
 
         /// <summary>
         /// Initializes a new instance of the <see cref="AsyncOperation"/> class.

Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/SURWScheduler.cs

@@ -0,0 +1,296 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Reflection.PortableExecutable;
+using PChecker.Generator.Object;
+using PChecker.Random;
+using PChecker.Runtime.StateMachines;
+using PChecker.SystematicTesting.Operations;
+using PChecker.SystematicTesting.Strategies.Probabilistic;
+
+namespace PChecker.SystematicTesting.Strategies.Feedback;
+
+internal class SURWScheduler : IScheduler
+{
+    const ulong NoMachine = ulong.MaxValue;
+    private readonly IRandomValueGenerator _randomValueGenerator;
+
+    /// <summary>
+    /// A mapping between machine ID and number of interesting events of that machine.
+    /// </summary>
+    private Dictionary<ulong, int> _executionLength;
+
+    /// <summary>
+    /// A mapping between machine ID and the number of interesting events left to execute on that machine.
+    /// </summary>
+    private Dictionary<ulong, int> _weights;
+
+    /// <summary>
+    /// A set of blocked machines.
+    /// </summary>
+    private HashSet<ulong> _blocked = new();
+
+    /// <summary>
+    /// The machine scheduled to execute next.
+    /// </summary>
+    private ulong _nextIntendedMachine = NoMachine;
+
+    /// <summary>
+    /// Machines that are created during the execution of the program.
+    /// </summary>
+    private HashSet<ulong> _createdMachines = new();
+
+    /// <summary>
+    /// A mapping between machine ID and the set of child machines that are created by that machine.
+    /// </summary>
+    private Dictionary<ulong, HashSet<ulong>> _childMachines;
+
+    /// <summary>
+    /// A set of machines from which events are uniformly sampled.
+    /// </summary>
+    private HashSet<ulong> _interestingMachines;
+
+    // These fields are only used for the first trial to construct interesting operations map.
+
+    private Dictionary<ulong, HashSet<ulong>> _interestingMachineMap = new();
+    private Dictionary<ulong, int> _machineExecutionLengthCache = new();
+
+    public SURWScheduler(Dictionary<ulong, int> executionLength, HashSet<ulong> interestingMachines,
+        Dictionary<ulong, HashSet<ulong>> childMachines,
+        IRandomValueGenerator random)
+    {
+        _executionLength = executionLength;
+        _weights = _executionLength.ToDictionary(kvp => kvp.Key, kvp => kvp.Value);
+        _randomValueGenerator = random;
+        _interestingMachines = interestingMachines;
+        _childMachines = childMachines;
+    }
+
+    private void CheckNewMachines(IEnumerable<AsyncOperation> ops)
+    {
+        foreach (var op in ops.Where(op => !_createdMachines.Contains(op.Id)))
+        {
+            _createdMachines.Add(op.Id);
+            if (op is StateMachineOperation stateMachineOperation)
+            {
+                var parentMachine = stateMachineOperation.StateMachine.Creator;
+                if (parentMachine == null) continue;
+                _childMachines.TryAdd(parentMachine.Id.Value, new HashSet<ulong>());
+                _childMachines[parentMachine.Id.Value].Add(stateMachineOperation.Id);
+                var childWeight = _weights.GetValueOrDefault(op.Id, 0);
+                var parentWeight = _weights.GetValueOrDefault(parentMachine.Id.Value, 0);
+                if (_nextIntendedMachine == parentMachine.Id.Value)
+                {
+                    var randomWeight = _randomValueGenerator.Next(Math.Max(parentWeight, 1)) + 1;
+                    if (childWeight > randomWeight)
+                    {
+                        _nextIntendedMachine = op.Id;
+                    }
+                }
+
+                _weights[parentMachine.Id.Value] = Math.Max(parentWeight - childWeight, 0);
+            }
+        }
+    }
+
+    private void UpdateNextIntendedMachine(List<AsyncOperation> machines)
+    {
+        var totalWeight = machines.Sum(op => _weights.GetValueOrDefault(op.Id, 0));
+        var selectedMachineWeight = _randomValueGenerator.Next(totalWeight) + 1;
+        var currentWeight = 0;
+        foreach (var op in machines)
+        {
+            var machineWeight = _weights.GetValueOrDefault(op.Id, 0);
+            currentWeight += machineWeight;
+            if (currentWeight >= selectedMachineWeight && (machineWeight != 0))
+            {
+                _nextIntendedMachine = op.Id;
+                break;
+            }
+        }
+    }
+
+    private void ConstructInterestingOperation(AsyncOperation op)
+    {
+        if (op.Type == AsyncOperationType.Send)
+        {
+            _interestingMachineMap.TryAdd(op.MessageReceiver, new HashSet<ulong>());
+            _interestingMachineMap[op.MessageReceiver].Add(op.Id);
+        }
+    }
+
+    public bool GetNextOperation(AsyncOperation current, IEnumerable<AsyncOperation> ops, out AsyncOperation next)
+    {
+        next = null;
+        var enabledOperations = ops.Where(op => op.Status is AsyncOperationStatus.Enabled).ToList();
+        if (enabledOperations.Count == 0)
+        {
+            return false;
+        }
+
+        CheckNewMachines(enabledOperations);
+        var filteredMachines = enabledOperations.Where(op => !_blocked.Contains(op.Id)).ToList();
+        if (filteredMachines.Count == 0)
+        {
+            _nextIntendedMachine = NoMachine;
+            _blocked.Clear();
+            return GetNextOperation(current, enabledOperations, out next);
+        }
+
+        var nextMachineIndex = _randomValueGenerator.Next(filteredMachines.Count);
+        var nextMachine = filteredMachines[nextMachineIndex];
+
+        if (nextMachine.Type == AsyncOperationType.Send && _interestingMachines.Contains(nextMachine.MessageReceiver))
+        {
+            if (_weights.GetValueOrDefault(nextMachine.Id, 0) == 0)
+            {
+                _weights[nextMachine.Id] = 1;
+            }
+
+            if (_nextIntendedMachine == NoMachine)
+            {
+                UpdateNextIntendedMachine(filteredMachines);
+            }
+
+            if (nextMachine.Id == _nextIntendedMachine)
+            {
+                _weights[nextMachine.Id] -= 1;
+                _blocked.Clear();
+                _nextIntendedMachine = NoMachine;
+            }
+            else
+            {
+                _blocked.Add(nextMachine.Id);
+                return GetNextOperation(current, enabledOperations, out next);
+            }
+
+            if (_executionLength.Count == 0)
+            {
+                _machineExecutionLengthCache[nextMachine.Id] =
+                    _machineExecutionLengthCache.GetValueOrDefault(nextMachine.Id, 0) + 1;
+            }
+        }
+
+        // Unlike the original work, we need to construct the interesting machine map dynamically.
+        if (_interestingMachines.Count == 0)
+        {
+            ConstructInterestingOperation(nextMachine);
+        }
+
+        next = nextMachine;
+        return true;
+    }
+
+    private Dictionary<ulong, int> BuildMachineWeights()
+    {
+        var machineWeights = new Dictionary<ulong, int>();
+        if (_machineExecutionLengthCache.Count != 0)
+        {
+            foreach (var machine in _createdMachines)
+            {
+                if (machineWeights.ContainsKey(machine)) continue;
+                BuildMachineWeightsRecursive(machine, machineWeights);
+            }
+        }
+
+        return machineWeights;
+    }
+
+    private int BuildMachineWeightsRecursive(ulong machine, Dictionary<ulong, int> machineWeights)
+    {
+        if (!machineWeights.ContainsKey(machine))
+        {
+            var weight = _machineExecutionLengthCache.GetValueOrDefault(machine, 0) +
+                         _childMachines.GetValueOrDefault(machine, new HashSet<ulong>()).Sum(childMachine =>
+                             BuildMachineWeightsRecursive(childMachine, machineWeights));
+            machineWeights.Add(machine, weight);
+        }
+
+        return machineWeights[machine];
+    }
+
+    private HashSet<ulong> BuildInterestingMachines()
+    {
+        var keys = _interestingMachineMap.Where(machine => machine.Value.Count > 2).Select(machine => machine.Key)
+            .ToList();
+        var interestingMachines = keys.OrderBy(k => _randomValueGenerator.Next()).ToList();
+        var count = Math.Max((int)(interestingMachines.Count * 0.1), 1);
+        return interestingMachines.Take(count).ToHashSet();
+    }
+
+    public void Reset()
+    {
+        _executionLength.Clear();
+        _interestingMachines.Clear();
+    }
+
+    public bool PrepareForNextIteration()
+    {
+        var newExecutionLength = _executionLength;
+        if (newExecutionLength.Count == 0)
+        {
+            newExecutionLength = BuildMachineWeights();
+        }
+
+        var newInterestingMachines = _interestingMachines;
+        if (newInterestingMachines.Count == 0)
+        {
+            newInterestingMachines = BuildInterestingMachines();
+        }
+
+        _executionLength = newExecutionLength;
+        _interestingMachines = newInterestingMachines;
+
+        _weights = _executionLength.ToDictionary(kvp => kvp.Key, kvp => kvp.Value);
+        _blocked.Clear();
+        _nextIntendedMachine = NoMachine;
+        _createdMachines.Clear();
+        _interestingMachineMap.Clear();
+        _machineExecutionLengthCache.Clear();
+        return true;
+    }
+
+    public IScheduler Mutate()
+    {
+        var newExecutionLength = _executionLength;
+        if (newExecutionLength.Count == 0)
+        {
+            newExecutionLength = BuildMachineWeights();
+        }
+
+        var newInterestingMachines = _interestingMachines;
+        if (newInterestingMachines.Count == 0)
+        {
+            newInterestingMachines = BuildInterestingMachines();
+        }
+
+        return new SURWScheduler(
+            newExecutionLength,
+            newInterestingMachines,
+            _childMachines,
+            ((ControlledRandom)_randomValueGenerator).Mutate()
+        );
+    }
+
+    public IScheduler New()
+    {
+        var newExecutionLength = _executionLength;
+        if (newExecutionLength.Count == 0)
+        {
+            newExecutionLength = BuildMachineWeights();
+        }
+
+        var newInterestingMachines = _interestingMachines;
+        if (newInterestingMachines.Count == 0)
+        {
+            newInterestingMachines = BuildInterestingMachines();
+        }
+
+        return new SURWScheduler(
+            newExecutionLength,
+            newInterestingMachines,
+            _childMachines,
+            ((ControlledRandom)_randomValueGenerator).Mutate()
+        );
+    }
+}

Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs

@@ -294,6 +294,12 @@ private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo
                 Strategy = new ScheduleAndInputStrategy(checkerConfiguration.MaxUnfairSchedulingSteps,
                     RandomValueGenerator, scheduler);
             }
+            else if (checkerConfiguration.SchedulingStrategy is "surw")
+            {
+                var scheduler = new SURWScheduler(new(), new(), new(), RandomValueGenerator);
+                Strategy = new ScheduleAndInputStrategy(checkerConfiguration.MaxFairSchedulingSteps,
+                    RandomValueGenerator, scheduler);
+            }
             else if (checkerConfiguration.SchedulingStrategy is "fairpct")
             {
                 var prefixLength = checkerConfiguration.MaxUnfairSchedulingSteps;
@@ -329,6 +335,11 @@ private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo
                 Strategy = new FeedbackGuidedStrategy(checkerConfiguration, new ControlledRandom(checkerConfiguration),
                     new POSScheduler(new ControlledRandom(checkerConfiguration)));
             }
+            else if (checkerConfiguration.SchedulingStrategy is "feedbacksurw")
+            {
+                Strategy = new FeedbackGuidedStrategy(checkerConfiguration, new ControlledRandom(checkerConfiguration),
+                    new SURWScheduler(new(), new(), new(), new ControlledRandom(checkerConfiguration)));
+            }
             else if (checkerConfiguration.SchedulingStrategy is "portfolio")
             {
                 Error.ReportAndExit("Portfolio testing strategy is only " +
@@ -417,9 +428,11 @@ private System.Threading.Tasks.Task CreateTestingTask()
             if (_checkerConfiguration.SchedulingStrategy is "random" ||
                 _checkerConfiguration.SchedulingStrategy is "pct" ||
                 _checkerConfiguration.SchedulingStrategy is "pos" ||
+                _checkerConfiguration.SchedulingStrategy is "surw" ||
                 _checkerConfiguration.SchedulingStrategy is "feedbackpct" ||
                 _checkerConfiguration.SchedulingStrategy is "feedbackpctcp" ||
                 _checkerConfiguration.SchedulingStrategy is "feedbackpos" ||
+                _checkerConfiguration.SchedulingStrategy is "feedbacksurw" ||
                 _checkerConfiguration.SchedulingStrategy is "fairpct" ||
                 _checkerConfiguration.SchedulingStrategy is "probabilistic" ||
                 _checkerConfiguration.SchedulingStrategy is "rl")