dscheck icon indicating copy to clipboard operation
dscheck copied to clipboard

Backtracking optimizations

Open art-w opened this issue 1 year ago • 5 comments

(Follow-up on https://github.com/sadiqj/dscheck/pull/2 )

Sorry for the big dirty PR! I was inspired to optimize the backtracking and it now terminates in a few seconds on the examples that I care about:

  • I started with some simple stuff, like not re-running the execution from scratch unless we really have to (= we are backtracking)
  • The backtracking steps happen when two "threads" access the same atomic: I thought it could be more precise, as we don't need to test the alternative ordering if both were doing an Atomic.get (we only want to backtrack when the atomic usages could yield a different outcome, so a "read" with a "write" etc.)
  • The backtracking was scheduling the alternate thread for only one operation: In general, this operation is not the one we wanted to permute (just a prerequisite) and so it had to do it multiple times before the real goal was achieved. In the example below, if we wanted to swap (A3) with (B3) then it would bubble the B operations one at a time:
AAA(A3)AAB1B2(B3)...
   \B1(A3)AAB2(B3)...
     \B2(A3)AA(B3)...
       \B3(A3)AA...

It now does a "big" backstep by scheduling all the operations to permute in the backtracking:

AAA(A3)AAB1B2(B3)...
   \B1B2(B3)(A3)AA...

This wasn't so simple though, as now the atomics and spawns can be created in a different order, changing their globally unique int identifiers. The fix to give them stable ids was to track the creations locally in each thread rather than globally (so rather than "I'm the Xth atomic ever created" we do "I'm the Xth atomic created by thread Yth... which was itself created by thread Zth from the root" with X,Y,Z local counters to each parent threads).

Furthermore, we sometimes want to backstep a thread operation to a point where the thread didn't exist yet... and so we need to also backstep its parent operations that led to our thread creation.

Anyway, I tested it intensively and hopefully I didn't mess up too badly but this was quite involved so there might be some bugs lurking... Let me know if I can do anything to ease the review :)

art-w avatar Oct 03 '22 10:10 art-w