From 3e0f1fa806a549c63583b5f369153c0fc8775b0d Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Thu, 19 Dec 2024 12:34:08 -0800 Subject: [PATCH] Modifying timeline --- .../Runtime/StateMachines/StateMachine.cs | 4 +- .../CheckerCore/Runtime/VectorTime.cs | 37 ++--- .../Feedback/Coverage/VectorClockTimeline.cs | 132 ++++++++++++++++++ .../SystematicTesting/TestReport.cs | 7 + .../SystematicTesting/TestingEngine.cs | 3 +- 5 files changed, 165 insertions(+), 18 deletions(-) create mode 100644 Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/VectorClockTimeline.cs diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs index 6f6019b44..961871b6e 100644 --- a/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs +++ b/Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs @@ -300,7 +300,7 @@ internal void Configure(ControlledRuntime runtime, StateMachineId id, IStateMach Id = id; Manager = manager; Inbox = inbox; - VectorTime = new VectorTime(Id); + VectorTime = new VectorTime(Id.Name); } /// @@ -543,6 +543,7 @@ public void SendEvent(PMachineValue target, Event ev) AnnounceInternal(ev); // Update vector clock VectorTime.Increment(); + VectorClockTimeline.AddToCurrentTimeline(ev.ToString(), VectorClockTimeline.EventType.SEND, VectorTime.Clock); BehavioralObserver.AddToCurrentTimeline(ev, BehavioralObserver.EventType.SEND, VectorTime); Runtime.SendEvent(target.Id, ev, this); } @@ -601,6 +602,7 @@ internal async Task RunEventHandlerAsync() { // Update state machine vector clock VectorTime.Merge(info.VectorTime); + VectorClockTimeline.AddToCurrentTimeline(e.ToString(), VectorClockTimeline.EventType.DEQUEUE, VectorTime.Clock); BehavioralObserver.AddToCurrentTimeline(e, BehavioralObserver.EventType.DEQUEUE, VectorTime); // Notify the runtime for a new event to handle. This is only used diff --git a/Src/PChecker/CheckerCore/Runtime/VectorTime.cs b/Src/PChecker/CheckerCore/Runtime/VectorTime.cs index 02359e892..0552a7f05 100644 --- a/Src/PChecker/CheckerCore/Runtime/VectorTime.cs +++ b/Src/PChecker/CheckerCore/Runtime/VectorTime.cs @@ -7,24 +7,24 @@ public class VectorTime { - // Dictionary that uses StateMachineId as the key and stores the logical clock as the value - public Dictionary Clock { get; private set; } + // Dictionary that uses String 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; + private String stateMachineId; - public VectorTime(StateMachineId stateMachineId) + public VectorTime(String stateMachineId) { this.stateMachineId = stateMachineId; - Clock = new Dictionary(); + 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); + Clock = new Dictionary(other.Clock); } // Increment the logical clock for this state machine @@ -38,7 +38,7 @@ public void Merge(VectorTime otherTime) { foreach (var entry in otherTime.Clock) { - StateMachineId otherMachineId = entry.Key; + String otherMachineId = entry.Key; int otherTimestamp = entry.Value; if (Clock.ContainsKey(otherMachineId)) @@ -55,17 +55,17 @@ public void Merge(VectorTime otherTime) } // 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, + // Return value: 1 = This vector clock happens after the other (greater), -1 = This vector clock happens before the other (less), // 0 = Clocks are equal or concurrent - public int CompareTo(VectorTime other) + public static int CompareTwo(Dictionary self, Dictionary other) { bool atLeastOneLess = false; bool atLeastOneGreater = false; - foreach (var machineId in Clock.Keys) + foreach (var machineId in self.Keys) { - int thisTime = Clock[machineId]; - int otherTime = other.Clock.ContainsKey(machineId) ? other.Clock[machineId] : 0; + int thisTime = self[machineId]; + int otherTime = other.ContainsKey(machineId) ? other[machineId] : 0; if (thisTime < otherTime) { @@ -82,22 +82,27 @@ public int CompareTo(VectorTime other) } if (atLeastOneLess && !atLeastOneGreater) { - return -1; + return 1; } if (atLeastOneGreater && !atLeastOneLess) { - return 1; + return -1; } return 0; } - + + + public int CompareTo(VectorTime other) + { + return CompareTwo(Clock, other.Clock); + } public override string ToString() { var elements = new List(); foreach (var entry in Clock) { - elements.Add($"StateMachine {entry.Key.Name}: {entry.Value}"); + elements.Add($"StateMachine {entry.Key}: {entry.Value}"); } return $"[{string.Join(", ", elements)}]"; } diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/VectorClockTimeline.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/VectorClockTimeline.cs new file mode 100644 index 000000000..f0f486aed --- /dev/null +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/VectorClockTimeline.cs @@ -0,0 +1,132 @@ +using System; +using System.Collections.Generic; +using System.IO; +using PChecker.Exceptions; +using PChecker.IO.Logging; +using PChecker.Runtime.StateMachines; + +namespace PChecker.Runtime; + +public class VectorClockTimeline +{ + private static Dictionary<(String, EventType), (HashSet> vcSet, HashSet<(String, EventType)> eSet)> CurrMap = new Dictionary<(String, EventType), (HashSet>, HashSet<(String, EventType)>)>(); + private static TextWriter Logger = new ConsoleLogger(); + private static HashSet UniqueTimelineSet = new HashSet(); + + public enum EventType + { + SEND, DEQUEUE + } + public static void AddToCurrentTimeline(String currE, EventType currType, Dictionary vectorTime) + { + if (!CurrMap.ContainsKey((currE, currType))) + { + CurrMap[(currE, currType)] = (new HashSet>(), new HashSet<(String, EventType)>()); + CurrMap[(currE, currType)].vcSet.Add(vectorTime); + } + else + { + foreach (var vc in CurrMap[(currE, currType)].vcSet) + { + int comparison = VectorTime.CompareTwo(vectorTime, vc); + if (comparison == 1) + { + CurrMap[(currE, currType)].vcSet.Remove(vc); + CurrMap[(currE, currType)].vcSet.Add(vectorTime); + break; + } + else if (comparison == -1) + { + new AssertionFailureException("An event occured after another but has less vector clock"); + } + else + { + CurrMap[(currE, currType)].vcSet.Add(vectorTime); + break; + } + } + } + + var (currVcSet, currESet) = CurrMap[(currE, currType)]; + + foreach ((String e, EventType t) in CurrMap.Keys) + { + var (vcSet, eSet) = CurrMap[(e, t)]; + + foreach (var vc in vcSet) + { + int comparison = VectorTime.CompareTwo(vectorTime, vc); + if (comparison == 1) + { + currESet.Add((e,t)); + break; + } + if (comparison == -1) + { + new AssertionFailureException("An event occured after another but has less vector clock"); + } + } + } + + + } + + public static void PrintTimeline() + { + foreach (var entry in CurrMap) + { + Logger.WriteLine($"\nEvent: {entry.Key.ToString()}"); + Logger.WriteLine(" Dependencies:"); + foreach (var dep in entry.Value.eSet) + { + Logger.WriteLine($" {dep}"); + } + } + } + + public static void RecordTimeline() + { + if (CurrMap.Keys.Count == 0) + { + return; + } + // PrintTimeline(); + int timelineHash = GenerateTimelineHash(); + UniqueTimelineSet.Add(timelineHash); + // Console.WriteLine($"Recorded timeline with hash: {timelineHash}"); + // Console.WriteLine($"Unique timelines: {string.Join(", ", UniqueTimelineSet)}"); + } + + // Step 2: Generate Hash for the Current Timeline + private static int GenerateTimelineHash() + { + unchecked // Allow overflow for hash calculation + { + int hash = 19; + + foreach (var entry in CurrMap) + { + var (vcSet, eSet) = entry.Value; + + // Hash the event name + hash = (hash * 31) + entry.Key.GetHashCode(); + + + // Hash dependencies + foreach (var e in eSet) + { + hash = (hash * 31) + e.GetHashCode(); + } + } + + return hash; + } + + } + + // Step 3: Get the Number of Unique Timelines + public static int GetUniqueTimelineCount() + { + return UniqueTimelineSet.Count; + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs index e8be37de1..fe328fb2c 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs @@ -6,6 +6,7 @@ using System.Runtime.Serialization; using System.Text; using PChecker.Coverage; +using PChecker.Runtime; using PChecker.Utilities; namespace PChecker.SystematicTesting @@ -247,6 +248,12 @@ public string GetText(CheckerConfiguration checkerConfiguration, string prefix = prefix.Equals("...") ? "....." : prefix, ExploredTimelines.Count, ExploredTimelines.Count == 1 ? string.Empty : "s"); + + report.AppendFormat( + "{0} Explored {1} vector clock timeline{2}", + prefix.Equals("...") ? "....." : prefix, + VectorClockTimeline.GetUniqueTimelineCount(), + VectorClockTimeline.GetUniqueTimelineCount() == 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 747fcbbbd..db879c07a 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -535,7 +535,8 @@ private void RegisterObservers(ControlledRuntime runtime) /// private void RunNextIteration(int schedule) { - BehavioralObserver.NextIter(); + // BehavioralObserver.NextIter(); + VectorClockTimeline.RecordTimeline(); if (!IsReplayModeEnabled && ShouldPrintIteration(schedule + 1)) { Logger.WriteLine($"..... Schedule #{schedule + 1}");