Probar código concurrente: detectores de carreras y verificación de modelos

Ejecutar todas las planificaciones demuestra un programa pequeño, pero cuesta el número de intercalados. Las herramientas reales toman dos atajos. Un detector de carreras observa una ejecución e informa de las variables que podrían competir en otra planificación. Un verificador de modelos recuerda los estados vistos. Para dos hilos de 10 pasos son 184 756 planificaciones frente a 121 estados.

Un detector de carreras no ejecuta hilos. Lee una traza: cada lectura y escritura de datos compartidos y cada adquisición y liberación de un cerrojo. Nuestros programas se convierten en listas de esas operaciones, y interleave convierte un programa y una planificación en la traza de esa ejecución. Dos hilos que leen y escriben x cada uno sin cerrojo dan los cuatro eventos siguientes. En esta planificación el hilo 0 termina antes de que empiece el hilo 1, así que una prueba vería la respuesta correcta. La pregunta del detector es otra: ¿podrían haberse solapado los dos hilos?

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

El primer detector usa una disciplina: toda variable compartida debería estar guardada por algún cerrojo que se tenga en cada acceso. La regla del lockset sigue los cerrojos que tiene cada hilo y, para cada variable, interseca los conjuntos de cerrojos tenidos en sus accesos. Si al menos dos hilos tocaron la variable, uno la escribió y la intersección es vacía, ningún cerrojo único la protege: se informa de una carrera potencial. El contador sin cerrojo se marca; el que tiene cerrojo, no. La regla es barata y puede dar una falsa alarma. En el traspaso siguiente el hilo 0 escribe x y luego se lo pasa al hilo 1 por el cerrojo. No había ningún cerrojo tenido en la escritura, así que la regla protesta, aunque los accesos en realidad están 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']

El segundo detector hace la pregunta exacta: ¿hay una cadena de órdenes desde el primer acceso al segundo? Existen dos tipos de arista, el orden dentro de un hilo y la pareja liberación y luego adquisición del mismo cerrojo. La relación happens-before es la clausura de ambas. Un reloj vectorial por hilo registra lo que el hilo ha visto; una liberación guarda el reloj en el cerrojo y una adquisición toma el máximo componente a componente con él. Un acceso es una carrera si un acceso anterior en conflicto de otro hilo tiene una época que el reloj actual no ha visto. En el traspaso, la liberación y la adquisición conectan la escritura con la lectura, así que no hay carrera. Solo informa de carreras reales, pero solo en los accesos que observó.

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

Un verificador de modelos visita el mismo programa, pero recuerda estados. En nuestros programas un estado es solo cuánto ha avanzado cada hilo, así que con hilos de n pasos hay (n1 + 1) × (n2 + 1) × ... estados, sean cuantas sean las planificaciones que llevan a ellos. Los hilos contadores siguientes dan las cifras para los datos reales, con las planificaciones y los 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

Una sola traza serie basta a los dos detectores para encontrar el cerrojo que falta, y el programa con cerrojo está limpio. La ventaja del verificador de modelos sobre la fuerza bruta es el factor entre 1820 y 65, y crece sin límite: para 10 y 10 pasos son 184 756 frente a 121. Por eso la verificación de modelos puede cubrir programas que la enumeración simple nunca alcanzaría, mientras un detector de carreras cuesta una pasada sobre una ejecución.

El laboratorio sigue la lección: la traza de una ejecución, la regla del lockset, la regla happens-before con relojes vectoriales, el recuento de estados, los programas de los hilos contadores y el estudio de ambos detectores y ambos tamaños de espacio sobre los días de subida de SPY.

• Función · preguntaSe apoya en
• interleave(programs, schedule)¿Qué pasó y en qué orden?Aritmética simple
• lockset_races(trace)¿Qué variables no tienen cerrojo común?Aritmética simple
• hb_races(trace)¿Qué variables tienen accesos sin orden?Aritmética simple
• count_states(lengths)¿Cuántos estados hay que recordar?Aritmética simple
• counter_programs(ups, locked)¿Qué hacen los hilos contadores?Aritmética simple
• study(bars)¿Coinciden los detectores en SPY?counter_programsinterleavelockset_raceshb_racescount_states

Siguiente tema: el código sin cerrojos tiene un peligro más que ningún detector ni verificador puede arreglar a posteriori: cuando un hilo libera un nodo que otro hilo aún está leyendo. Los punteros de peligro y la recuperación por épocas construyen las dos formas clásicas de liberar memoria con seguridad, y el explorador muestra un uso tras liberar bajo cada planificación que no haya impedido.