Projeto final: uma distribuição de dados de mercado sem travas com provas de seus invariantes

O projeto final é uma distribuição: um produtor publica ticks do SPY e vários consumidores leem todos eles, sem nenhuma trava. Tudo o que você construiu se encontra aqui. Uma cauda que só o produtor move, um cursor privado por consumidor para que ninguém dispute, uma ordem de escrita que decide o que um leitor pode ver e um explorador que transforma «parece funcionar» numa afirmação sobre cada escalonamento.

O fluxo é um registro que só cresce. A posição p guarda tick<p> e tail diz quantas posições foram publicadas. Só o produtor escreve ticks e a cauda, então não há o que disputar do lado dele. Cada consumidor possui um cursor, a próxima posição que lerá, e ninguém mais o escreve. Esse é todo o truque de uma distribuição: os consumidores nunca escrevem nada que os outros leem, então acrescentar um consumidor não custa nada aos demais. O único fato compartilhado é a cauda, e a única pergunta é em que ordem o produtor escreve o tick e move a cauda. Movê-la depois dos dados: um leitor que vê a nova cauda encontra os dados. Movê-la antes: um leitor pode ver uma posição ainda não escrita.

def publish(shared, tick, safe=True):    if safe:        yield        pos = shared["tail"]        shared["tick%d" % pos] = tick        shared["put%d" % pos] = tick        yield        shared["tail"] = pos + 1    else:        yield        pos = shared["tail"]        shared["tail"] = pos + 1        yield        shared["tick%d" % pos] = tick        shared["put%d" % pos] = tickfor safe in (True, False):    shared, _ = run_prefix(lambda sh: [publish(sh, 9369, safe)], [0], make_feed(1))    print("safe  " if safe else "unsafe", "after one turn:", {k: v for k, v in shared.items() if k in ("tail", "tick0")})

safe   after one turn: {'tail': 0, 'tick0': 9369}
unsafe after one turn: {'tail': 1}

Uma consulta leva dois turnos. O primeiro lê a cauda. O segundo lê o cursor do consumidor e, se o cursor está atrás da cauda, lê o tick, avança o cursor e anota o que obteve. Nada pode mudar a posição sob seus pés, porque só este consumidor escreve seu cursor. O que pode dar errado é o conteúdo do tick: um leitor que entra depois de a cauda mover mas antes de os dados chegarem não lê nada. A consulta anota isso como None, para o verificador ver.

def poll(shared, c):    yield    tail = shared["tail"]    yield    pos = shared["cur%d" % c]    if pos >= tail:        return None    value = shared.get("tick%d" % pos)    shared["cur%d" % c] = pos + 1    shared["got%d_%d" % (c, pos)] = value    return valueready = dict(make_feed(1), tail=1)shared, alive = run_prefix(lambda sh: [poll(sh, 0)], [0, 0], ready)print("tail is 1 but tick0 was never written:", {k: v for k, v in shared.items() if k.startswith(("cur", "got"))})

tail is 1 but tick0 was never written: {'cur0': 1, 'got0_0': None}

O que significa «correto» para o fluxo? Três afirmações sobre o estado final. Rasgado: cada tick recebido por um consumidor é igual ao tick posto naquela posição (um tick ausente recebido como None está rasgado). Buraco: cada consumidor recebeu as posições 0, 1, 2, ... sem buraco. Estouro: nenhum cursor está além da cauda. verify explora cada escalonamento de um produtor e dos consumidores e conta os que quebram cada uma. O explorador é a prova: não pode amostrar a execução sortuda, visita todas.

def violations(final):    puts = {int(key[3:]): value for key, value in final.items() if key.startswith("put")}    gots = {}    for key, value in final.items():        if key.startswith("got"):            c, p = key[3:].split("_")            gots[(int(c), int(p))] = value    broken = []    if any(value != puts.get(p) for (c, p), value in gots.items()):        broken.append("torn")    for c in {c for c, _ in gots}:        if sorted(p for cc, p in gots if cc == c) != list(range(sum(1 for cc, _ in gots if cc == c))):            broken.append("gap")            break    if any(key.startswith("cur") and value > final["tail"] for key, value in final.items()):        broken.append("overrun")    return sorted(broken)def verify(ticks, polls, safe=True):    outcomes = explore_all(feed_threads(ticks, polls, safe), make_feed(len(polls)))    broken = {}    delivered = 0    for key, count in outcomes.items():        final = dict(key)        delivered = max(delivered, sum(1 for k in final if k.startswith("got")))        for name in violations(final):            broken[name] = broken.get(name, 0) + count    return {"schedules": sum(outcomes.values()), "broken": dict(sorted(broken.items())), "delivered": delivered}ticks = [9369, 9305]print("safe  ", verify(ticks, (2, 1), True))print("unsafe", verify(ticks, (2, 1), False))

safe   {'schedules': 3150, 'broken': {}, 'delivered': 3}
unsafe {'schedules': 3150, 'broken': {'torn': 869}, 'delivered': 3}

O mesmo programa, 3150 escalonamentos, e uma única troca de ordem de duas linhas transforma «nenhum quebrado» em 869 quebrados. A maioria são escalonamentos que alguns milhares de execuções de teste quase nunca atingiriam. Esse é o argumento para explorar em vez de testar, e é toda a habilidade numa tabela: um modelo pequeno o bastante para enumerar, um verificador de invariantes e um veredicto sobre cada escalonamento.

O laboratório segue a aula: o fluxo vazio, o produtor nas suas duas ordens, a consulta do consumidor, o verificador dos três invariantes, o verificador que explora todos os escalonamentos, uma repetição de uma execução calma em que cada consumidor recebe os ticks em ordem e o estudo em fechamentos do SPY.

• Função · perguntaBaseia-se em
• make_feed(consumers)O que é compartilhado?Aritmética simples
• publish(shared, tick, safe)Dados primeiro ou cauda primeiroAritmética simples
• poll(shared, c)O próximo tick do consumidor cAritmética simples
• violations(final)Quais invariantes quebraram?Aritmética simples
• verify(ticks, polls, safe)O fluxo está correto sob todos os escalonamentos?explore_allviolations
• drain(ticks, polls)O que cada consumidor recebe?run_prefix
• study(bars)Seguro, inseguro e calmo no SPYverifydrain

Isso completa a habilidade sem travas. Agora você sabe construir as peças (atômicos, compare-and-swap, pilhas e filas), nomear os perigos (corridas, ABA, reclamação) e, acima de tudo, checar um desenho contra cada escalonamento em vez de confiar numa execução que passou por acaso. O próximo passo é a mesma disciplina em hardware real, nos tópicos de atômicos de C++.