Proyecto final: una difusión de datos de mercado sin cerrojos con pruebas de sus invariantes

El proyecto final es una difusión: un productor publica ticks de SPY y varios consumidores los leen todos, sin ningún cerrojo. Todo lo que ha construido se junta aquí. Una cola que solo mueve el productor, un cursor privado por consumidor para que nadie compita, un orden de escritura que decide lo que puede ver un lector y un explorador que convierte «parece funcionar» en una afirmación sobre cada planificación.

El flujo es un registro que solo crece. La posición p contiene tick<p> y tail dice cuántas posiciones están publicadas. Solo el productor escribe ticks y la cola, así que no hay nada que disputar en su lado. Cada consumidor posee un cursor, la siguiente posición que leerá, y nadie más lo escribe. Ese es todo el truco de una difusión: los consumidores nunca escriben nada que los otros lean, así que añadir un consumidor no cuesta nada a los demás. El único hecho compartido es la cola, y la única pregunta es en qué orden escribe el productor el tick y mueve la cola. Si la mueve después de los datos, un lector que ve la nueva cola encuentra los datos. Si la mueve antes, un lector puede ver una posición aún no 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}

Un sondeo toma dos turnos. El primero lee la cola. El segundo lee el cursor del consumidor y, si el cursor está por detrás de la cola, lee el tick, avanza el cursor y anota lo que obtuvo. Nada puede cambiar la posición bajo sus pies, porque solo este consumidor escribe su cursor. Lo que puede fallar es el contenido del tick: un lector que entra tras mover la cola pero antes de que lleguen los datos no lee nada. El sondeo lo anota como None, para que el comprobador lo vea.

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}

¿Qué significa «correcto» para el flujo? Tres afirmaciones sobre el estado final. Roto: cada tick recibido por un consumidor es igual al tick puesto en esa posición (un tick ausente recibido como None está roto). Hueco: cada consumidor recibió las posiciones 0, 1, 2, ... sin huecos. Desbordamiento: ningún cursor está más allá de la cola. verify explora cada planificación de un productor y los consumidores y cuenta las que rompen cada una. El explorador es la prueba: no puede muestrear la ejecución afortunada, las 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}

El mismo programa, 3150 planificaciones, y un solo cambio de orden de dos líneas convierte «ninguna rota» en 869 rotas. La mayoría son planificaciones que unos miles de ejecuciones de prueba casi nunca alcanzarían. Ese es el argumento para explorar en vez de probar, y es toda la habilidad en una tabla: un modelo lo bastante pequeño para enumerarlo, un comprobador de invariantes y un veredicto sobre cada planificación.

El laboratorio sigue la lección: el flujo vacío, el productor en sus dos órdenes, el sondeo del consumidor, el comprobador de los tres invariantes, el verificador que explora todas las planificaciones, una repetición de una ejecución tranquila en la que cada consumidor recibe los ticks en orden y el estudio sobre cierres de SPY.

• Función · preguntaSe apoya en
• make_feed(consumers)¿Qué se comparte?Aritmética simple
• publish(shared, tick, safe)Datos primero o cola primeroAritmética simple
• poll(shared, c)El siguiente tick del consumidor cAritmética simple
• violations(final)¿Qué invariantes se rompieron?Aritmética simple
• verify(ticks, polls, safe)¿Es correcto el flujo bajo todas las planificaciones?explore_allviolations
• drain(ticks, polls)¿Qué recibe cada consumidor?run_prefix
• study(bars)Seguro, inseguro y tranquilo en SPYverifydrain

Con esto termina la habilidad sin cerrojos. Ya sabe construir las piezas (atómicos, compare-and-swap, pilas y colas), nombrar los peligros (carreras, ABA, recuperación) y, sobre todo, comprobar un diseño contra cada planificación en lugar de fiarse de una ejecución que pasó por casualidad. El siguiente paso es la misma disciplina en hardware real, en los temas de atómicos de C++.