Tester le code concurrent : détecteurs de courses et vérification de modèles

Exécuter tous les ordonnancements prouve un petit programme, mais cela coûte le nombre d'entrelacements. Les vrais outils prennent deux raccourcis. Un détecteur de courses observe une exécution et signale les variables qui pourraient se heurter dans un autre ordonnancement. Un vérificateur de modèles retient les états déjà vus. Pour deux threads de 10 étapes, c'est 184 756 ordonnancements contre 121 états.

Un détecteur de courses n'exécute pas de threads. Il lit une trace : chaque lecture et écriture de données partagées, chaque acquisition et libération d'un verrou. Nos programmes deviennent des listes de telles opérations, et interleave transforme un programme et un ordonnancement en la trace de cette exécution. Deux threads qui lisent et écrivent chacun x sans verrou donnent les quatre événements ci-dessous. Dans cet ordonnancement le thread 0 finit avant que le thread 1 commence, si bien qu'un test verrait la bonne réponse. La question du détecteur est autre : les deux threads auraient-ils pu se chevaucher ?

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

Le premier détecteur applique une discipline : toute variable partagée devrait être gardée par un verrou tenu à chaque accès. La règle du lockset suit les verrous que chaque thread détient et, pour chaque variable, fait l'intersection des ensembles de verrous détenus lors de ses accès. Si au moins deux threads ont touché la variable, que l'un l'a écrite et que l'intersection est vide, aucun verrou unique ne la protège : on signale une course potentielle. Le compteur sans verrou est signalé ; celui avec verrou ne l'est pas. La règle est bon marché et peut donner une fausse alerte. Dans le passage de témoin ci-dessous, le thread 0 écrit x puis le transmet au thread 1 par le verrou. Aucun verrou n'était tenu lors de l'écriture, donc la règle proteste, alors que les accès sont en fait ordonnés.

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

Le second détecteur pose la question exacte : existe-t-il une chaîne d'ordonnancements du premier accès au second ? Il existe deux sortes d'arêtes, l'ordre à l'intérieur d'un thread et la paire libération puis acquisition du même verrou. La relation happens-before est la fermeture des deux. Une horloge vectorielle par thread enregistre ce que le thread a vu ; une libération range l'horloge dans le verrou et une acquisition prend le maximum point par point avec elle. Un accès est une course si un accès antérieur conflictuel d'un autre thread a une époque que l'horloge courante n'a pas vue. Dans le passage de témoin, la libération et l'acquisition relient l'écriture à la lecture, donc pas de course. Il ne signale que les vraies courses, mais seulement dans les accès qu'il a observés.

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 vérificateur de modèles visite le même programme mais retient les états. Dans nos programmes un état est seulement l'avancement de chaque thread, donc avec des threads de n étapes il y a (n1 + 1) × (n2 + 1) × ... états, quel que soit le nombre d'ordonnancements qui y mènent. Les threads compteurs ci-dessous donnent les chiffres pour les vraies données, avec les ordonnancements et les états côte à côte.

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

Une seule trace en série suffit aux deux détecteurs pour trouver le verrou manquant, et le programme avec verrou est propre. L'avantage du vérificateur de modèles sur la force brute est le facteur entre 1 820 et 65, et il croît sans limite : pour 10 et 10 étapes, c'est 184 756 contre 121. C'est pourquoi la vérification de modèles peut couvrir des programmes que l'énumération simple n'atteindrait jamais, alors qu'un détecteur de courses coûte un passage sur une exécution.

Le labo suit le cours : la trace d'une exécution, la règle du lockset, la règle happens-before avec horloges vectorielles, le décompte des états, les programmes des threads compteurs, et l'étude des deux détecteurs et des deux tailles d'espace sur les jours de hausse de SPY.

• Fonction · questionS'appuie sur
• interleave(programs, schedule)Que s'est-il passé, dans quel ordre ?De l'arithmétique simple
• lockset_races(trace)Quelles variables n'ont aucun verrou commun ?De l'arithmétique simple
• hb_races(trace)Quelles variables ont des accès non ordonnés ?De l'arithmétique simple
• count_states(lengths)Combien d'états faut-il retenir ?De l'arithmétique simple
• counter_programs(ups, locked)Que font les threads compteurs ?De l'arithmétique simple
• study(bars)Les détecteurs s'accordent-ils sur SPY ?counter_programsinterleavelockset_raceshb_racescount_states

Sujet suivant : le code sans verrou a un danger de plus qu'aucun détecteur ni vérificateur ne peut réparer après coup : quand un thread libère un nœud qu'un autre thread lit encore. Les pointeurs de danger et la récupération par époques bâtissent les deux façons classiques de libérer la mémoire en sûreté, et l'explorateur montre un usage après libération sous chaque ordonnancement que vous n'avez pas empêché.