Un búfer circular de un productor y un consumidor

La cola sin cerrojos más simple no necesita comparar e intercambiar en absoluto. Dé a cada posición un solo escritor: solo el productor escribe la cola, solo el consumidor escribe la cabeza. Una lectura obsoleta de la posición del otro lado es siempre segura, así que un búfer circular puede pasar ticks entre dos hilos sin cerrojo. El explorador lo demuestra sobre 291 planificaciones, y lo muestra fallando en 458 de 1072 cuando se une un segundo productor.

Un búfer circular mantiene dos contadores que solo crecen. El productor escribe la casilla tail % capacity y luego publica subiendo tail; el consumidor lee la casilla head % capacity y luego la libera subiendo head. El búfer está lleno cuando tail - head == capacity y vacío cuando head == tail. ¿Por qué es seguro sin cerrojo? El productor es el único escritor de tail, así que puede guardar su propia copia local. Lee head para buscar espacio y, si ese valor está obsoleto, la cabeza obsoleta es menor que la real, así que el productor cree el búfer más lleno de lo que está y, como mucho, descarta un elemento, sin sobrescribir nunca una casilla sin leer. La tail obsoleta del consumidor también es menor, así que como mucho ve el búfer vacío. Es el principio de escritor único.

def initial_state():    return {"head": 0, "tail": 0, "pushed": (), "popped": ()}def ring_producer(items, capacity):    def thread(shared):        tail = 0        for item in items:            yield            head = shared.get("head", 0)            if tail - head < capacity:                yield                shared["slot%d" % (tail % capacity)] = item                yield                tail += 1                shared["tail"] = tail                shared["pushed"] = shared.get("pushed", ()) + (item,)    return threaddef ring_consumer(attempts, capacity):    def thread(shared):        head = 0        for _ in range(attempts):            yield            tail = shared.get("tail", 0)            if head != tail:                yield                item = shared.get("slot%d" % (head % capacity))                yield                head += 1                shared["head"] = head                shared["popped"] = shared.get("popped", ()) + (item,)    return threadtwo = lambda shared: [ring_producer((7, 8), 2)(shared), ring_consumer(2, 2)(shared)]for prefix in ([0, 0, 0], [0, 0, 0, 1, 1, 1], [0, 0, 0, 0, 0, 0, 1, 1, 1, 1]):    print(prefix, run_prefix(two, prefix, initial_state())[0])

[0, 0, 0] {'head': 0, 'tail': 1, 'pushed': (7,), 'popped': (), 'slot0': 7}
[0, 0, 0, 1, 1, 1] {'head': 1, 'tail': 1, 'pushed': (7,), 'popped': (7,), 'slot0': 7}
[0, 0, 0, 0, 0, 0, 1, 1, 1, 1] {'head': 1, 'tail': 2, 'pushed': (7, 8), 'popped': (7,), 'slot0': 7, 'slot1': 8}

Tres turnos del productor empujan el primer tick: lee la cabeza, guarda el elemento en slot0 y publica tail: 1. Tras tres turnos del consumidor, head: 1 y popped: (7,). En la última línea el productor ha empujado ambos elementos (slot0: 7, slot1: 8) y el consumidor ha tomado el primero; el hilo 1 sigue vivo porque le queda un intento.

¿Qué debe prometer una cola? Dos cosas. Los elementos sacados son los elementos metidos, en el mismo orden y sin huecos: popped es un prefijo de pushed (la propiedad FIFO). Y no se saca nada que nunca se metió: len(popped) <= len(pushed). Los hilos registran lo que meten y sacan en el mismo turno que termina la operación, así que violations puede comprobar ambas en cualquier estado final. verify ejecuta entonces todo el programa bajo cada planificación con explore_all y cuenta las planificaciones que rompen cada invariante. Un diccionario broken vacío sobre todas las planificaciones es una demostración, para ese tamaño de programa.

def violations(final):    pushed, popped = tuple(final.get("pushed", ())), tuple(final.get("popped", ()))    broken = []    if popped != pushed[: len(popped)]:        broken.append("order")    if len(popped) > len(pushed):        broken.append("count")    return sorted(broken)def verify(producers, attempts, capacity):    def make_threads(shared):        return [ring_producer(items, capacity)(shared) for items in producers] + [ring_consumer(attempts, capacity)(shared)]    outcomes = explore_all(make_threads, initial_state())    broken = {}    pushed = popped = 0    for key, count in outcomes.items():        final = dict(key)        pushed = max(pushed, len(final.get("pushed", ())))        popped = max(popped, len(final.get("popped", ())))        for name in violations(final):            broken[name] = broken.get(name, 0) + count    return {"schedules": sum(outcomes.values()), "broken": dict(sorted(broken.items())), "pushed": pushed, "popped": popped}print(violations({"pushed": (7, 8), "popped": (8,)}))print(verify([(7, 8)], 2, 2))print(verify([(7, 8)], 2, 1))

['order']
{'schedules': 101, 'broken': {}, 'pushed': 2, 'popped': 2}
{'schedules': 25, 'broken': {}, 'pushed': 2, 'popped': 2}

Un productor con dos elementos en un búfer de dos casillas, leído por un consumidor con dos intentos, tiene 101 planificaciones y ninguna rompe un invariante. Con un búfer de una sola casilla el productor tiene que descartar un elemento cuando el consumidor es lento, pero sigue siendo correcto: 25 planificaciones, ninguna violación. La lista sacada (8,) tras empujar (7, 8) es, como se espera, una violación del orden.

El argumento de seguridad se apoya en un hecho: tail tiene un escritor. Añada un segundo productor y dos hilos mantienen cada uno su idea de la cola. Ambos leen el mismo head, calculan la misma casilla y la segunda escritura sobrescribe la primera. El explorador lo encuentra: 458 de las 1072 planificaciones de dos productores (un tick cada uno) terminan con un popped que no es prefijo de pushed. La solución no es un parche de este búfer sino otra estructura, una cola de varios productores, que los temas siguientes construyen con comparar e intercambiar.

print(verify([(7,), (8,)], 2, 2))

{'schedules': 1072, 'broken': {'order': 458}, 'pushed': 2, 'popped': 1}

ticks = [int(round(float(c) * 100)) for c in load_bars()["close"].iloc[:4]]print(ticks)print("one producer: ", verify([ticks[:2]], 3, 2))print("two producers:", verify([ticks[:1], ticks[1:2]], 2, 2))

[9369, 9305, 9354, 9349]
one producer:  {'schedules': 291, 'broken': {}, 'pushed': 2, 'popped': 2}
two producers: {'schedules': 1072, 'broken': {'order': 458}, 'pushed': 2, 'popped': 1}

Toda la lección cabe en dos números: un escritor por posición basta para la corrección en 291 planificaciones, y dos escritores en la misma posición fallan en el 43 % de 1072. El explorador no adivinó; ejecutó todos los intercalados.

El laboratorio sigue la lección: el búfer vacío, los hilos productor y consumidor, la comprobación de los dos invariantes, el verificador que lanza el explorador y el estudio que envía cierres de SPY por el búfer con uno y con dos productores.

• Función · preguntaSe apoya en
• initial_state()¿Cómo es un búfer vacío?Aritmética simple
• ring_producer(items, capacity)¿Cómo empuja el productor?Aritmética simple
• ring_consumer(attempts, capacity)¿Cómo saca el consumidor?Aritmética simple
• violations(final)¿Qué invariantes rompe este estado?Aritmética simple
• verify(producers, attempts, capacity)¿Es correcto el búfer bajo todas las planificaciones?explore_allviolations
• study(bars)¿Qué se rompe con un segundo productor?verify

Siguiente tema: el truco del escritor único tiene un límite, y comparar e intercambiar también. El problema ABA y los punteros etiquetados construye una pila sin cerrojos sobre comparar e intercambiar, muestra una planificación en la que el intercambio tiene éxito aunque la pila haya cambiado por debajo, y lo repara con una etiqueta de versión.