Skip to content

Commit

Permalink
Modifying timeline
Browse files Browse the repository at this point in the history
  • Loading branch information
Christine Zhou committed Dec 19, 2024
1 parent 545dec4 commit 3e0f1fa
Show file tree
Hide file tree
Showing 5 changed files with 165 additions and 18 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}

/// <summary>
Expand Down Expand Up @@ -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);
}
Expand Down Expand Up @@ -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
Expand Down
37 changes: 21 additions & 16 deletions Src/PChecker/CheckerCore/Runtime/VectorTime.cs
Original file line number Diff line number Diff line change
Expand Up @@ -7,24 +7,24 @@

public class VectorTime
{
// Dictionary that uses StateMachineId as the key and stores the logical clock as the value
public Dictionary<StateMachineId, int> Clock { get; private set; }
// Dictionary that uses String as the key and stores the logical clock as the value
public Dictionary<String, int> 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<StateMachineId, int>();
Clock = new Dictionary<String, int>();
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<StateMachineId, int>(other.Clock);
Clock = new Dictionary<String, int>(other.Clock);
}

// Increment the logical clock for this state machine
Expand All @@ -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))
Expand All @@ -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<String, int> self, Dictionary<String, int> 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)
{
Expand All @@ -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<string>();
foreach (var entry in Clock)
{
elements.Add($"StateMachine {entry.Key.Name}: {entry.Value}");
elements.Add($"StateMachine {entry.Key}: {entry.Value}");
}
return $"[{string.Join(", ", elements)}]";
}
Expand Down
Original file line number Diff line number Diff line change
@@ -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<Dictionary<String, int>> vcSet, HashSet<(String, EventType)> eSet)> CurrMap = new Dictionary<(String, EventType), (HashSet<Dictionary<String, int>>, HashSet<(String, EventType)>)>();
private static TextWriter Logger = new ConsoleLogger();
private static HashSet<int> UniqueTimelineSet = new HashSet<int>();

public enum EventType
{
SEND, DEQUEUE
}
public static void AddToCurrentTimeline(String currE, EventType currType, Dictionary<String, int> vectorTime)
{
if (!CurrMap.ContainsKey((currE, currType)))
{
CurrMap[(currE, currType)] = (new HashSet<Dictionary<String, int>>(), 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;
}
}
7 changes: 7 additions & 0 deletions Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
using System.Runtime.Serialization;
using System.Text;
using PChecker.Coverage;
using PChecker.Runtime;
using PChecker.Utilities;

namespace PChecker.SystematicTesting
Expand Down Expand Up @@ -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)
Expand Down
3 changes: 2 additions & 1 deletion Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
Original file line number Diff line number Diff line change
Expand Up @@ -535,7 +535,8 @@ private void RegisterObservers(ControlledRuntime runtime)
/// </summary>
private void RunNextIteration(int schedule)
{
BehavioralObserver.NextIter();
// BehavioralObserver.NextIter();
VectorClockTimeline.RecordTimeline();
if (!IsReplayModeEnabled && ShouldPrintIteration(schedule + 1))
{
Logger.WriteLine($"..... Schedule #{schedule + 1}");
Expand Down

0 comments on commit 3e0f1fa

Please sign in to comment.