If I understand this correctly, this approach has limitations regarding soft forward-progress guarantees.
Consider a cmpxchg loop where the body computation is not quite trivial, but on real hardware (and with real schedulers) is exceedingly unlikely to be interrupted on a given CPU. Thus, if `n` is the number of CPUs, it has a worst-case `1/n` chance of making progress. But with this testing approach, it instead has a `1/t^p` chance, where `t` is the number of tasks (which may be far larger than the number of CPUs) and `p` is the number of pauses (easily at least 3) within the not-quite-trivial loop body; this is sufficient to turn a working algorithm into a broken one.
OTOH, if you do want the tester to detect soft forward-progress as a bug (because you want hard forward-progress), this doesn't seem to provide useful tools either.
(Regardless this is certainly useful for a lot of concurrency problems).
i don't think that's right. it's just 1/t. after all, after t time, one task must have made progress; since there are t tasks, the probability that i'm the task that made progress is just 1/t
the primary point of confusion, i think, is that getting interrupted does not mean that you are necessarily going to lose the cas
Consider a cmpxchg loop where the body computation is not quite trivial, but on real hardware (and with real schedulers) is exceedingly unlikely to be interrupted on a given CPU. Thus, if `n` is the number of CPUs, it has a worst-case `1/n` chance of making progress. But with this testing approach, it instead has a `1/t^p` chance, where `t` is the number of tasks (which may be far larger than the number of CPUs) and `p` is the number of pauses (easily at least 3) within the not-quite-trivial loop body; this is sufficient to turn a working algorithm into a broken one.
OTOH, if you do want the tester to detect soft forward-progress as a bug (because you want hard forward-progress), this doesn't seem to provide useful tools either.
(Regardless this is certainly useful for a lot of concurrency problems).