It seems like it would be possible to enumerate all interesting orderings of several threads running at once at the threading-engine level, and therefore do this kind of probabilistic test deterministically.
Of course, the number of possible orderings of two n-length programs is very high (2n choose n, since 2n instructions are run in total and you can place the n instructions in one thread first). But the language definition also provides some concept of 'commuting' operations. For example, unrelated writes to two different variables can't have their orderings matter. That should cut down the number of orderings a great deal. And it's possible useful even if it it's only practical for small programs with few total orderings.
Is there a language or framework that does something like this?