That said, although modeling out-of-order execution might make the semantics
simpler, the additional expressivity definitely makes the resulting analysis
more complex.
Fully modeling out-of-order execution leads to an explosion in
the number of possible executions of a program; naively incorporating
out-of-order execution into a detection or mitigation tool results in an
intractable analysis.
Indeed, while Guarnieri et al.  [1]} and Colvin and
Winter [2]} present analysis tools based on their respective
out-of-order semantics, they only analyze very simple Spectre gadgets, not
code used in real programs.
Instead, for analysis tools based on out-of-order semantics to scale to real
programs, developers need to use lemmas to reduce the number of possibilities
the analysis needs to consider.
As one example, Pitchfork [3]} operates on a set of
“worst-case schedules” which represent a small subset of all possible
out-of-order schedules.
The developers formally argue that this reduction does not affect the
soundness of Pitchfork's analysis.
