[pshc]

Their debugger searches for bugs exhaustively over all non-equivalent thread timings, but I can find no mention (in the paper or otherwise) of whether this will blow up with a large number of threads or amount of control flow; even the illustration on their site screams "exponential!" to me.

Interesting paper from what I could glean, though.

EDIT: "Jinx dynamically builds a set of potential interleavings (i.e., alternate eventualities, or execution scenarios, that will occur under some future set of conditions) that are most likely to result in concurrency faults, and quickly tests those execution paths to surface concurrency problems including deadlocks, race conditions, and atomicity violations." So it's more selective than I first thought.

[pgodman100]

Hi. Disclaimer: I work for Corensic.

We avoid exponential search space problems by using sampling, and curtailing of exploration. We choose what to explore based on research about where bugs are likely to lie. Exhaustive examination of all but fairly trivial problems is impossible for exactly this reason, and this is why we sample: rather than force users to change the way they write code, we deal with the way they have written code.

Thanks, Pete

[stcredzero]

We avoid exponential search space problems by using sampling, and curtailing of exploration.

Basically, you use the same general strategies that are used to write Go playing programs.

[pgodman100]

Yes, this is a lot like AI approaches used for playing games. We examine many and nested what-if scenarios involving reordering of memory communications to identify problematic sequences. Note that we operate at the memory level and so we don't have problems with particular OS or threading-package constructs. If your code can run in parallel, Jinx can explore it.