It tracks "conflicts" at mutable boundaries, building: 1. A "shadow stack" recording when values are assigned to objects which are referenced from more than one thread. 2. A finer-grained model of SQL and Redis items that take into account some of the semantics of their concurrency models.
The code executes normally once, to get conflict points, then it uses a version of an algorithm called Dynamic Partial Order Reduction (DPOR) to efficiently search through all non-isomorphic traces looking for failures (either a crash, a statically detected deadlock, or a violation of the property/invariant provided in the test). This was partially inspired by the rust concurrency testing library Loom, though uses monkey-patching instead of customer concurrency primitives.