Skip to content

Commit

Permalink
Revert the dynamic sync point generation algorithm for PCT scheduler. (…
Browse files Browse the repository at this point in the history 
…#802)

* Revert PCT scheduler changes.

* Set max unfair scheduling steps for all feedback guided algorithms.

* Fix warnings.

* Clean up changes.
  • Loading branch information
@aoli-al
aoli-al authored Nov 20, 2024
1 parent ec71574 commit 65042fe
Show file tree
Hide file tree
Showing 2 changed files with 46 additions and 64 deletions.
11 changes: 2 additions & 9 deletions Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/FeedbackGuidedStrategy.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ public record GeneratorRecord(int Priority, StrategyGenerator Generator, List<in
private int _pendingMutations = 0;
private bool _shouldExploreNew = false;
private HashSet<GeneratorRecord> _visitedGenerators = new HashSet<GeneratorRecord>();
private GeneratorRecord? _currentParent = null;
private GeneratorRecord _currentParent = null;

private System.Random _rnd = new System.Random();

Expand All @@ -41,14 +41,7 @@ public record GeneratorRecord(int Priority, StrategyGenerator Generator, List<in
/// </summary>
public FeedbackGuidedStrategy(CheckerConfiguration checkerConfiguration, ControlledRandom inputGenerator, IScheduler scheduler)
{
if (scheduler is PCTScheduler)
{
_maxScheduledSteps = checkerConfiguration.MaxUnfairSchedulingSteps;
}
else
{
_maxScheduledSteps = checkerConfiguration.MaxFairSchedulingSteps;
}
_maxScheduledSteps = checkerConfiguration.MaxUnfairSchedulingSteps;
Generator = new StrategyGenerator(inputGenerator, scheduler);
}

Expand Down
99 changes: 44 additions & 55 deletions Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/PCTScheduler.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,11 +27,6 @@ internal class PCTScheduler : IScheduler
/// </summary>
private readonly IRandomValueGenerator _randomValueGenerator;

/// <summary>
/// The maximum number of steps to schedule.
/// </summary>
private readonly int MaxScheduledSteps;

/// <summary>
/// The number of scheduled steps.
/// </summary>
Expand All @@ -50,18 +45,13 @@ internal class PCTScheduler : IScheduler
/// <summary>
/// List of prioritized operations.
/// </summary>
private readonly List<AsyncOperation> PrioritizedOperations;

/// <summary>
/// Next execution point where the priority should be changed.
/// </summary>
private int _nextPriorityChangePoint;
private readonly List<AsyncOperation> PrioritizedOperations = new();

/// <summary>
/// Number of switch points left (leq MaxPrioritySwitchPoints).
/// Set of priority change points.
/// </summary>
private int _numSwitchPointsLeft;

private readonly SortedSet<int> PriorityChangePoints = new();
/// <summary>
/// Initializes a new instance of the <see cref="PCTStrategy"/> class.
/// </summary>
Expand All @@ -71,14 +61,11 @@ public PCTScheduler(int maxPrioritySwitchPoints, int scheduleLength, IRandomValu
ScheduledSteps = 0;
ScheduleLength = scheduleLength;
MaxPrioritySwitchPoints = maxPrioritySwitchPoints;
PrioritizedOperations = new List<AsyncOperation>();
double switchPointProbability = 0.1;
if (ScheduleLength != 0)
{
switchPointProbability = 1.0 * _numSwitchPointsLeft / (ScheduleLength - ScheduledSteps + 1);
PreparePriorityChangePoints(ScheduleLength);
}
_nextPriorityChangePoint = Generator.Mutator.Utils.SampleGeometric(switchPointProbability, random.NextDouble());


}

public virtual bool GetNextOperation(AsyncOperation current, IEnumerable<AsyncOperation> ops,
Expand All @@ -89,28 +76,37 @@ public virtual bool GetNextOperation(AsyncOperation current, IEnumerable<AsyncOp
var enabledOperations = ops.Where(op => op.Status is AsyncOperationStatus.Enabled).ToList();
if (enabledOperations.Count == 0)
{
if (_nextPriorityChangePoint == ScheduledSteps)
if (PriorityChangePoints.Contains(ScheduledSteps))
{
MovePriorityChangePointForward();
}

return false;
}

var highestEnabledOp = GetPrioritizedOperation(enabledOperations, current);
if (next is null)
{
next = highestEnabledOp;
}
next = GetPrioritizedOperation(enabledOperations, current);

return true;
}

/// <summary>
/// Moves the current priority change point forward. This is a useful
/// optimization when a priority change point is assigned in either a
/// sequential execution or a nondeterministic choice.
/// </summary>
private void MovePriorityChangePointForward()
{
_nextPriorityChangePoint += 1;
Debug.WriteLine("<PCTLog> Moving priority change to '{0}'.", _nextPriorityChangePoint);
PriorityChangePoints.Remove(ScheduledSteps);
var newPriorityChangePoint = ScheduledSteps + 1;
while (PriorityChangePoints.Contains(newPriorityChangePoint))
{
newPriorityChangePoint++;
}

PriorityChangePoints.Add(newPriorityChangePoint);
Debug.WriteLine("<PCTLog> Moving priority change to '{0}'.", newPriorityChangePoint);
}


private AsyncOperation GetHighestPriorityEnabledOperation(IEnumerable<AsyncOperation> choices)
{
Expand Down Expand Up @@ -146,36 +142,21 @@ private AsyncOperation GetPrioritizedOperation(List<AsyncOperation> ops, AsyncOp
}


var prioritizedSchedulable = GetHighestPriorityEnabledOperation(ops);
if (_nextPriorityChangePoint == ScheduledSteps)
if (PriorityChangePoints.Contains(ScheduledSteps))
{
if (ops.Count == 1)
{
MovePriorityChangePointForward();
}
else
{
PrioritizedOperations.Remove(prioritizedSchedulable);
PrioritizedOperations.Add(prioritizedSchedulable);
Debug.WriteLine("<PCTLog> 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;
}

var priority = GetHighestPriorityEnabledOperation(ops);
PrioritizedOperations.Remove(priority);
PrioritizedOperations.Add(priority);
Debug.WriteLine("<PCTLog> Operation '{0}' changes to lowest priority.", priority);
}
}
var prioritizedSchedulable = GetHighestPriorityEnabledOperation(ops);

if (Debug.IsEnabled)
{
Expand Down Expand Up @@ -209,18 +190,26 @@ public virtual bool PrepareForNextIteration()
{
ScheduleLength = Math.Max(ScheduleLength, ScheduledSteps);
ScheduledSteps = 0;
_numSwitchPointsLeft = MaxPrioritySwitchPoints;

PrioritizedOperations.Clear();
double switchPointProbability = 0.1;
if (ScheduleLength != 0)
PriorityChangePoints.Clear();
return true;
}

private void PreparePriorityChangePoints(int step)
{
List<int> listOfInts = new List<int>();
for (int i = 0; i < step; i++)
{
switchPointProbability = 1.0 * _numSwitchPointsLeft / (ScheduleLength - ScheduledSteps + 1);
listOfInts.Add(i);
}

_nextPriorityChangePoint =
Generator.Mutator.Utils.SampleGeometric(switchPointProbability, _randomValueGenerator.NextDouble());
return true;
for (int i = 0; i < MaxPrioritySwitchPoints; i++)
{
int index = _randomValueGenerator.Next(listOfInts.Count);
PriorityChangePoints.Add(listOfInts[index]);
listOfInts.RemoveAt(index);
}
}

public IScheduler Mutate()
Expand Down

0 comments on commit 65042fe

Please sign in to comment.