An interleaving explorer: finding bugs by enumerating schedules

Trying schedules by hand finds a bug only if you guess the right one. An explorer runs the program under every schedule, lists every outcome and hands you the schedule that broke it. For two threads counting the up days of ten SPY returns there are 210 schedules, and only 10 of them give the right count.

A schedule is an order of turns, and thread t takes exactly lengths[t] of them. To count the orders, put all the turns in a row (the sum of the lengths of them), which can be arranged in that many factorial ways; then divide by the factorial of each thread's turns, because swapping two turns of the same thread does not give a new schedule. This is the multinomial coefficient. It grows fast: two threads of 2 turns each have only 6 schedules, three threads of 3 turns have 1,680, and two threads of 10 turns have 184,756. That is why nobody can check a concurrent program by trying schedules at random and hoping.

def count_schedules(lengths):    total = factorial(sum(lengths))    for n in lengths:        total //= factorial(n)    return totalprint(count_schedules([2, 2]))print(count_schedules([3, 3, 3]))print(count_schedules([10, 10]))

6
1680
184756

In the last lab a thread was a list of steps. Real code is better written as ordinary Python, so from now on a thread is a generator that takes the shared dictionary and runs yield before every access to shared data. One call of next() then runs the thread up to its next access and no further, which makes one turn exactly one step that another thread can interleave with. run_threads primes every generator (runs it to its first yield), gives a turn to the thread named by each entry of the schedule, and when the schedule ends lets the unfinished threads finish in thread order. all_schedules lists every order of turns by choosing which thread goes first and recursing on what is left. Below, the six schedules of two threads that increment once each.

def all_schedules(lengths):    if sum(lengths) == 0:        return [[]]    out = []    for tid, n in enumerate(lengths):        if n:            rest = list(lengths)            rest[tid] -= 1            out += [[tid] + tail for tail in all_schedules(rest)]    return outdef run_threads(make_threads, schedule, shared=None):    shared = dict(shared or {})    threads = make_threads(shared)    alive = [True] * len(threads)    def turn(tid):        try:            next(threads[tid])        except StopIteration:            alive[tid] = False    for tid in range(len(threads)):        turn(tid)    for tid in schedule:        if alive[tid]:            turn(tid)    while any(alive):        for tid in range(len(threads)):            if alive[tid]:                turn(tid)    return sharedtwo = lambda shared: [increments(1)(shared), increments(1)(shared)]for schedule in all_schedules([2, 2]):    print(schedule, run_threads(two, schedule))

[0, 0, 1, 1] {'x': 2}
[0, 1, 0, 1] {'x': 1}
[0, 1, 1, 0] {'x': 1}
[1, 0, 0, 1] {'x': 1}
[1, 0, 1, 0] {'x': 1}
[1, 1, 0, 0] {'x': 2}

Two of the six schedules end at 2, the other four at 1. The two good ones are those where one thread does both its steps before the other starts. In the other four both threads read before either writes, which is exactly the lost update of the last lab, now found without guessing.

explore runs the program under every schedule and counts how many schedules give each final state. The key is a sorted tuple of (name, value) pairs so that equal states are the same key. find_schedule asks the question a bug report asks: which schedule breaks my invariant? It returns the first one, and because run_threads is deterministic you can replay it, print it, or paste it into a test. If it returns None, the invariant holds under every schedule, which is a proof for this small program, not a hope.

def explore(make_threads, lengths, shared=None):    outcomes = {}    for schedule in all_schedules(lengths):        key = tuple(sorted(run_threads(make_threads, schedule, shared).items()))        outcomes[key] = outcomes.get(key, 0) + 1    return outcomesdef find_schedule(make_threads, lengths, check, shared=None):    for schedule in all_schedules(lengths):        if not check(run_threads(make_threads, schedule, shared)):            return schedule    return Noneprint(explore(two, [2, 2]))print(find_schedule(two, [2, 2], lambda shared: shared["x"] == 2))

{(('x', 2),): 2, (('x', 1),): 4}
[0, 1, 0, 1]

returns = [float(r) for r in load_bars()["close"].pct_change().dropna()][:10]ups = [sum(1 for r in returns[start::2] if r > 0) for start in (0, 1)]lengths = [2 * k for k in ups]many = lambda shared: [increments(k)(shared) for k in ups]print(ups, count_schedules(lengths))print({dict(key)["x"]: n for key, n in explore(many, lengths).items()})

[2, 3] 210
{5: 10, 4: 70, 3: 104, 2: 26}

The right answer, x = 5, appears in only 10 of 210 schedules, about 5%. A test that runs the program once, or a hundred times on a real machine where the threads rarely overlap exactly like this, would pass almost every time and still ship a bug. The explorer cannot miss it, and find_schedule hands you the first culprit: [0, 0, 0, 1, 0, 1, 1, 1, 1, 1].

The lab follows the lecture: the number of schedules, the list of all of them, the machine that runs generator threads under a schedule, the explorer that counts outcomes, the search for the first schedule that breaks an invariant, and the study of two threads counting SPY up days.

• Function · questionBuilds on
• count_schedules(lengths)How many schedules does the program have?Plain arithmetic
• all_schedules(lengths)Which are they, in order?Plain arithmetic
• run_threads(make_threads, schedule, shared)What does one schedule leave behind?Plain arithmetic
• explore(make_threads, lengths, shared)Which outcomes exist, and how often?all_schedulesrun_threads
• find_schedule(make_threads, lengths, check)Which schedule breaks the invariant first?all_schedulesrun_threads
• study(bars)How many schedules of SPY counting go wrong?count_schedulesexplorefind_schedule

Next topic: the explorer shows that the bug is real; now we repair it. Atomics and read-modify-write adds the operations a processor can do in one indivisible step, such as fetch-and-add and compare-and-swap, and you check with the explorer that the counter is right under every schedule.