I have been playing around with various settings in the arbiter - the body of code that says when an instruction is interesting enough to be a choice point, and that also chooses whom to run next at a choice point we haven't visited before - and am interested to note the differences in the direction of tree traversal.
At any choice point we haven't visited before, choosing any thread to run will make progress with the search (the real progress logic is in the explorer, which marks off old branches as all explored, uninteresting, or still interesting) - so the arbiter can choose to continue running the current thread (unless it descheduled itself), or to preempt and run somebody else. I call staying with the current thread the "leftmost branch", so a left-to-right tree traversal is one which starts off with fewer preemptions.
The interesting trend is that left-to-right traversals seem to take more time to find a bug (which I did not expect), but produce shorter, more concise choice traces at the end (which I did). Traversing left-to-right finds an 8-long choice trace (2-3-4-2-3-2-3-4) in 6.5 minutes, while a right-to-left traversal of the same tree finds a 15-long choice trace (2-3-2-3-4-3-4-3-4-3-2-4-2-3-4) in 2.5 minutes.
Also, with one particular bug that I edited the guest kernel to have, a different failure came up in each traversal order (one tripped an assert, and another got a thread wedged on an unowned-but-locked mutex). I wasn't surprised, but still think it is very cool.
Next up: making sure landslide can easily find already-known bugs in student-submitted kernels, rather than just in my own.
