PSharp icon indicating copy to clipboard operation
PSharp copied to clipboard

PCT algorithm bugs

Open paulthomson opened this issue 7 years ago • 1 comments

I think there are some bugs in the PCT algorithm. I will send a pull request or more details later.

paulthomson avatar Jul 14 '17 16:07 paulthomson

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!

paulthomson avatar Jul 15 '17 08:07 paulthomson