Testing concurrent code: race detectors and model checking

Running every schedule proves a small program, but it costs the number of interleavings. Real tools take two shortcuts. A race detector watches one run and reports the variables that could race in some other schedule. A model checker remembers the states it has seen. For two threads of 10 steps that is 184,756 schedules against 121 states.

A race detector does not run threads. It reads a trace: every read and write of shared data, and every acquire and release of a lock. Our programs become lists of such operations, and interleave turns a program and a schedule into the trace of that run. Two threads that each read and write x and use no lock give the four events below. In this schedule thread 0 finishes before thread 1 starts, so a test would see the right answer. The question for the detector is different: could the two threads have overlapped?

def interleave(programs, schedule):    position = [0] * len(programs)    trace = []    for tid in schedule:        kind, name = programs[tid][position[tid]]        position[tid] += 1        trace.append((tid, kind, name))    return traceunlocked = [[("read", "x"), ("write", "x")], [("read", "x"), ("write", "x")]]trace = interleave(unlocked, [0, 0, 1, 1])print(trace)

[(0, 'read', 'x'), (0, 'write', 'x'), (1, 'read', 'x'), (1, 'write', 'x')]

The first detector uses a discipline: every shared variable should be guarded by some lock that is held at every access. The lockset rule tracks the locks each thread holds, and for every variable intersects the sets of locks held at its accesses. If at least two threads touched the variable, one of them wrote it, and the intersection is empty, then no single lock protects it: report a potential race. The unlocked counter is flagged; the locked one is not. The rule is cheap, and it can raise a false alarm. In the hand-over below thread 0 writes x, and then passes it to thread 1 through the lock. No lock was held at the write, so the rule complains, although the accesses are in fact ordered.

def lockset_races(trace):    held = {}    accesses = {}    for tid, kind, name in trace:        locks = held.setdefault(tid, set())        if kind == "acquire":            locks.add(name)        elif kind == "release":            locks.discard(name)        else:            accesses.setdefault(name, []).append((tid, kind == "write", frozenset(locks)))    racy = []    for name, history in accesses.items():        threads = {tid for tid, _, _ in history}        writes = any(is_write for _, is_write, _ in history)        common = frozenset.intersection(*(locks for _, _, locks in history))        if len(threads) >= 2 and writes and not common:            racy.append(name)    return sorted(racy)locked = [[("acquire", "m"), ("read", "x"), ("write", "x"), ("release", "m")]] * 2guarded = interleave(locked, [0, 0, 0, 0, 1, 1, 1, 1])handoff = [(0, "write", "x"), (0, "acquire", "m"), (0, "release", "m"), (1, "acquire", "m"), (1, "release", "m"), (1, "read", "x")]print("unlocked:", lockset_races(trace))print("locked:  ", lockset_races(guarded))print("handoff: ", lockset_races(handoff))

unlocked: ['x']
locked:   []
handoff:  ['x']

The second detector asks the exact question: is there a chain of orderings from the first access to the second? Two kinds of edge exist, the order inside a thread and the pair release then acquire of the same lock. The happens-before relation is the closure of both. A vector clock per thread records what the thread has seen; a release stores the clock in the lock and an acquire takes the pointwise maximum with it. An access is a race if a conflicting earlier access by another thread has an epoch the current clock has not seen. On the hand-over, the release and the acquire connect the write to the read, so there is no race. It reports only real races, but only in the accesses it observed.

def hb_races(trace):    clocks = {}    lock_clocks = {}    history = {}    racy = set()    for tid, kind, name in trace:        clock = clocks.setdefault(tid, {tid: 1})        if kind == "acquire":            for u, value in lock_clocks.get(name, {}).items():                clock[u] = max(clock.get(u, 0), value)        elif kind == "release":            lock_clocks[name] = dict(clock)            clock[tid] += 1        else:            is_write = kind == "write"            for u, was_write, epoch in history.get(name, []):                if u != tid and (is_write or was_write) and clock.get(u, 0) < epoch:                    racy.add(name)            history.setdefault(name, []).append((tid, is_write, clock[tid]))    return sorted(racy)print("unlocked:", hb_races(trace))print("locked:  ", hb_races(guarded))print("handoff: ", hb_races(handoff))

unlocked: ['x']
locked:   []
handoff:  []

A model checker visits the same program, but it remembers states. In our programs a state is only how far each thread has got, so with threads of n steps there are (n1 + 1) × (n2 + 1) × ... states, however many schedules lead to them. The counter threads below give the numbers for the real data, with the schedules and the states side by side.

def count_states(lengths):    total = 1    for n in lengths:        total *= n + 1    return totaldef counter_programs(ups, locked):    programs = []    for count in ups:        program = []        for _ in range(count):            program += ([("acquire", "m")] if locked else []) + [("read", "x"), ("write", "x")] + ([("release", "m")] if locked else [])        programs.append(program)    return programsreturns = [float(r) for r in load_bars()["close"].pct_change().dropna()][:6]ups = [sum(1 for r in returns[start::2] if r > 0) for start in (0, 1)]for name, lock in (("unlocked", False), ("locked", True)):    programs = counter_programs(ups, lock)    lengths = [len(p) for p in programs]    trace = interleave(programs, serial_schedule(lengths))    print(name, len(trace), "events", lockset_races(trace), hb_races(trace), count_schedules(lengths), "schedules,", count_states(lengths), "states")

unlocked 8 events ['x'] ['x'] 28 schedules, 21 states
locked 16 events [] [] 1820 schedules, 65 states

One serial trace is enough for both detectors to find the missing lock, and the locked program is clean. The model checker's advantage over brute force is the factor between 1,820 and 65, and it grows without bound: for 10 and 10 steps it is 184,756 against 121. That is why model checking can cover programs that plain enumeration never could, while a race detector costs one pass over one run.

The lab follows the lecture: the trace of a run, the lockset rule, the happens-before rule with vector clocks, the count of states, the programs of the counting threads, and the study of both detectors and both space sizes on SPY up days.

• Function · questionBuilds on
• interleave(programs, schedule)What happened, in what order?Plain arithmetic
• lockset_races(trace)Which variables have no common lock?Plain arithmetic
• hb_races(trace)Which variables have unordered accesses?Plain arithmetic
• count_states(lengths)How many states must be remembered?Plain arithmetic
• counter_programs(ups, locked)What do the counting threads do?Plain arithmetic
• study(bars)Do the detectors agree on SPY?counter_programsinterleavelockset_raceshb_racescount_states

Next topic: lock-free code has one more danger that no detector or checker can fix after the fact: when a thread frees a node that another thread is still reading. Hazard pointers and epoch reclamation build the two classic ways to free memory safely, and the explorer shows a use-after-free under every schedule that you have not prevented.