From 2eda0405e49b61168d6f131d8736cae7a07f2c4d Mon Sep 17 00:00:00 2001 From: ChristineZh0u <48167738+ChristineZh0u@users.noreply.github.com> Date: Thu, 17 Oct 2024 22:00:46 -0700 Subject: [PATCH] Added VectorTime and BehavioralObserver class for feedback strategy (#799) Co-authored-by: Christine Zhou --- .../CheckerCore/Runtime/Events/EventInfo.cs | 5 +- .../StateMachines/EventQueues/EventQueue.cs | 4 +- .../Runtime/StateMachines/StateMachine.cs | 13 ++ .../CheckerCore/Runtime/VectorTime.cs | 124 +++++++++++++ .../SystematicTesting/ControlledRuntime.cs | 2 +- .../Feedback/Coverage/BehavioralObserver.cs | 166 ++++++++++++++++++ .../SystematicTesting/TestingEngine.cs | 1 + 7 files changed, 311 insertions(+), 4 deletions(-) create mode 100644 Src/PChecker/CheckerCore/Runtime/VectorTime.cs create mode 100644 Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/BehavioralObserver.cs 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 23327d0a8..1c6b81445 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs @@ -649,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/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/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index d0bfe9974..da7952ce7 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -542,6 +542,7 @@ private void RegisterObservers(ControlledRuntime runtime) /// private void RunNextIteration(int schedule) { + BehavioralObserver.NextIter(); if (!IsReplayModeEnabled && ShouldPrintIteration(schedule + 1)) { Logger.WriteLine($"..... Schedule #{schedule + 1}");