Probabilistic Concurrency Testing.
Burckhardt, Kothari, Musuvathi, Nagarakatte. "A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs", ASPLOS 2010.
Each managed process gets a random initial priority. On every step the
highest-priority enabled (i.e. ready) process runs. Before the test
starts, d - 1 step indices are drawn uniformly from [1, max_steps];
at each, the priority of whichever process would run next is demoted
to a fresh, lower-than-everyone priority. This produces a randomized
schedule that hits any bug of depth d with probability ≥ 1 / (n · k^(d-1))
per iteration.
Options
:seed— RNG seed (required):max_steps— total scheduling steps (required):bug_depth—din PCT terms (default 3):high_prio_max— upper bound for initial priorities (default 1_000_000)
Note: the algorithm ships PCT as described. For liveness add Lockstep.Strategy.FairPCT.