Testar código concorrente: detectores de corrida e verificação de modelos

Executar todos os escalonamentos prova um programa pequeno, mas custa o número de intercalações. As ferramentas reais tomam dois atalhos. Um detector de corridas observa uma execução e informa as variáveis que poderiam competir em outro escalonamento. Um verificador de modelos lembra dos estados vistos. Para duas threads de 10 passos são 184 756 escalonamentos contra 121 estados.

Um detector de corridas não executa threads. Ele lê um trace: cada leitura e escrita de dados compartilhados e cada aquisição e liberação de uma trava. Nossos programas viram listas dessas operações, e interleave transforma um programa e um escalonamento no trace daquela execução. Duas threads que leem e escrevem x cada uma sem trava dão os quatro eventos abaixo. Neste escalonamento a thread 0 termina antes de a thread 1 começar, então um teste veria a resposta certa. A pergunta do detector é outra: as duas threads poderiam ter se sobreposto?

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

O primeiro detector usa uma disciplina: toda variável compartilhada deveria ser guardada por alguma trava mantida em cada acesso. A regra do lockset acompanha as travas que cada thread mantém e, para cada variável, intersecta os conjuntos de travas mantidos em seus acessos. Se pelo menos duas threads tocaram a variável, uma a escreveu e a interseção é vazia, nenhuma trava única a protege: reporta-se uma corrida potencial. O contador sem trava é sinalizado; o com trava, não. A regra é barata e pode dar um falso alarme. Na passagem abaixo a thread 0 escreve x e depois o entrega à thread 1 pela trava. Nenhuma trava era mantida na escrita, então a regra reclama, embora os acessos estejam na verdade ordenados.

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

O segundo detector faz a pergunta exata: existe uma cadeia de ordens do primeiro acesso ao segundo? Há dois tipos de aresta, a ordem dentro de uma thread e o par liberação e depois aquisição da mesma trava. A relação happens-before é o fecho de ambas. Um relógio vetorial por thread registra o que a thread viu; uma liberação guarda o relógio na trava e uma aquisição toma o máximo componente a componente com ele. Um acesso é uma corrida se um acesso anterior conflitante de outra thread tem uma época que o relógio atual não viu. Na passagem, a liberação e a aquisição ligam a escrita à leitura, então não há corrida. Ele só reporta corridas reais, mas apenas nos acessos que observou.

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

Um verificador de modelos visita o mesmo programa, mas lembra estados. Nos nossos programas um estado é só o quanto cada thread avançou, então com threads de n passos há (n1 + 1) × (n2 + 1) × ... estados, quantos forem os escalonamentos que levam a eles. As threads contadoras abaixo dão os números para os dados reais, com os escalonamentos e os estados lado a lado.

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

Um único trace serial basta para os dois detectores acharem a trava que falta, e o programa com trava está limpo. A vantagem do verificador de modelos sobre a força bruta é o fator entre 1820 e 65, e cresce sem limite: para 10 e 10 passos são 184 756 contra 121. Por isso a verificação de modelos pode cobrir programas que a enumeração simples nunca alcançaria, enquanto um detector de corridas custa uma passada sobre uma execução.

O laboratório segue a aula: o trace de uma execução, a regra do lockset, a regra happens-before com relógios vetoriais, a contagem de estados, os programas das threads contadoras e o estudo dos dois detectores e dos dois tamanhos de espaço nos dias de alta do SPY.

• Função · perguntaBaseia-se em
• interleave(programs, schedule)O que aconteceu, em que ordem?Aritmética simples
• lockset_races(trace)Quais variáveis não têm trava comum?Aritmética simples
• hb_races(trace)Quais variáveis têm acessos não ordenados?Aritmética simples
• count_states(lengths)Quantos estados é preciso lembrar?Aritmética simples
• counter_programs(ups, locked)O que fazem as threads contadoras?Aritmética simples
• study(bars)Os detectores concordam no SPY?counter_programsinterleavelockset_raceshb_racescount_states

Próximo tópico: o código sem travas tem mais um perigo que nenhum detector ou verificador consegue consertar depois: quando uma thread libera um nó que outra thread ainda está lendo. Hazard pointers e reclamação por épocas constroem as duas formas clássicas de liberar memória com segurança, e o explorador mostra um uso após liberação sob cada escalonamento que você não impediu.