Skip to content

Commit b45194b

Browse files
aoli-alankushdesaiChristineZh0uChristine Zhou
authored
Add feedback-guided scheduling algorithms (#791)
* Add feedback strategy. (#715) * Add feedback guided scheduling algorithms. * Fix tests. * Add location information to events. * fix change. * Improving the code with some cleanup. (#719) * Disable trace logging to save disk space. * Update feedback algorithm. * fix feedback strategy. * refactor. * Remove experiment features. --------- Co-authored-by: Ao Li <[email protected]> * PR cleanup (#723) * Added support for generating a warning when spec handles an event but does not add it in its observes list (#716) * Create custom converter for JSON serialization in .NET8 (#717) * Create custom converter for JSON serialization in .NET8 * Add check for different dictionary type for null replacement --------- Co-authored-by: Eric Hua <[email protected]> --------- Co-authored-by: Ankush Desai <[email protected]> Co-authored-by: Eric Hua <[email protected]> Co-authored-by: Eric Hua <[email protected]> * Merge Recent Bug Fixes (#778) * Added support for generating a warning when spec handles an event but does not add it in its observes list (#716) * Create custom converter for JSON serialization in .NET8 (#717) * Create custom converter for JSON serialization in .NET8 * Add check for different dictionary type for null replacement --------- Co-authored-by: Eric Hua <[email protected]> * udpate. * update. * update. --------- Co-authored-by: Eric Hua <[email protected]> Co-authored-by: Eric Hua <[email protected]> Co-authored-by: Ao Li <[email protected]> * Fix feedback strategy and remove experiment features. * Removing Pattern (#786) Co-authored-by: Christine Zhou <[email protected]> * Remove conflict analysis * Removing compiler changes (#789) Co-authored-by: Christine Zhou <[email protected]> * Cleanup. * Revert changes to Event. * Revert changes. * Fix merge conflicts. * Remove temp file. * Rename LastSentReceiver to MessageReceiver * Simplify scheduler implementation. * Revert changes in QLearning strategy. * Refactor. * Added VectorTime and BehavioralObserver class for feedback strategy (#799) Co-authored-by: Christine Zhou <[email protected]> * Revert changes in PCTStrategy. * Revert changes in Probabilistic folder. * revert change. --------- Co-authored-by: Ankush Desai <[email protected]> Co-authored-by: ChristineZh0u <[email protected]> Co-authored-by: Christine Zhou <[email protected]>
1 parent b7c44e2 commit b45194b

File tree

26 files changed

+1675
-38
lines changed

26 files changed

+1675
-38
lines changed

‎Src/PChecker/CheckerCore/Coverage/CoverageInfo.cs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,8 @@ public CoverageInfo()
5454
Machines = new HashSet<string>();
5555
MachinesToStates = new Dictionary<string, HashSet<string>>();
5656
RegisteredEvents = new Dictionary<string, HashSet<string>>();
57+
EventInfo = new EventCoverage();
58+
CoverageGraph = new Graph();
5759
}
5860

5961
/// <summary>

‎Src/PChecker/CheckerCore/Random/IRandomValueGenerator.cs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
// Copyright (c) Microsoft Corporation.
22
// Licensed under the MIT License.
33

4+
using System;
5+
46
namespace PChecker.Random
57
{
68
/// <summary>

‎Src/PChecker/CheckerCore/Runtime/Events/EventInfo.cs‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,8 @@ internal class EventInfo
2323
[DataMember]
2424
internal EventOriginInfo OriginInfo { get; private set; }
2525

26+
internal VectorTime VectorTime;
27+
2628
/// <summary>
2729
/// Initializes a new instance of the <see cref="EventInfo"/> class.
2830
/// </summary>
@@ -34,10 +36,11 @@ internal EventInfo(Event e)
3436
/// <summary>
3537
/// Initializes a new instance of the <see cref="EventInfo"/> class.
3638
/// </summary>
37-
internal EventInfo(Event e, EventOriginInfo originInfo)
39+
internal EventInfo(Event e, EventOriginInfo originInfo, VectorTime v)
3840
: this(e)
3941
{
4042
OriginInfo = originInfo;
43+
VectorTime = new VectorTime(v);
4144
}
4245
}
4346
}

‎Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventQueue.cs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ public EnqueueStatus Enqueue(Event e, EventInfo info)
157157
// A default event handler exists.
158158
var stateName = StateMachine.CurrentState.GetType().Name;
159159
var eventOrigin = new EventOriginInfo(StateMachine.Id, StateMachine.GetType().FullName, stateName);
160-
return (DequeueStatus.Default, DefaultEvent.Instance, new EventInfo(DefaultEvent.Instance, eventOrigin));
160+
return (DequeueStatus.Default, DefaultEvent.Instance, new EventInfo(DefaultEvent.Instance, eventOrigin, StateMachine.VectorTime));
161161
}
162162

163163
/// <summary>
@@ -209,7 +209,7 @@ public void RaiseEvent(Event e)
209209
{
210210
var stateName = StateMachine.CurrentState.GetType().Name;
211211
var eventOrigin = new EventOriginInfo(StateMachine.Id, StateMachine.GetType().FullName, stateName);
212-
var info = new EventInfo(e, eventOrigin);
212+
var info = new EventInfo(e, eventOrigin, StateMachine.VectorTime);
213213
RaisedEvent = (e, info);
214214
StateMachineManager.OnRaiseEvent(e, info);
215215
}

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,11 @@ public abstract class StateMachine
5454
/// </summary>
5555
private protected IEventQueue Inbox;
5656

57+
/// <summary>
58+
/// Keeps track of state machine's current vector time.
59+
/// </summary>
60+
public VectorTime VectorTime;
61+
5762
/// <summary>
5863
/// Cache of state machine types to a map of action names to action declarations.
5964
/// </summary>
@@ -295,6 +300,7 @@ internal void Configure(ControlledRuntime runtime, StateMachineId id, IStateMach
295300
Id = id;
296301
Manager = manager;
297302
Inbox = inbox;
303+
VectorTime = new VectorTime(Id);
298304
}
299305

300306
/// <summary>
@@ -535,6 +541,9 @@ public void SendEvent(PMachineValue target, Event ev)
535541
Assert(target.Permissions.Contains(ev.GetType().Name),
536542
$"Event {ev.GetType().Name} is not in the permissions set of the target machine");
537543
AnnounceInternal(ev);
544+
// Update vector clock
545+
VectorTime.Increment();
546+
BehavioralObserver.AddToCurrentTimeline(ev, BehavioralObserver.EventType.SEND, VectorTime);
538547
Runtime.SendEvent(target.Id, ev, this);
539548
}
540549

@@ -590,6 +599,10 @@ internal async Task RunEventHandlerAsync()
590599

591600
if (status is DequeueStatus.Success)
592601
{
602+
// Update state machine vector clock
603+
VectorTime.Merge(info.VectorTime);
604+
BehavioralObserver.AddToCurrentTimeline(e, BehavioralObserver.EventType.DEQUEUE, VectorTime);
605+
593606
// Notify the runtime for a new event to handle. This is only used
594607
// during bug-finding and operation bounding, because the runtime
595608
// has to schedule an state machine when a new operation is dequeued.

‎Src/PChecker/CheckerCore/Runtime/VectorTime.cs‎

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
using System;
2+
using System.Collections.Generic;
3+
using System.IO;
4+
using System.Linq;
5+
using PChecker.Runtime.StateMachines;
6+
using PChecker.IO.Logging;
7+
8+
public class VectorTime
9+
{
10+
// Dictionary that uses StateMachineId as the key and stores the logical clock as the value
11+
public Dictionary<StateMachineId, int> Clock { get; private set; }
12+
13+
// The ID of the current state machine
14+
15+
private StateMachineId stateMachineId;
16+
17+
public VectorTime(StateMachineId stateMachineId)
18+
{
19+
this.stateMachineId = stateMachineId;
20+
Clock = new Dictionary<StateMachineId, int>();
21+
Clock[stateMachineId] = 0; // Initialize the clock for this state machine
22+
}
23+
24+
// Clone constructor (creates a snapshot of the vector clock)
25+
public VectorTime(VectorTime other)
26+
{
27+
Clock = new Dictionary<StateMachineId, int>(other.Clock);
28+
}
29+
30+
// Increment the logical clock for this state machine
31+
public void Increment()
32+
{
33+
Clock[stateMachineId]++;
34+
}
35+
36+
// Merge another vector clock into this one
37+
public void Merge(VectorTime otherTime)
38+
{
39+
foreach (var entry in otherTime.Clock)
40+
{
41+
StateMachineId otherMachineId = entry.Key;
42+
int otherTimestamp = entry.Value;
43+
44+
if (Clock.ContainsKey(otherMachineId))
45+
{
46+
// Take the maximum timestamp for each state machine
47+
Clock[otherMachineId] = Math.Max(Clock[otherMachineId], otherTimestamp);
48+
}
49+
else
50+
{
51+
// Add the state machine's timestamp if it doesn't exist in this time
52+
Clock[otherMachineId] = otherTimestamp;
53+
}
54+
}
55+
}
56+
57+
// Compare this vector clock to another for sorting purposes
58+
// Rturn value: -1 = This vector clock happens after the other, 1 = This vector clock happens before the other,
59+
// 0 = Clocks are equal or concurrent
60+
public int CompareTo(VectorTime other)
61+
{
62+
bool atLeastOneLess = false;
63+
bool atLeastOneGreater = false;
64+
65+
foreach (var machineId in Clock.Keys)
66+
{
67+
int thisTime = Clock[machineId];
68+
int otherTime = other.Clock.ContainsKey(machineId) ? other.Clock[machineId] : 0;
69+
70+
if (thisTime < otherTime)
71+
{
72+
atLeastOneLess = true;
73+
}
74+
else if (thisTime > otherTime)
75+
{
76+
atLeastOneGreater = true;
77+
}
78+
if (atLeastOneLess && atLeastOneGreater)
79+
{
80+
return 0;
81+
}
82+
}
83+
if (atLeastOneLess && !atLeastOneGreater)
84+
{
85+
return -1;
86+
}
87+
if (atLeastOneGreater && !atLeastOneLess)
88+
{
89+
return 1;
90+
}
91+
return 0;
92+
}
93+
94+
95+
public override string ToString()
96+
{
97+
var elements = new List<string>();
98+
foreach (var entry in Clock)
99+
{
100+
elements.Add($"StateMachine {entry.Key.Name}: {entry.Value}");
101+
}
102+
return $"[{string.Join(", ", elements)}]";
103+
}
104+
105+
public override bool Equals(object obj)
106+
{
107+
if (obj is VectorTime other)
108+
{
109+
return Clock.OrderBy(x => x.Key).SequenceEqual(other.Clock.OrderBy(x => x.Key));
110+
}
111+
return false;
112+
}
113+
114+
public override int GetHashCode()
115+
{
116+
int hash = 17;
117+
foreach (var entry in Clock)
118+
{
119+
hash = hash * 31 + entry.Key.GetHashCode();
120+
hash = hash * 31 + entry.Value.GetHashCode();
121+
}
122+
return hash;
123+
}
124+
}

‎Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
using System.Threading.Tasks;
1515
using PChecker.Coverage;
1616
using PChecker.Exceptions;
17+
using PChecker.Feedback;
1718
using PChecker.Random;
1819
using PChecker.Runtime.Events;
1920
using PChecker.Runtime.Logging;
@@ -150,7 +151,6 @@ private static ControlledRuntime CreateWithConfiguration(CheckerConfiguration ch
150151
/// </summary>
151152
public JsonWriter JsonLogger => LogWriter.JsonLogger;
152153

153-
154154
/// <summary>
155155
/// Returns the current hashed state of the monitors.
156156
/// </summary>
@@ -618,6 +618,8 @@ private EnqueueStatus EnqueueEvent(StateMachineId targetId, Event e, StateMachin
618618
"Cannot send event '{0}' to state machine id '{1}' that is not bound to an state machine instance.",
619619
e.GetType().FullName, targetId.Value);
620620

621+
Scheduler.ScheduledOperation.MessageReceiver = targetId.ToString();
622+
621623
Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Send);
622624
ResetProgramCounter(sender);
623625

@@ -647,7 +649,7 @@ private EnqueueStatus EnqueueEvent(StateMachine stateMachine, Event e, StateMach
647649
var originInfo = new EventOriginInfo(sender.Id, sender.GetType().FullName,
648650
sender.CurrentState.GetType().Name);
649651

650-
var eventInfo = new EventInfo(e, originInfo);
652+
var eventInfo = new EventInfo(e, originInfo, sender.VectorTime);
651653

652654
LogWriter.LogSendEvent(stateMachine.Id, sender.Id.Name, sender.Id.Type, sender.CurrentStateName,
653655
e, isTargetHalted: false);

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,11 @@ internal abstract class AsyncOperation : IAsyncOperation
4949
/// True if the next awaiter is controlled, else false.
5050
/// </summary>
5151
internal bool IsAwaiterControlled;
52+
53+
/// <summary>
54+
/// The receiver if the operation is Send.
55+
/// </summary>
56+
public string MessageReceiver = "";
5257

5358
/// <summary>
5459
/// Initializes a new instance of the <see cref="AsyncOperation"/> class.

0 commit comments

Comments
 (0)