PSharp
PSharp copied to clipboard
PCT algorithm bugs
I think there are some bugs in the PCT algorithm. I will send a pull request or more details later.
Here I would change:
var mIndex = RandomNumberGenerator.Next(PrioritizedSchedulableChoices.Count) + 1;
// ->
var mIndex = RandomNumberGenerator.Next(PrioritizedSchedulableChoices.Count + 1);
The former does not allow mIndex
to be 0. This means a thread can never be added as the highest priority thread. Or is this intentional because the 0th thread is always the initial thread? Will it ever do sends?
And here in the Fisher-Yates shuffle, I think the random choice should be between 0 and idx (inclusive), not 0 and ScheduleLength (exclusive). Unless both are valid.
There are a few other changes I could suggest. In particular, PCT implementations that I can find (four of them, including two of my own :) ) pick priority change points by repeatedly doing changePoints.Add(Random.Next(k)); if two change points end up on the same scheduling point, that is fine---there will just be two threads that get lowered. But maybe we should fix/dismiss the two queries above first so we have a baseline for comparison for any additional changes. Maybe we should also wait until DPOR is merged!