diff --git a/Src/PChecker/CheckerCore/Coverage/CoverageInfo.cs b/Src/PChecker/CheckerCore/Coverage/CoverageInfo.cs index dcca7a6f0..642e88e56 100644 --- a/Src/PChecker/CheckerCore/Coverage/CoverageInfo.cs +++ b/Src/PChecker/CheckerCore/Coverage/CoverageInfo.cs @@ -54,6 +54,8 @@ public CoverageInfo() Machines = new HashSet(); MachinesToStates = new Dictionary>(); RegisteredEvents = new Dictionary>(); + EventInfo = new EventCoverage(); + CoverageGraph = new Graph(); } /// diff --git a/Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs b/Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs index 60cd4b084..c9ead6f6b 100644 --- a/Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs +++ b/Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs @@ -1,6 +1,8 @@ // Copyright (c) Microsoft Corporation. // Licensed under the MIT License. +using System; + namespace PChecker.Random { /// diff --git a/Src/PChecker/CheckerCore/Runtime/Events/EventInfo.cs b/Src/PChecker/CheckerCore/Runtime/Events/EventInfo.cs index a4de78098..993ab9dae 100644 --- a/Src/PChecker/CheckerCore/Runtime/Events/EventInfo.cs +++ b/Src/PChecker/CheckerCore/Runtime/Events/EventInfo.cs @@ -23,6 +23,8 @@ internal class EventInfo [DataMember] internal EventOriginInfo OriginInfo { get; private set; } + internal VectorTime VectorTime; + /// /// Initializes a new instance of the class. /// @@ -34,10 +36,11 @@ internal EventInfo(Event e) /// /// Initializes a new instance of the class. /// - internal EventInfo(Event e, EventOriginInfo originInfo) + internal EventInfo(Event e, EventOriginInfo originInfo, VectorTime v) : this(e) { OriginInfo = originInfo; + VectorTime = new VectorTime(v); } } } \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventQueue.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventQueue.cs index 7db5bb744..569c08243 100644 --- a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventQueue.cs +++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventQueue.cs @@ -157,7 +157,7 @@ public EnqueueStatus Enqueue(Event e, EventInfo info) // A default event handler exists. var stateName = StateMachine.CurrentState.GetType().Name; var eventOrigin = new EventOriginInfo(StateMachine.Id, StateMachine.GetType().FullName, stateName); - return (DequeueStatus.Default, DefaultEvent.Instance, new EventInfo(DefaultEvent.Instance, eventOrigin)); + return (DequeueStatus.Default, DefaultEvent.Instance, new EventInfo(DefaultEvent.Instance, eventOrigin, StateMachine.VectorTime)); } /// @@ -209,7 +209,7 @@ public void RaiseEvent(Event e) { var stateName = StateMachine.CurrentState.GetType().Name; var eventOrigin = new EventOriginInfo(StateMachine.Id, StateMachine.GetType().FullName, stateName); - var info = new EventInfo(e, eventOrigin); + var info = new EventInfo(e, eventOrigin, StateMachine.VectorTime); RaisedEvent = (e, info); StateMachineManager.OnRaiseEvent(e, info); } diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs index 0c2ae5701..6f6019b44 100644 --- a/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs +++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs @@ -54,6 +54,11 @@ public abstract class StateMachine /// private protected IEventQueue Inbox; + /// + /// Keeps track of state machine's current vector time. + /// + public VectorTime VectorTime; + /// /// Cache of state machine types to a map of action names to action declarations. /// @@ -295,6 +300,7 @@ internal void Configure(ControlledRuntime runtime, StateMachineId id, IStateMach Id = id; Manager = manager; Inbox = inbox; + VectorTime = new VectorTime(Id); } /// @@ -535,6 +541,9 @@ public void SendEvent(PMachineValue target, Event ev) Assert(target.Permissions.Contains(ev.GetType().Name), $"Event {ev.GetType().Name} is not in the permissions set of the target machine"); AnnounceInternal(ev); + // Update vector clock + VectorTime.Increment(); + BehavioralObserver.AddToCurrentTimeline(ev, BehavioralObserver.EventType.SEND, VectorTime); Runtime.SendEvent(target.Id, ev, this); } @@ -590,6 +599,10 @@ internal async Task RunEventHandlerAsync() if (status is DequeueStatus.Success) { + // Update state machine vector clock + VectorTime.Merge(info.VectorTime); + BehavioralObserver.AddToCurrentTimeline(e, BehavioralObserver.EventType.DEQUEUE, VectorTime); + // Notify the runtime for a new event to handle. This is only used // during bug-finding and operation bounding, because the runtime // has to schedule an state machine when a new operation is dequeued. diff --git a/Src/PChecker/CheckerCore/Runtime/VectorTime.cs b/Src/PChecker/CheckerCore/Runtime/VectorTime.cs new file mode 100644 index 000000000..02359e892 --- /dev/null +++ b/Src/PChecker/CheckerCore/Runtime/VectorTime.cs @@ -0,0 +1,124 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using PChecker.Runtime.StateMachines; +using PChecker.IO.Logging; + +public class VectorTime +{ + // Dictionary that uses StateMachineId as the key and stores the logical clock as the value + public Dictionary Clock { get; private set; } + + // The ID of the current state machine + + private StateMachineId stateMachineId; + + public VectorTime(StateMachineId stateMachineId) + { + this.stateMachineId = stateMachineId; + Clock = new Dictionary(); + Clock[stateMachineId] = 0; // Initialize the clock for this state machine + } + + // Clone constructor (creates a snapshot of the vector clock) + public VectorTime(VectorTime other) + { + Clock = new Dictionary(other.Clock); + } + + // Increment the logical clock for this state machine + public void Increment() + { + Clock[stateMachineId]++; + } + + // Merge another vector clock into this one + public void Merge(VectorTime otherTime) + { + foreach (var entry in otherTime.Clock) + { + StateMachineId otherMachineId = entry.Key; + int otherTimestamp = entry.Value; + + if (Clock.ContainsKey(otherMachineId)) + { + // Take the maximum timestamp for each state machine + Clock[otherMachineId] = Math.Max(Clock[otherMachineId], otherTimestamp); + } + else + { + // Add the state machine's timestamp if it doesn't exist in this time + Clock[otherMachineId] = otherTimestamp; + } + } + } + + // Compare this vector clock to another for sorting purposes + // Rturn value: -1 = This vector clock happens after the other, 1 = This vector clock happens before the other, + // 0 = Clocks are equal or concurrent + public int CompareTo(VectorTime other) + { + bool atLeastOneLess = false; + bool atLeastOneGreater = false; + + foreach (var machineId in Clock.Keys) + { + int thisTime = Clock[machineId]; + int otherTime = other.Clock.ContainsKey(machineId) ? other.Clock[machineId] : 0; + + if (thisTime < otherTime) + { + atLeastOneLess = true; + } + else if (thisTime > otherTime) + { + atLeastOneGreater = true; + } + if (atLeastOneLess && atLeastOneGreater) + { + return 0; + } + } + if (atLeastOneLess && !atLeastOneGreater) + { + return -1; + } + if (atLeastOneGreater && !atLeastOneLess) + { + return 1; + } + return 0; + } + + + public override string ToString() + { + var elements = new List(); + foreach (var entry in Clock) + { + elements.Add($"StateMachine {entry.Key.Name}: {entry.Value}"); + } + return $"[{string.Join(", ", elements)}]"; + } + + public override bool Equals(object obj) + { + if (obj is VectorTime other) + { + return Clock.OrderBy(x => x.Key).SequenceEqual(other.Clock.OrderBy(x => x.Key)); + } + return false; + } + + public override int GetHashCode() + { + int hash = 17; + foreach (var entry in Clock) + { + hash = hash * 31 + entry.Key.GetHashCode(); + hash = hash * 31 + entry.Value.GetHashCode(); + } + return hash; + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs index 9f1cd0528..1c6b81445 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs @@ -14,6 +14,7 @@ using System.Threading.Tasks; using PChecker.Coverage; using PChecker.Exceptions; +using PChecker.Feedback; using PChecker.Random; using PChecker.Runtime.Events; using PChecker.Runtime.Logging; @@ -150,7 +151,6 @@ private static ControlledRuntime CreateWithConfiguration(CheckerConfiguration ch /// public JsonWriter JsonLogger => LogWriter.JsonLogger; - /// /// Returns the current hashed state of the monitors. /// @@ -618,6 +618,8 @@ 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.ScheduleNextEnabledOperation(AsyncOperationType.Send); ResetProgramCounter(sender); @@ -647,7 +649,7 @@ private EnqueueStatus EnqueueEvent(StateMachine stateMachine, Event e, StateMach var originInfo = new EventOriginInfo(sender.Id, sender.GetType().FullName, sender.CurrentState.GetType().Name); - var eventInfo = new EventInfo(e, originInfo); + var eventInfo = new EventInfo(e, originInfo, sender.VectorTime); LogWriter.LogSendEvent(stateMachine.Id, sender.Id.Name, sender.Id.Type, sender.CurrentStateName, e, isTargetHalted: false); diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Operations/AsyncOperation.cs b/Src/PChecker/CheckerCore/SystematicTesting/Operations/AsyncOperation.cs index cac165309..bbc6803e9 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/Operations/AsyncOperation.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/Operations/AsyncOperation.cs @@ -49,6 +49,11 @@ internal abstract class AsyncOperation : IAsyncOperation /// True if the next awaiter is controlled, else false. /// internal bool IsAwaiterControlled; + + /// + /// The receiver if the operation is Send. + /// + public string MessageReceiver = ""; /// /// Initializes a new instance of the class. diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/BehavioralObserver.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/BehavioralObserver.cs new file mode 100644 index 000000000..35a3353d0 --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/BehavioralObserver.cs @@ -0,0 +1,166 @@ +using System; +using System.Collections.Generic; +using System.IO; +using PChecker.IO.Logging; +using PChecker.Runtime.Events; + +namespace PChecker.Runtime; + +public class BehavioralObserver +{ + private static HashSet<(VectorTime, Event, EventType)> CurrTimeline = new HashSet<(VectorTime, Event, EventType)>(); + private static List AllTimeline = new List(); + private static TextWriter Logger = new ConsoleLogger(); + // MinHash object with 100 hash functions, check how many of these 100 values are identical between the two sets + private static MinHash minHash = new MinHash(100); + + + public enum EventType + { + SEND, DEQUEUE + } + + public BehavioralObserver() + { + CurrTimeline = new HashSet<(VectorTime, Event, EventType)>(); + } + + public static void AddToCurrentTimeline(Event e, EventType t, VectorTime vectorTime) + { + CurrTimeline.Add((new VectorTime(vectorTime), e, t)); + } + + public static int CalculateDiff(int[] currentSignature, int[] otherSignature) + { + double similarity = minHash.ComputeSimilarity(currentSignature, otherSignature); + double differenceScore = 1 - similarity; + return (int)(differenceScore * 100); // Scale the difference score (e.g., multiply by 100) + } + + public static int GetUniqueScore(int[] currentSignature) + { + int scoreSum = 0; + foreach (var otherSignature in AllTimeline) + { + int score = CalculateDiff(currentSignature, otherSignature); + if (score == 0) + { + return 0; + } + scoreSum += score; + } + return scoreSum/AllTimeline.Count; + } + + public static void PrintTimeline(List<(VectorTime, Event, EventType)> timeline) + { + Logger.WriteLine("Global state of all machines:"); + foreach (var entry in timeline) + { + Logger.WriteLine($"Machine {entry}"); + } + } + + public static List<(VectorTime, Event, EventType)> SortByVectorClock() + { + List<(VectorTime, Event, EventType)> sortedTimeline = new List<(VectorTime, Event, EventType)>(CurrTimeline); + + // Sort by event name then vector time + sortedTimeline.Sort((x, y) => x.Item2.ToString().CompareTo(y.Item2.ToString())); + sortedTimeline.Sort((x, y) => x.Item1.CompareTo(y.Item1)); + + return sortedTimeline; + } + + public static void NextIter() + { + if (CurrTimeline.Count == 0) + { + return; + } + List<(VectorTime, Event, EventType)> SortedCurrTimeline = SortByVectorClock(); + int[] currSignature = minHash.ComputeMinHashSignature(SortedCurrTimeline); + if (AllTimeline.Count == 0) + { + AllTimeline.Add(currSignature); + return; + } + int uniqueScore = GetUniqueScore(currSignature); + Logger.WriteLine($"----**** UniquenessScore: {uniqueScore}"); + if (uniqueScore != 0) + { + AllTimeline.Add(currSignature); + } + CurrTimeline = new HashSet<(VectorTime, Event, EventType)>(); + } +} + +public class MinHash +{ + private int numHashFunctions; // Number of hash functions to use + private List> hashFunctions; // List of hash functions + + public MinHash(int numHashFunctions) + { + this.numHashFunctions = numHashFunctions; + this.hashFunctions = new List>(); + + System.Random rand = new System.Random(); + for (int i = 0; i < numHashFunctions; i++) + { + int a = rand.Next(); + int b = rand.Next(); + hashFunctions.Add(x => a * x + b); + } + } + + // Create a MinHash signature for a given set + public int[] ComputeMinHashSignature(List<(VectorTime, Event, BehavioralObserver.EventType)> set) + { + int[] signature = new int[numHashFunctions]; + + for (int i = 0; i < numHashFunctions; i++) + { + signature[i] = int.MaxValue; + } + foreach (var element in set) + { + int elementHash = ComputeElementHash(element); + + for (int i = 0; i < numHashFunctions; i++) + { + int hashedValue = hashFunctions[i](elementHash); + if (hashedValue < signature[i]) + { + signature[i] = hashedValue; + } + } + } + return signature; + } + + // Compute a composite hash for the (VectorTime, Event, EventType) tuple + private int ComputeElementHash((VectorTime, Event, BehavioralObserver.EventType) element) + { + int hash1 = element.Item1.GetHashCode(); + int hash2 = element.Item2.GetHashCode(); + int hash3 = element.Item3.GetHashCode(); + return hash1 ^ hash2 ^ hash3; + } + + // Compute Jaccard similarity based on MinHash signatures + public double ComputeSimilarity(int[] signature1, int[] signature2) + { + int identicalMinHashes = 0; + + for (int i = 0; i < numHashFunctions; i++) + { + if (signature1[i] == signature2[i]) + { + identicalMinHashes++; + } + } + return (double)identicalMinHashes / numHashFunctions; + } +} + diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/TimelineObserver.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/TimelineObserver.cs new file mode 100644 index 000000000..e58aacb20 --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/TimelineObserver.cs @@ -0,0 +1,191 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using PChecker.Runtime.Events; +using PChecker.Runtime.Logging; +using PChecker.Runtime.StateMachines; + +namespace PChecker.Feedback; + +internal class TimelineObserver: IControlledRuntimeLog +{ + + private HashSet<(string, string, string)> _timelines = new(); + private Dictionary> _allEvents = new(); + private Dictionary> _orderedEvents = new(); + private IControlledRuntimeLog _controlledRuntimeLogImplementation; + + public static readonly List<(int, int)> Coefficients = new(); + public static int NumOfCoefficients = 50; + + static TimelineObserver() + { + // Fix seed to generate same random numbers across runs. + var rand = new System.Random(0); + + for (int i = 0; i < NumOfCoefficients; i++) + { + Coefficients.Add((rand.Next(), rand.Next())); + } + } + + public int GetTimelineHash() + { + return GetAbstractTimeline().GetHashCode(); + } + + public string GetAbstractTimeline() + { + var tls = _timelines.Select(it => $"<{it.Item1}, {it.Item2}, {it.Item3}>").ToList(); + tls.Sort(); + return string.Join(";", tls); + } + + public string GetTimeline() + { + return string.Join(";", _orderedEvents.Select(it => + { + var events = string.Join(",", it.Value); + return $"{it.Key}: {events}"; + })); + } + + public List GetTimelineMinhash() + { + List minHash = new(); + var timelineHash = _timelines.Select(it => it.GetHashCode()); + foreach (var (a, b) in Coefficients) + { + int minValue = Int32.MaxValue; + foreach (var value in timelineHash) + { + int hash = a * value + b; + minValue = Math.Min(minValue, hash); + } + minHash.Add(minValue); + } + return minHash; + } + + public void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType) + { + } + + public void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName) + { + } + + public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, + Event e, bool isTargetHalted) + { + } + + public void OnRaiseEvent(StateMachineId id, string stateName, Event e) + { + } + + public void OnEnqueueEvent(StateMachineId id, Event e) + { + } + + public void OnDequeueEvent(StateMachineId id, string stateName, Event e) + { + string actor = id.Type; + + _allEvents.TryAdd(actor, new()); + _orderedEvents.TryAdd(actor, new()); + + string name = e.GetType().Name; + foreach (var ev in _allEvents[actor]) + { + _timelines.Add((actor, ev, name)); + } + _allEvents[actor].Add(name); + _orderedEvents[actor].Add(name); + } + + public void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked) + { + } + + public void OnWaitEvent(StateMachineId id, string stateName, Type eventType) + { + } + + public void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes) + { + } + + public void OnStateTransition(StateMachineId id, string stateName, bool isEntry) + { + } + + public void OnGotoState(StateMachineId id, string currentStateName, string newStateName) + { + } + + public void OnDefaultEventHandler(StateMachineId id, string stateName) + { + } + + public void OnHalt(StateMachineId id, int inboxSize) + { + } + + public void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e) + { + } + + public void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e) + { + } + + public void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex) + { + } + + public void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex) + { + } + + public void OnCreateMonitor(string monitorType) + { + } + + public void OnMonitorExecuteAction(string monitorType, string stateName, string actionName) + { + } + + public void OnMonitorProcessEvent(string monitorType, string stateName, string senderName, string senderType, + string senderStateName, Event e) + { + } + + public void OnMonitorRaiseEvent(string monitorType, string stateName, Event e) + { + } + + public void OnMonitorStateTransition(string monitorType, string stateName, bool isEntry, bool? isInHotState) + { + } + + public void OnMonitorError(string monitorType, string stateName, bool? isInHotState) + { + } + + public void OnRandom(object result, string callerName, string callerType) + { + } + + public void OnAssertionFailure(string error) + { + } + + public void OnStrategyDescription(string strategyName, string description) + { + } + + public void OnCompleted() + { + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/FeedbackGuidedStrategy.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/FeedbackGuidedStrategy.cs new file mode 100644 index 000000000..fa4ca7d04 --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/FeedbackGuidedStrategy.cs @@ -0,0 +1,271 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using PChecker.Generator; +using PChecker.Feedback; +using PChecker.Generator.Object; +using PChecker.SystematicTesting.Strategies.Probabilistic; +using AsyncOperation = PChecker.SystematicTesting.Operations.AsyncOperation; +using Debug = System.Diagnostics.Debug; + +namespace PChecker.SystematicTesting.Strategies.Feedback; + + +internal class FeedbackGuidedStrategy : IFeedbackGuidedStrategy +{ + public record StrategyGenerator(ControlledRandom InputGenerator, IScheduler Scheduler); + + public record GeneratorRecord(int Priority, StrategyGenerator Generator, List MinHash); + + internal StrategyGenerator Generator; + + private readonly int _maxScheduledSteps; + + protected int ScheduledSteps; + + private readonly HashSet _visitedTimelines = new(); + + private List _savedGenerators = new (); + private int _pendingMutations = 0; + private bool _shouldExploreNew = false; + private HashSet _visitedGenerators = new HashSet(); + private GeneratorRecord? _currentParent = null; + + private System.Random _rnd = new System.Random(); + + + + /// + /// Initializes a new instance of the class. + /// + public FeedbackGuidedStrategy(CheckerConfiguration checkerConfiguration, ControlledRandom inputGenerator, IScheduler scheduler) + { + if (scheduler is PCTScheduler) + { + _maxScheduledSteps = checkerConfiguration.MaxUnfairSchedulingSteps; + } + else + { + _maxScheduledSteps = checkerConfiguration.MaxFairSchedulingSteps; + } + Generator = new StrategyGenerator(inputGenerator, scheduler); + } + + /// + public virtual bool GetNextOperation(AsyncOperation current, IEnumerable ops, out AsyncOperation next) + { + var result = Generator.Scheduler.GetNextOperation(current, ops, out next); + ScheduledSteps++; + return result; + } + + /// + public bool GetNextBooleanChoice(AsyncOperation current, int maxValue, out bool next) + { + next = Generator.InputGenerator.Next(maxValue) == 0; + ScheduledSteps++; + return true; + } + + /// + public bool GetNextIntegerChoice(AsyncOperation current, int maxValue, out int next) + { + next = Generator.InputGenerator.Next(maxValue); + ScheduledSteps++; + return true; + } + + /// + public virtual bool PrepareForNextIteration() + { + ScheduledSteps = 0; + PrepareNextInput(); + return true; + } + + /// + public int GetScheduledSteps() + { + return ScheduledSteps; + } + + /// + public bool HasReachedMaxSchedulingSteps() + { + if (_maxScheduledSteps == 0) + { + return false; + } + + return ScheduledSteps >= _maxScheduledSteps; + } + + /// + public bool IsFair() + { + return true; + } + + /// + public string GetDescription() + { + return "feedback"; + } + + /// + public void Reset() + { + ScheduledSteps = 0; + } + + private int ComputeDiversity(int timeline, List hash) + { + if (!_visitedTimelines.Add(timeline)) + { + return 0; + } + + if (_savedGenerators.Count == 0) + { + return 20; + } + + var maxSim = int.MinValue; + foreach (var record in _savedGenerators) + { + var timelineHash = record.MinHash; + var similarity = 0; + for (int i = 0; i < hash.Count; i++) + { + if (hash[i] == timelineHash[i]) + { + similarity += 1; + } + } + + maxSim = Math.Max(maxSim, similarity); + } + + + return (hash.Count - maxSim) + 20; + } + + /// + /// This method observes the results of previous run and prepare for the next run. + /// + public virtual void ObserveRunningResults(TimelineObserver timelineObserver) + { + var timelineHash = timelineObserver.GetTimelineHash(); + var timelineMinhash = timelineObserver.GetTimelineMinhash(); + + int diversityScore = ComputeDiversity(timelineHash, timelineMinhash); + + if (diversityScore == 0) + { + return; + } + + int priority = diversityScore; + + if (priority > 0) + { + var record = new GeneratorRecord(priority, Generator, timelineMinhash); + if (_savedGenerators.Count == 0) + { + _savedGenerators.Add(record); + return; + } + + // Maybe use binary search to speed up in the future. + var index = 0; + while (index < _savedGenerators.Count && priority < _savedGenerators[index].Priority) + { + index += 1; + } + if (index >= _savedGenerators.Count) + { + _savedGenerators.Add(record); + } + else + { + _savedGenerators.Insert(index, record); + } + } + } + + public int TotalSavedInputs() + { + return _savedGenerators.Count; + } + + private void PrepareNextInput() + { + Generator.Scheduler.PrepareForNextIteration(); + if (_savedGenerators.Count == 0) + { + // Mutate current input if no input is saved. + Generator = NewGenerator(); + } + else + { + if (_currentParent == null && !_shouldExploreNew) + { + _currentParent = _savedGenerators.First(); + _visitedGenerators.Add(_currentParent); + _pendingMutations = 50; + } + + if (_pendingMutations == 0) + { + _shouldExploreNew = false; + bool found = false; + foreach (var generator in _savedGenerators) + { + if (_visitedGenerators.Contains(generator)) continue; + _currentParent = generator; + _visitedGenerators.Add(generator); + _pendingMutations = generator.Priority; + found = true; + break; + } + + if (!found) + { + if (_rnd.NextDouble() < 0.5) + { + _visitedGenerators.Clear(); + _currentParent = _savedGenerators.First(); + _visitedGenerators.Add(_currentParent); + _pendingMutations = _currentParent.Priority; + } + else + { + _shouldExploreNew = true; + _currentParent = null; + _pendingMutations = 50; + } + } + } + + Generator = _shouldExploreNew ? NewGenerator() : MutateGenerator(_currentParent.Generator); + _pendingMutations -= 1; + } + } + + + protected virtual StrategyGenerator MutateGenerator(StrategyGenerator prev) + { + return new StrategyGenerator(prev.InputGenerator.Mutate(), prev.Scheduler.Mutate()); + } + + protected virtual StrategyGenerator NewGenerator() + { + return new StrategyGenerator(Generator.InputGenerator.New(), Generator.Scheduler.New()); + } + + public void DumpStats(TextWriter writer) + { + writer.WriteLine($"..... Total saved: {TotalSavedInputs()}, pending mutations: {_pendingMutations}, visited generators: {_visitedGenerators.Count}"); + } +} diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Generator/ControlledRandom.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Generator/ControlledRandom.cs new file mode 100644 index 000000000..d271a830b --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Generator/ControlledRandom.cs @@ -0,0 +1,69 @@ +using System; +using PChecker.Generator.Mutator; +using PChecker.Random; + +namespace PChecker.Generator.Object; + +/// +/// Controlled Random. +/// +public class ControlledRandom: IRandomValueGenerator +{ + public RandomChoices IntChoices; + public RandomChoices DoubleChoices; + + /// + /// Constructor + /// + /// + /// + public ControlledRandom(RandomChoices @int, RandomChoices @double) + { + IntChoices = @int; + DoubleChoices = @double; + } + + public ControlledRandom(CheckerConfiguration checkerConfiguration) : this(new System.Random((int?)checkerConfiguration.RandomGeneratorSeed ?? Guid.NewGuid().GetHashCode())) + { + } + + public ControlledRandom(System.Random random) + { + IntChoices = new RandomChoices(random); + DoubleChoices = new RandomChoices(random); + } + + /// + public uint Seed { get; set; } + + /// + public int Next() + { + return IntChoices.Next(); + } + + /// + public int Next(int maxValue) + { + return IntChoices.Next() % maxValue; + } + + /// + public double NextDouble() + { + return DoubleChoices.Next(); + } + + public ControlledRandom New() + { + return new ControlledRandom(IntChoices.Random); + } + + public ControlledRandom Mutate() + { + return new ControlledRandom(Utils.MutateRandomChoices(IntChoices, 5, 5, IntChoices.Random), + Utils.MutateRandomChoices(DoubleChoices, 5, 5, DoubleChoices.Random) + ); + } + +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Generator/RandomChoices.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Generator/RandomChoices.cs new file mode 100644 index 000000000..ad7c65674 --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Generator/RandomChoices.cs @@ -0,0 +1,50 @@ +using System; +using System.Collections.Generic; +using System.Data.Common; +using PChecker.Exceptions; + +namespace PChecker.Generator.Object; + +public class RandomChoices +where T: IConvertible +{ + internal readonly System.Random Random; + public int Pos; + public List Data = new(); + + public RandomChoices(System.Random random) + { + Random = random; + } + + public RandomChoices(RandomChoices other) + { + Random = other.Random; + Data = new List(other.Data); + } + + public T Next() + { + if (Pos == Data.Count) + { + Data.Add(GenerateNew()); + } + return Data[Pos++]; + } + + public T GenerateNew() + { + if (typeof(T).IsAssignableFrom(typeof(int))) + { + return (T) Convert.ChangeType(Random.Next(), typeof(T)); + } + else if (typeof(T).IsAssignableFrom(typeof(double))) + { + return (T) Convert.ChangeType(Random.NextDouble(), typeof(T)); + } + else + { + throw new RuntimeException("The random choices only supports int and double type."); + } + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Generator/Utils.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Generator/Utils.cs new file mode 100644 index 000000000..8ae1e5b16 --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Generator/Utils.cs @@ -0,0 +1,38 @@ +using System; +using System.Linq; +using PChecker.Generator.Object; + +namespace PChecker.Generator.Mutator; + +public class Utils +{ + public static int SampleGeometric(double p, double random) { + var result = Math.Ceiling(Math.Log(1 - random) / Math.Log(1 - p)); + return (int)result; + } + public static RandomChoices MutateRandomChoices (RandomChoices randomChoices, int meanMutationCount, int meanMutationSize, System.Random random) + where T: IConvertible + { + meanMutationCount = Math.Max(Math.Min(randomChoices.Data.Count / 3, meanMutationCount), 1); + meanMutationSize = Math.Max(Math.Min(randomChoices.Data.Count / 3, meanMutationSize), 1); + RandomChoices newChoices = new RandomChoices(randomChoices); + int mutations = Utils.SampleGeometric(1.0f / meanMutationCount, random.NextDouble()); + + while (mutations-- > 0) + { + int offset = random.Next(newChoices.Data.Count); + int mutationSize = Utils.SampleGeometric(1.0f / meanMutationSize, random.NextDouble()); + for (int i = offset; i < offset + mutationSize; i++) + { + if (i >= newChoices.Data.Count) + { + break; + } + + newChoices.Data[i] = newChoices.GenerateNew(); + } + } + + return newChoices; + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/IFeedbackGuidedStrategy.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/IFeedbackGuidedStrategy.cs new file mode 100644 index 000000000..ad3c3c824 --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/IFeedbackGuidedStrategy.cs @@ -0,0 +1,12 @@ +using System; +using System.IO; +using PChecker.Feedback; + +namespace PChecker.SystematicTesting.Strategies.Feedback; + +internal interface IFeedbackGuidedStrategy: ISchedulingStrategy +{ + public void ObserveRunningResults(TimelineObserver timelineObserver); + public int TotalSavedInputs(); + public void DumpStats(TextWriter writer); +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/IScheduler.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/IScheduler.cs new file mode 100644 index 000000000..1d43076f4 --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/IScheduler.cs @@ -0,0 +1,14 @@ +using System.Collections.Generic; +using PChecker.Random; +using PChecker.SystematicTesting.Operations; + +namespace PChecker.SystematicTesting.Strategies.Probabilistic; + +internal interface IScheduler +{ + public bool GetNextOperation(AsyncOperation current, IEnumerable ops, out AsyncOperation next); + public void Reset(); + public bool PrepareForNextIteration(); + public IScheduler Mutate(); + public IScheduler New(); +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/PCTScheduler.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/PCTScheduler.cs new file mode 100644 index 000000000..56b15b353 --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/PCTScheduler.cs @@ -0,0 +1,236 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using System.Collections.Generic; +using System.Linq; +using PChecker.Generator.Object; +using PChecker.IO.Debugging; +using PChecker.Random; +using PChecker.SystematicTesting.Operations; + +namespace PChecker.SystematicTesting.Strategies.Probabilistic +{ + /// + /// A priority-based probabilistic scheduling strategy. + /// + /// + /// This strategy is described in the following paper: + /// https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/asplos277-pct.pdf + /// + internal class PCTScheduler : IScheduler + { + + + /// + /// Random value generator. + /// + private readonly IRandomValueGenerator _randomValueGenerator; + + /// + /// The maximum number of steps to schedule. + /// + private readonly int MaxScheduledSteps; + + /// + /// The number of scheduled steps. + /// + private int ScheduledSteps; + + /// + /// Max number of priority switch points. + /// + internal readonly int MaxPrioritySwitchPoints; + + /// + /// Approximate length of the schedule across all schedules. + /// + internal int ScheduleLength; + + /// + /// List of prioritized operations. + /// + private readonly List PrioritizedOperations; + + /// + /// Next execution point where the priority should be changed. + /// + private int _nextPriorityChangePoint; + + /// + /// Number of switch points left (leq MaxPrioritySwitchPoints). + /// + private int _numSwitchPointsLeft; + + /// + /// Initializes a new instance of the class. + /// + public PCTScheduler(int maxPrioritySwitchPoints, int scheduleLength, IRandomValueGenerator random) + { + _randomValueGenerator = random; + ScheduledSteps = 0; + ScheduleLength = scheduleLength; + MaxPrioritySwitchPoints = maxPrioritySwitchPoints; + PrioritizedOperations = new List(); + double switchPointProbability = 0.1; + if (ScheduleLength != 0) + { + switchPointProbability = 1.0 * _numSwitchPointsLeft / (ScheduleLength - ScheduledSteps + 1); + } + _nextPriorityChangePoint = Generator.Mutator.Utils.SampleGeometric(switchPointProbability, random.NextDouble()); + + } + + public virtual bool GetNextOperation(AsyncOperation current, IEnumerable ops, + out AsyncOperation next) + { + ScheduledSteps++; + next = null; + var enabledOperations = ops.Where(op => op.Status is AsyncOperationStatus.Enabled).ToList(); + if (enabledOperations.Count == 0) + { + if (_nextPriorityChangePoint == ScheduledSteps) + { + MovePriorityChangePointForward(); + } + + return false; + } + + var highestEnabledOp = GetPrioritizedOperation(enabledOperations, current); + if (next is null) + { + next = highestEnabledOp; + } + + return true; + } + + private void MovePriorityChangePointForward() + { + _nextPriorityChangePoint += 1; + Debug.WriteLine(" Moving priority change to '{0}'.", _nextPriorityChangePoint); + } + + private AsyncOperation GetHighestPriorityEnabledOperation(IEnumerable choices) + { + AsyncOperation prioritizedOp = null; + foreach (var entity in PrioritizedOperations) + { + if (choices.Any(m => m == entity)) + { + prioritizedOp = entity; + break; + } + } + + return prioritizedOp; + } + + + /// + /// Returns the prioritized operation. + /// + private AsyncOperation GetPrioritizedOperation(List ops, AsyncOperation current) + { + if (PrioritizedOperations.Count == 0) + { + PrioritizedOperations.Add(current); + } + + foreach (var op in ops.Where(op => !PrioritizedOperations.Contains(op))) + { + var mIndex = _randomValueGenerator.Next(PrioritizedOperations.Count) + 1; + PrioritizedOperations.Insert(mIndex, op); + Debug.WriteLine(" Detected new operation '{0}' at index '{1}'.", op.Id, mIndex); + } + + + var prioritizedSchedulable = GetHighestPriorityEnabledOperation(ops); + if (_nextPriorityChangePoint == ScheduledSteps) + { + if (ops.Count == 1) + { + MovePriorityChangePointForward(); + } + else + { + PrioritizedOperations.Remove(prioritizedSchedulable); + PrioritizedOperations.Add(prioritizedSchedulable); + Debug.WriteLine(" Operation '{0}' changes to lowest priority.", prioritizedSchedulable); + + _numSwitchPointsLeft -= 1; + // Update the next priority change point. + if (_numSwitchPointsLeft > 0) + { + double switchPointProbability = 0.1; + if (ScheduleLength != 0) + { + switchPointProbability = 1.0 * _numSwitchPointsLeft / (ScheduleLength - ScheduledSteps + 1); + } + + _nextPriorityChangePoint = + Generator.Mutator.Utils.SampleGeometric(switchPointProbability, + _randomValueGenerator.NextDouble()) + ScheduledSteps; + } + + } + } + + if (Debug.IsEnabled) + { + Debug.WriteLine(" Prioritized schedulable '{0}'.", prioritizedSchedulable); + Debug.Write(" Priority list: "); + for (var idx = 0; idx < PrioritizedOperations.Count; idx++) + { + if (idx < PrioritizedOperations.Count - 1) + { + Debug.Write("'{0}', ", PrioritizedOperations[idx]); + } + else + { + Debug.WriteLine("'{0}'.", PrioritizedOperations[idx]); + } + } + } + + return ops.First(op => op.Equals(prioritizedSchedulable)); + } + + public void Reset() + { + ScheduleLength = 0; + ScheduledSteps = 0; + PrioritizedOperations.Clear(); + } + + /// + public virtual bool PrepareForNextIteration() + { + ScheduleLength = Math.Max(ScheduleLength, ScheduledSteps); + ScheduledSteps = 0; + _numSwitchPointsLeft = MaxPrioritySwitchPoints; + + PrioritizedOperations.Clear(); + double switchPointProbability = 0.1; + if (ScheduleLength != 0) + { + switchPointProbability = 1.0 * _numSwitchPointsLeft / (ScheduleLength - ScheduledSteps + 1); + } + + _nextPriorityChangePoint = + Generator.Mutator.Utils.SampleGeometric(switchPointProbability, _randomValueGenerator.NextDouble()); + return true; + } + + public IScheduler Mutate() + { + return new PCTScheduler(MaxPrioritySwitchPoints, ScheduleLength, ((ControlledRandom) _randomValueGenerator).Mutate()); + } + + public IScheduler New() + { + return new PCTScheduler(MaxPrioritySwitchPoints, ScheduleLength, ((ControlledRandom) _randomValueGenerator).New()); + } + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/POSScheduler.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/POSScheduler.cs new file mode 100644 index 000000000..548c1fb87 --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/POSScheduler.cs @@ -0,0 +1,160 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using PChecker.Feedback; +using PChecker.Generator.Object; +using PChecker.IO.Debugging; +using PChecker.Random; +using PChecker.SystematicTesting.Operations; + +namespace PChecker.SystematicTesting.Strategies.Probabilistic; + +internal class POSScheduler: IScheduler +{ + private IRandomValueGenerator _randomValueGenerator; + + /// + /// List of prioritized operations. + /// + private readonly List PrioritizedOperations; + + /// + /// Initializes a new instance of the class. + /// + public POSScheduler(IRandomValueGenerator random) + { + _randomValueGenerator = random; + PrioritizedOperations = new List(); + } + + public bool GetNextOperation(AsyncOperation current, IEnumerable ops, out AsyncOperation next) + { + next = null; + var enabledOperations = ops.Where(op => op.Status is AsyncOperationStatus.Enabled).ToList(); + if (enabledOperations.Count == 0) + { + return false; + } + + var highestEnabledOp = GetPrioritizedOperation(enabledOperations, current); + next = highestEnabledOp; + if (next.Type == AsyncOperationType.Send) + { + ResetPriorities(next, enabledOperations); + } + return true; + } + + void ResetPriorities(AsyncOperation next, IEnumerable ops) + { + foreach (var op in ops) + { + if (op.Type == AsyncOperationType.Send) + { + if (op.MessageReceiver == next.MessageReceiver) + { + PrioritizedOperations.Remove(op); + } + } + } + PrioritizedOperations.Remove(next); + } + + private AsyncOperation GetHighestPriorityEnabledOperation(IEnumerable choices) + { + AsyncOperation prioritizedOp = null; + foreach (var entity in PrioritizedOperations) + { + if (choices.Any(m => m == entity)) + { + prioritizedOp = entity; + break; + } + } + + return prioritizedOp; + } + + /// + /// Returns the prioritized operation. + /// + private AsyncOperation GetPrioritizedOperation(List ops, AsyncOperation current) + { + if (PrioritizedOperations.Count == 0) + { + PrioritizedOperations.Add(current); + } + + foreach (var op in ops.Where(op => !PrioritizedOperations.Contains(op))) + { + var mIndex = _randomValueGenerator.Next(PrioritizedOperations.Count) + 1; + PrioritizedOperations.Insert(mIndex, op); + Debug.WriteLine(" Detected new operation '{0}' at index '{1}'.", op.Id, mIndex); + } + + if (FindNonRacingOperation(ops, out var next)) + { + return next; + } + + var prioritizedSchedulable = GetHighestPriorityEnabledOperation(ops); + + if (Debug.IsEnabled) + { + Debug.WriteLine(" Prioritized schedulable '{0}'.", prioritizedSchedulable); + Debug.Write(" Priority list: "); + for (var idx = 0; idx < PrioritizedOperations.Count; idx++) + { + if (idx < PrioritizedOperations.Count - 1) + { + Debug.Write("'{0}', ", PrioritizedOperations[idx]); + } + else + { + Debug.WriteLine("'{0}'.", PrioritizedOperations[idx]); + } + } + } + + return ops.First(op => op.Equals(prioritizedSchedulable)); + } + + private bool FindNonRacingOperation(IEnumerable ops, out AsyncOperation next) + { + var nonRacingOps = ops.Where(op => op.Type != AsyncOperationType.Send); + if (!nonRacingOps.Any()) + { + next = null; + return false; + } + if (!nonRacingOps.Skip(1).Any()) + { + next = nonRacingOps.First(); + return true; + } + next = GetHighestPriorityEnabledOperation(nonRacingOps); + return true; + } + + public void Reset() + { + PrioritizedOperations.Clear(); + } + + /// + public virtual bool PrepareForNextIteration() + { + PrioritizedOperations.Clear(); + return true; + } + + public IScheduler Mutate() + { + return new POSScheduler(((ControlledRandom)_randomValueGenerator).Mutate()); + } + + public IScheduler New() + { + return new POSScheduler(((ControlledRandom)_randomValueGenerator).New()); + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/RandomScheduler.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/RandomScheduler.cs new file mode 100644 index 000000000..4194e51d9 --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/RandomScheduler.cs @@ -0,0 +1,57 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using PChecker.Generator.Mutator; +using PChecker.Generator.Object; +using PChecker.Random; +using PChecker.SystematicTesting.Operations; +using PChecker.SystematicTesting.Strategies.Probabilistic; + +namespace PChecker.SystematicTesting.Strategies.Probabilistic; + +internal class RandomScheduler : IScheduler +{ + private readonly IRandomValueGenerator _randomValueGenerator; + public RandomScheduler(IRandomValueGenerator randomValueGenerator) + { + _randomValueGenerator = randomValueGenerator; + } + + public bool GetNextOperation(AsyncOperation current, IEnumerable ops, out AsyncOperation next) + { + var enabledOperations = ops.Where(op => op.Status is AsyncOperationStatus.Enabled).ToList(); + next = null; + if (enabledOperations.Count == 0) + { + return false; + } + + if (enabledOperations.Count == 1) + { + next = enabledOperations[0]; + return true; + } + var idx = _randomValueGenerator.Next(enabledOperations.Count); + next = enabledOperations[idx]; + return true; + } + + public void Reset() + { + } + + public bool PrepareForNextIteration() + { + return true; + } + + IScheduler IScheduler.Mutate() + { + return new RandomScheduler(((ControlledRandom)_randomValueGenerator).Mutate()); + } + + IScheduler IScheduler.New() + { + return new RandomScheduler(((ControlledRandom)_randomValueGenerator).New()); + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/ScheduleAndInputStrategy.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/ScheduleAndInputStrategy.cs new file mode 100644 index 000000000..1491786e1 --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/ScheduleAndInputStrategy.cs @@ -0,0 +1,114 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using System.Collections.Generic; +using System.Linq; +using PChecker.Feedback; +using PChecker.IO.Debugging; +using PChecker.Random; +using PChecker.SystematicTesting.Operations; + +namespace PChecker.SystematicTesting.Strategies.Probabilistic +{ + /// + /// A priority-based probabilistic scheduling strategy. + /// + /// + /// This strategy is described in the following paper: + /// https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/asplos277-pct.pdf + /// + internal class ScheduleAndInputStrategy: ISchedulingStrategy + { + + /// + /// Random value generator. + /// + private readonly IRandomValueGenerator RandomValueGenerator; + + /// + /// The maximum number of steps to schedule. + /// + private readonly int MaxScheduledSteps; + + private int _scheduledSteps; + + internal readonly IScheduler Scheduler; + + /// + /// Initializes a new instance of the class. + /// + public ScheduleAndInputStrategy(int maxSteps, IRandomValueGenerator random, IScheduler scheduler) + { + RandomValueGenerator = random; + MaxScheduledSteps = maxSteps; + Scheduler = scheduler; + } + + /// + public bool GetNextOperation(AsyncOperation current, IEnumerable ops, out AsyncOperation next) + { + _scheduledSteps++; + return Scheduler.GetNextOperation(current, ops, out next); + } + + /// + public bool GetNextBooleanChoice(AsyncOperation current, int maxValue, out bool next) + { + next = false; + if (RandomValueGenerator.Next(maxValue) == 0) + { + next = true; + } + + _scheduledSteps++; + + return true; + } + + /// + public bool GetNextIntegerChoice(AsyncOperation current, int maxValue, out int next) + { + next = RandomValueGenerator.Next(maxValue); + _scheduledSteps++; + return true; + } + + /// + public int GetScheduledSteps() => _scheduledSteps; + + /// + public bool HasReachedMaxSchedulingSteps() + { + if (MaxScheduledSteps == 0) + { + return false; + } + + return _scheduledSteps >= MaxScheduledSteps; + } + + /// + public bool IsFair() => false; + + /// + public string GetDescription() + { + var text = $"pct[seed '" + RandomValueGenerator.Seed + "']"; + return text; + } + + public bool PrepareForNextIteration() { + _scheduledSteps = 0; + return Scheduler.PrepareForNextIteration(); + } + + + /// + public void Reset() + { + _scheduledSteps = 0; + Scheduler.Reset(); + } + } +} diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs index 24befbed6..e8be37de1 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs @@ -100,6 +100,13 @@ public class TestReport /// [DataMember] public HashSet InternalErrors { get; internal set; } + + /// + /// Set of hashes of timelines discovered by the scheduler. + /// + [DataMember] + public HashSet ExploredTimelines = new(); + /// /// Lock for the test report. @@ -147,6 +154,7 @@ public bool Merge(TestReport testReport) lock (Lock) { CoverageInfo.Merge(testReport.CoverageInfo); + ExploredTimelines.UnionWith(testReport.ExploredTimelines); NumOfFoundBugs += testReport.NumOfFoundBugs; @@ -232,6 +240,13 @@ public string GetText(CheckerConfiguration checkerConfiguration, string prefix = prefix.Equals("...") ? "....." : prefix, totalExploredSchedules, totalExploredSchedules == 1 ? string.Empty : "s"); + + report.AppendLine(); + report.AppendFormat( + "{0} Explored {1} timeline{2}", + prefix.Equals("...") ? "....." : prefix, + ExploredTimelines.Count, + ExploredTimelines.Count == 1 ? string.Empty : "s"); if (totalExploredSchedules > 0 && NumOfFoundBugs > 0) diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index 672d54433..32a33cfce 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -3,6 +3,7 @@ using System; using System.Collections.Generic; +using System.Diagnostics; using System.IO; using System.Linq; using System.Reflection; @@ -15,6 +16,10 @@ using System.Threading.Tasks; using System.Xml; using PChecker.Coverage; +using PChecker.Feedback; +using PChecker.Generator; +using PChecker.Generator.Mutator; +using PChecker.Generator.Object; using PChecker.IO; using PChecker.IO.Debugging; using PChecker.IO.Logging; @@ -23,10 +28,12 @@ using PChecker.Runtime.Logging; using PChecker.SystematicTesting.Strategies; using PChecker.SystematicTesting.Strategies.Exhaustive; +using PChecker.SystematicTesting.Strategies.Feedback; using PChecker.SystematicTesting.Strategies.Probabilistic; using PChecker.SystematicTesting.Strategies.Special; using PChecker.SystematicTesting.Traces; using PChecker.Utilities; +using Debug = PChecker.IO.Debugging.Debug; using Task = PChecker.Tasks.Task; namespace PChecker.SystematicTesting @@ -159,12 +166,17 @@ public override void Write(Utf8JsonWriter writer, Encoding value, JsonSerializer /// private int PrintGuard; + private StreamWriter TimelineFileStream; + + /// /// Creates a new systematic testing engine. /// public static TestingEngine Create(CheckerConfiguration checkerConfiguration) => Create(checkerConfiguration, LoadAssembly(checkerConfiguration.AssemblyToBeAnalyzed)); + private Stopwatch watch; + /// /// Creates a new systematic testing engine. /// @@ -235,6 +247,7 @@ internal TestingEngine(CheckerConfiguration checkerConfiguration, Delegate test) : this(checkerConfiguration, new TestMethodInfo(test)) { } + /// /// Initializes a new instance of the class. @@ -259,13 +272,12 @@ private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo CancellationTokenSource = new CancellationTokenSource(); PrintGuard = 1; - + TimelineFileStream = new StreamWriter(checkerConfiguration.OutputDirectory + "timeline.txt"); // Initialize a new instance of JsonVerboseLogs if running in verbose mode. if (checkerConfiguration.IsVerbose) { JsonVerboseLogs = new List>(); } - if (checkerConfiguration.SchedulingStrategy is "replay") { var scheduleDump = GetScheduleForReplay(out var isFair); @@ -281,6 +293,12 @@ private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo Strategy = new PCTStrategy(checkerConfiguration.MaxUnfairSchedulingSteps, checkerConfiguration.StrategyBound, RandomValueGenerator); } + else if (checkerConfiguration.SchedulingStrategy is "pos") + { + var scheduler = new POSScheduler(RandomValueGenerator); + Strategy = new ScheduleAndInputStrategy(checkerConfiguration.MaxUnfairSchedulingSteps, + RandomValueGenerator, scheduler); + } else if (checkerConfiguration.SchedulingStrategy is "fairpct") { var prefixLength = checkerConfiguration.MaxUnfairSchedulingSteps; @@ -301,6 +319,21 @@ private TestingEngine(CheckerConfiguration checkerConfiguration, TestMethodInfo { Strategy = new DFSStrategy(checkerConfiguration.MaxUnfairSchedulingSteps); } + else if (checkerConfiguration.SchedulingStrategy is "feedback") + { + Strategy = new FeedbackGuidedStrategy(checkerConfiguration, new ControlledRandom(checkerConfiguration), + new RandomScheduler(new ControlledRandom(checkerConfiguration))); + } + else if (checkerConfiguration.SchedulingStrategy is "feedbackpct") + { + Strategy = new FeedbackGuidedStrategy(checkerConfiguration, new ControlledRandom(checkerConfiguration), + new PCTScheduler(checkerConfiguration.StrategyBound, 0, new ControlledRandom(checkerConfiguration))); + } + else if (checkerConfiguration.SchedulingStrategy is "feedbackpos") + { + Strategy = new FeedbackGuidedStrategy(checkerConfiguration, new ControlledRandom(checkerConfiguration), + new POSScheduler(new ControlledRandom(checkerConfiguration))); + } else if (checkerConfiguration.SchedulingStrategy is "portfolio") { Error.ReportAndExit("Portfolio testing strategy is only " + @@ -388,6 +421,10 @@ private System.Threading.Tasks.Task CreateTestingTask() var options = string.Empty; if (_checkerConfiguration.SchedulingStrategy is "random" || _checkerConfiguration.SchedulingStrategy is "pct" || + _checkerConfiguration.SchedulingStrategy is "pos" || + _checkerConfiguration.SchedulingStrategy is "feedbackpct" || + _checkerConfiguration.SchedulingStrategy is "feedbackpctcp" || + _checkerConfiguration.SchedulingStrategy is "feedbackpos" || _checkerConfiguration.SchedulingStrategy is "fairpct" || _checkerConfiguration.SchedulingStrategy is "probabilistic" || _checkerConfiguration.SchedulingStrategy is "rl") @@ -404,7 +441,7 @@ _checkerConfiguration.SchedulingStrategy is "probabilistic" || { // Invokes the user-specified initialization method. TestMethodInfo.InitializeAllIterations(); - + watch = Stopwatch.StartNew(); var maxIterations = IsReplayModeEnabled ? 1 : _checkerConfiguration.TestingIterations; int i = 0; while (maxIterations == 0 || i < maxIterations) @@ -471,7 +508,7 @@ _checkerConfiguration.SchedulingStrategy is "probabilistic" || var directory = _checkerConfiguration.OutputDirectory; var file = Path.GetFileNameWithoutExtension(_checkerConfiguration.AssemblyToBeAnalyzed); file += "_" + _checkerConfiguration.TestingProcessId; - var jsonVerbosePath = directory + file + "_verbose.trace.json"; + var jsonVerbosePath = directory + file + "_verbose.trace.json"; Logger.WriteLine("... Emitting verbose logs:"); Logger.WriteLine($"..... Writing {jsonVerbosePath}"); @@ -480,15 +517,25 @@ _checkerConfiguration.SchedulingStrategy is "probabilistic" || using var jsonStreamFile = File.Create(jsonVerbosePath); JsonSerializer.Serialize(jsonStreamFile, JsonVerboseLogs, jsonSerializerConfig); } - }, CancellationTokenSource.Token); } + /// + /// Register required observers. + /// + private void RegisterObservers(ControlledRuntime runtime) + { + // Always output a json log of the error + JsonLogger = new JsonWriter(); + runtime.SetJsonLogger(JsonLogger); + } + /// /// Runs the next testing schedule. /// private void RunNextIteration(int schedule) { + BehavioralObserver.NextIter(); if (!IsReplayModeEnabled && ShouldPrintIteration(schedule + 1)) { Logger.WriteLine($"..... Schedule #{schedule + 1}"); @@ -503,6 +550,8 @@ private void RunNextIteration(int schedule) // Runtime used to serialize and test the program in this schedule. ControlledRuntime runtime = null; + TimelineObserver timelineObserver = new TimelineObserver(); + // Logger used to intercept the program output if no custom logger // is installed and if verbosity is turned off. InMemoryLogger runtimeLogger = null; @@ -516,9 +565,9 @@ private void RunNextIteration(int schedule) // Creates a new instance of the controlled runtime. runtime = new ControlledRuntime(_checkerConfiguration, Strategy); - // Always output a json log of the error - JsonLogger = new JsonWriter(); - runtime.SetJsonLogger(JsonLogger); + runtime.RegisterLog(timelineObserver); + RegisterObservers(runtime); + // If verbosity is turned off, then intercept the program log, and also redirect // the standard output and error streams to a nul logger. @@ -547,6 +596,11 @@ private void RunNextIteration(int schedule) callback(schedule); } + if (Strategy is IFeedbackGuidedStrategy strategy) + { + strategy.ObserveRunningResults(timelineObserver); + } + // Checks that no monitor is in a hot state at termination. Only // checked if no safety property violations have been found. if (!runtime.Scheduler.BugFound) @@ -567,7 +621,7 @@ private void RunNextIteration(int schedule) runtime.LogWriter.LogCompletion(); - GatherTestingStatistics(runtime); + GatherTestingStatistics(runtime, timelineObserver); if (!IsReplayModeEnabled && TestReport.NumOfFoundBugs > 0) { @@ -578,6 +632,10 @@ private void RunNextIteration(int schedule) } ConstructReproducableTrace(runtime); + if (_checkerConfiguration.OutputDirectory != null) + { + TryEmitTraces(_checkerConfiguration.OutputDirectory, "trace_0"); + } } } finally @@ -589,6 +647,18 @@ private void RunNextIteration(int schedule) Console.SetError(stdErr); } + + if (ShouldPrintIteration(schedule)) + { + var seconds = watch.Elapsed.TotalSeconds; + Logger.WriteLine($"Elapsed: {seconds}, " + + $"# timelines: {TestReport.ExploredTimelines.Count}"); + if (Strategy is IFeedbackGuidedStrategy s) + { + s.DumpStats(Logger); + } + } + if (!IsReplayModeEnabled && _checkerConfiguration.PerformFullExploration && runtime.Scheduler.BugFound) { Logger.WriteLine($"..... Schedule #{schedule + 1} " + @@ -596,7 +666,8 @@ private void RunNextIteration(int schedule) $"[task-{_checkerConfiguration.TestingProcessId}]"); } - // Cleans up the runtime before the next schedule starts. + // Cleans up the runtime before the next iteration starts. + runtimeLogger?.Dispose(); runtime?.Dispose(); } @@ -631,8 +702,10 @@ public string GetReport() /// /// Returns an object where the value null is replaced with "null" /// - public object RecursivelyReplaceNullWithString(object obj) { - if (obj == null) { + public object RecursivelyReplaceNullWithString(object obj) + { + if (obj == null) + { return "null"; } if (obj is Dictionary dictionaryStr) { @@ -653,16 +726,20 @@ public object RecursivelyReplaceNullWithString(object obj) { } return newDictionary; } - else if (obj is List list) { + else if (obj is List list) + { var newList = new List(); - foreach (var item in list) { + foreach (var item in list) + { var newItem = RecursivelyReplaceNullWithString(item); if (newItem != null) newList.Add(newItem); } + return newList; } - else { + else + { return obj; } } @@ -717,8 +794,10 @@ public void TryEmitTraces(string directory, string file) Logger.WriteLine($"..... Writing {jsonPath}"); // Remove the null objects from payload recursively for each log event - for(int i=0; i /// Gathers the exploration strategy statistics from the specified runtimne. /// - private void GatherTestingStatistics(ControlledRuntime runtime) + private void GatherTestingStatistics(ControlledRuntime runtime, TimelineObserver timelineObserver) { var report = runtime.Scheduler.GetReport(); if (_checkerConfiguration.ReportActivityCoverage) { report.CoverageInfo.CoverageGraph = Graph; } - + var coverageInfo = runtime.GetCoverageInfo(); report.CoverageInfo.Merge(coverageInfo); TestReport.Merge(report); - + var timelineHash = timelineObserver.GetTimelineHash(); + TestReport.ExploredTimelines.Add(timelineObserver.GetTimelineHash()); + // Also save the graph snapshot of the last iteration, if there is one. + Graph = coverageInfo.CoverageGraph; // Also save the graph snapshot of the last schedule, if there is one. Graph = coverageInfo.CoverageGraph; } @@ -901,15 +983,13 @@ private void ConstructReproducableTrace(ControlledRuntime runtime) if (_checkerConfiguration.IsLivenessCheckingEnabled) { stringBuilder.Append("--liveness-temperature-threshold:" + - _checkerConfiguration.LivenessTemperatureThreshold). - Append(Environment.NewLine); + _checkerConfiguration.LivenessTemperatureThreshold).Append(Environment.NewLine); } if (!string.IsNullOrEmpty(_checkerConfiguration.TestCaseName)) { stringBuilder.Append("--test-method:" + - _checkerConfiguration.TestCaseName). - Append(Environment.NewLine); + _checkerConfiguration.TestCaseName).Append(Environment.NewLine); } for (var idx = 0; idx < runtime.Scheduler.ScheduleTrace.Count; idx++) @@ -945,7 +1025,9 @@ private string[] GetScheduleForReplay(out bool isFair) string[] scheduleDump; if (_checkerConfiguration.ScheduleTrace.Length > 0) { - scheduleDump = _checkerConfiguration.ScheduleTrace.Split(new string[] { Environment.NewLine }, StringSplitOptions.None); + scheduleDump = + _checkerConfiguration.ScheduleTrace.Split(new string[] { Environment.NewLine }, + StringSplitOptions.None); } else { @@ -1013,4 +1095,4 @@ public void SetLogger(TextWriter logger) ErrorReporter.Logger = logger; } } -} \ No newline at end of file +} diff --git a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs index 8d5ae2200..d9679b59d 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs @@ -180,7 +180,7 @@ private static Scope BuildGlobalScope(ICompilerConfiguration config, PParser.Pro { DeclarationVisitor.PopulateDeclarations(config.Handler, globalScope, programUnit, nodesToDeclarations); } - + return globalScope; } diff --git a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs index 764282661..f29e8eb27 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs @@ -347,7 +347,7 @@ public override object VisitSpecMachineDecl(PParser.SpecMachineDeclContext conte return specMachine; } - + public override object VisitMachineBody(PParser.MachineBodyContext context) { foreach (var machineEntryContext in context.machineEntry()) diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs index 01d2716f2..ff6d1e2d0 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs @@ -50,7 +50,6 @@ public override IPExpr VisitNamedTupleAccessExpr(PParser.NamedTupleAccessExprCon { throw handler.TypeMismatch(subExpr, TypeKind.NamedTuple); } - var fieldName = context.field.GetText(); if (!tuple.LookupEntry(fieldName, out var entry)) { diff --git a/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs b/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs index 2175c5b28..f93a61c0f 100644 --- a/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs +++ b/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs @@ -54,9 +54,16 @@ internal PCheckerOptions() var schedulingGroup = Parser.GetOrCreateGroup("scheduling", "Search prioritization options"); schedulingGroup.AddArgument("sch-random", null, "Choose the random scheduling strategy (this is the default)", typeof(bool)); + schedulingGroup.AddArgument("sch-feedback", null, "Choose the random scheduling strategy with feedback mutation", typeof(bool)); + + schedulingGroup.AddArgument("sch-feedbackpct", null, "Choose the PCT scheduling strategy with feedback mutation", typeof(uint)); + schedulingGroup.AddArgument("sch-feedbackpos", null, + "Choose the POS scheduling strategy with feedback mutation", typeof(bool)); + schedulingGroup.AddArgument("sch-probabilistic", "sp", "Choose the probabilistic scheduling strategy with given probability for each scheduling decision where the probability is " + "specified as the integer N in the equation 0.5 to the power of N. So for N=1, the probability is 0.5, for N=2 the probability is 0.25, N=3 you get 0.125, etc.", typeof(uint)); schedulingGroup.AddArgument("sch-pct", null, "Choose the PCT scheduling strategy with given maximum number of priority switch points", typeof(uint)); + schedulingGroup.AddArgument("sch-pos", null, "Choose the POS scheduling strategy", typeof(bool)); schedulingGroup.AddArgument("sch-fairpct", null, "Choose the fair PCT scheduling strategy with given maximum number of priority switch points", typeof(uint)); schedulingGroup.AddArgument("sch-rl", null, "Choose the reinforcement learning (RL) scheduling strategy", typeof(bool)).IsHidden = true; var schCoverage = schedulingGroup.AddArgument("sch-coverage", null, "Choose the scheduling strategy for coverage mode (options: learn, random, dfs, stateless). (default: learn)"); @@ -74,7 +81,6 @@ internal PCheckerOptions() advancedGroup.AddArgument("xml-trace", null, "Specify a filename for XML runtime log output to be written to", typeof(bool)); advancedGroup.AddArgument("psym-args", null, "Specify a concatenated list of additional PSym-specific arguments to pass, each starting with a colon").IsHidden = true; advancedGroup.AddArgument("jvm-args", null, "Specify a concatenated list of PSym-specific JVM arguments to pass, each starting with a colon").IsHidden = true; - } /// @@ -226,11 +232,15 @@ private static void UpdateConfigurationWithParsedArgument(CheckerConfiguration c checkerConfiguration.RandomGeneratorSeed = (uint)option.Value; break; case "sch-random": + case "sch-pos": + case "sch-feedbackpos": + case "sch-feedback": checkerConfiguration.SchedulingStrategy = option.LongName.Substring(4); break; case "sch-probabilistic": case "sch-pct": case "sch-fairpct": + case "sch-feedbackpct": checkerConfiguration.SchedulingStrategy = option.LongName.Substring(4); checkerConfiguration.StrategyBound = (int)(uint)option.Value; break; @@ -336,15 +346,18 @@ private static void SanitizeConfiguration(CheckerConfiguration checkerConfigurat if (checkerConfiguration.SchedulingStrategy != "portfolio" && checkerConfiguration.SchedulingStrategy != "random" && + checkerConfiguration.SchedulingStrategy != "feedback" && + checkerConfiguration.SchedulingStrategy != "feedbackpct" && + checkerConfiguration.SchedulingStrategy != "feedbackpos" && checkerConfiguration.SchedulingStrategy != "pct" && + checkerConfiguration.SchedulingStrategy != "pos" && checkerConfiguration.SchedulingStrategy != "fairpct" && checkerConfiguration.SchedulingStrategy != "probabilistic" && checkerConfiguration.SchedulingStrategy != "rl" && checkerConfiguration.SchedulingStrategy != "replay" && checkerConfiguration.SchedulingStrategy != "learn" && checkerConfiguration.SchedulingStrategy != "dfs" && - checkerConfiguration.SchedulingStrategy != "stateless") - { + checkerConfiguration.SchedulingStrategy != "stateless") { Error.CheckerReportAndExit("Please provide a scheduling strategy (see --sch* options)"); } @@ -377,7 +390,6 @@ private static void FindLocalPCompiledFile(CheckerConfiguration checkerConfigura enumerationOptions.RecurseSubdirectories = true; enumerationOptions.MaxRecursionDepth = 3; - var files = from file in Directory.GetFiles(checkerConfiguration.PCompiledPath, filePattern, enumerationOptions) let info = new FileInfo(file)