Optimization possible

[jcp19]

Basically, the races seem to be very "local" in the sense that even though they have hundreds of candidates, what happens, at least in the case of the cyclon, is that these races translate into a few unique locations. Therefore, a possible optimization would be to make a list of unique possible locations in race from the set of candidates to race conditions and then only solve until you find a race. All other candidates can be ignored because even if they are sat, they will give rise to a race that has already been detected

[jcp19]

Another idea in line with the previous one:

Instead of querying the SAT solver for each data race candidate, we can instead, for each pair of candidate locations, gather all candidate pairs in a Collection P and then, generate the following assertion to be run with the HB model:

p1.fst = p1.snd || p2.fst = p2.snd || ... || pN.fst = pN.snd,

where pi is a pair of P.

The advantage of this is that the SAT solver will only be queried once per candidate location and it will stop whenever the first concurrent pair of events is found.