测试并发代码：竞态检测器与模型检验

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')]

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']

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:  []

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