Le modèle mémoire : acquire et release

Un processeur peut exécuter deux lectures et écritures indépendantes dans l'un ou l'autre ordre, et un autre cœur peut voir le résultat de ce choix. Publiez un prix SPY puis levez un drapeau : un lecteur qui voit le drapeau peut quand même lire un prix de 0. Sur les quatre façons d'ordonner l'écrivain et le lecteur, une seule est sûre : release côté écrivain associé à acquire côté lecteur.

Les tampons d'écriture, les caches et le compilateur laissent tous un cœur terminer une écriture ou une lecture postérieure avant une antérieure, tant qu'un seul thread ne peut pas le voir. Un autre thread le peut. Notre machine le modélise directement : un thread est une liste d'opérations, et il peut exécuter, dans n'importe quel ordre, toute opération dont les contraintes d'ordre sont satisfaites. Les opérations sur la même adresse gardent toujours leur ordre, sinon un thread ne verrait pas ses propres écritures. Un chargement acquire bloque tout ce qui suit ; une écriture release attend tout ce qui précède. Deux fonctions disent tout : must_wait liste ce qu'une opération attend, et eligible liste ce qui peut s'exécuter ensuite.

def must_wait(ops, j):    waits = []    for i in range(j):        same = ops[i][1] == ops[j][1]        after_acquire = ops[i][0] == "load" and ops[i][3] == "acquire"        release = ops[j][0] == "store" and ops[j][3] == "release"        if same or after_acquire or release:            waits.append(i)    return waitsdef eligible(ops, done):    return [j for j in range(len(ops)) if j not in done and all(i in done for i in must_wait(ops, j))]writer = [("store", "data", 1, "relaxed"), ("store", "flag", 1, "release")]reader = [("load", "flag", "r1", "acquire"), ("load", "data", "r2", "relaxed")]print(must_wait(writer, 1), eligible(writer, set()), eligible(writer, {0}))print(must_wait(reader, 1), eligible(reader, set()))print(eligible([("load", "flag", "r1", "relaxed"), ("load", "data", "r2", "relaxed")], set()))

[0] [0] [1]
[0] [0]
[0, 1]

L'écriture release du drapeau attend la position 0, l'écriture des données, donc l'écrivain ne peut exécuter ses opérations que dans l'ordre. Le chargement acquire du drapeau bloque le chargement des données qui le suit, donc le lecteur s'exécute aussi dans l'ordre. Avec des chargements simples, les deux sont éligibles à la fois et le lecteur peut lire les données en premier.

outcomes est l'explorateur des sujets précédents pour cette nouvelle machine. Un état, c'est quelles opérations chaque thread a faites, la mémoire et les registres. À partir d'un état, il essaie chaque opération éligible de chaque thread, et quand il ne reste rien à exécuter les registres forment un résultat. Comme beaucoup d'ordres mènent au même état, il mémorise les états déjà vus. Le test de passage de message publie avec deux écritures, les données puis le drapeau, et consomme avec deux chargements, le drapeau puis les données. Le consommateur a tort quand il voit r1 == 1 (le drapeau) et r2 == 0 (pas encore de données), ce que vérifie reads_stale.

def outcomes(programs, memory=None):    found = set()    seen = set()    def visit(done, mem, regs):        state = (tuple(frozenset(d) for d in done), tuple(sorted(mem.items())), tuple(sorted(regs.items())))        if state in seen:            return        seen.add(state)        moved = False        for tid, ops in enumerate(programs):            for j in eligible(ops, done[tid]):                moved = True                kind, address, x, _ = ops[j]                mem2, regs2 = dict(mem), dict(regs)                if kind == "store":                    mem2[address] = x                else:                    regs2[x] = mem.get(address, 0)                done2 = [set(d) for d in done]                done2[tid].add(j)                visit(done2, mem2, regs2)        if not moved:            found.add(tuple(sorted(regs.items())))    visit([set() for _ in programs], dict(memory or {}), {})    return founddef mp_programs(write_order, read_order):    return [        [("store", "data", 1, "relaxed"), ("store", "flag", 1, write_order)],        [("load", "flag", "r1", read_order), ("load", "data", "r2", "relaxed")],    ]def reads_stale(results):    return any(dict(outcome).get("r1") == 1 and dict(outcome).get("r2") == 0 for outcome in results)for pair in (("relaxed", "relaxed"), ("release", "acquire")):    results = outcomes(mp_programs(*pair))    print(pair, sorted(results), "stale:", reads_stale(results))

('relaxed', 'relaxed') [(('r1', 0), ('r2', 0)), (('r1', 0), ('r2', 1)), (('r1', 1), ('r2', 0)), (('r1', 1), ('r2', 1))] stale: True
('release', 'acquire') [(('r1', 0), ('r2', 0)), (('r1', 0), ('r2', 1)), (('r1', 1), ('r2', 1))] stale: False

Avec des ordres relaxed, le consommateur peut finir avec les quatre paires (r1, r2), y compris (1, 0), la périmée. Avec release sur l'écriture du drapeau et acquire sur son chargement, il n'en reste que trois : le lecteur qui voit le drapeau voit aussi les données, car aucun des deux côtés ne peut être réordonné de part et d'autre du drapeau.

Un seul côté suffit-il ? Essayons les quatre paires. Release seul côté écrivain échoue : le lecteur peut charger les données avant le drapeau. Acquire seul côté lecteur échoue : l'écrivain peut ranger le drapeau avant les données. Seule la paire fonctionne, ce que montre le tableau ci-dessous. C'est le contrat release-acquire de std::atomic en C++ et de Rust, et la raison pour laquelle une file sans verrou publie une case par une écriture release d'un indice et la lit par un chargement acquire.

PAIRS = [("relaxed", "relaxed"), ("release", "relaxed"), ("relaxed", "acquire"), ("release", "acquire")]def ordering_table():    return {pair: reads_stale(outcomes(mp_programs(*pair))) for pair in PAIRS}for pair, stale in ordering_table().items():    print("write", pair[0], "| read", pair[1], "->", "can read stale data" if stale else "safe")

write relaxed | read relaxed -> can read stale data
write release | read relaxed -> can read stale data
write relaxed | read acquire -> can read stale data
write release | read acquire -> safe

price = int(round(float(load_bars()["close"].iloc[0]) * 100))programs = mp_programs("release", "acquire")programs[0][0] = ("store", "data", price, "relaxed")print(price, sorted(outcomes(programs)))

9369 [(('r1', 0), ('r2', 0)), (('r1', 0), ('r2', 9369)), (('r1', 1), ('r2', 9369))]

Avec le premier cours de clôture de SPY, 9 369 cents, le lecteur peut voir le drapeau et un prix de 0 dans trois des quatre configurations. Un bug de ce genre passe tous les tests sur une machine qui garde l'ordre, et apparaît sur une autre. C'est pourquoi la paire sûre doit être prouvée sur tous les ordres permis, comme le fait l'explorateur.

Le labo suit le cours : ce qu'une opération doit attendre, quelles opérations peuvent s'exécuter ensuite, tous les résultats d'un ensemble de threads, le test de passage de message, la vérification des données périmées, le tableau des quatre ordres et l'étude qui publie un vrai prix SPY.

• Fonction · questionS'appuie sur
• must_wait(ops, j)Qu'est-ce que cette opération doit attendre ?De l'arithmétique simple
• eligible(ops, done)Quelles opérations peuvent passer ensuite ?De l'arithmétique simple
• outcomes(programs, memory)Avec quoi les threads peuvent-ils finir ?eligible
• mp_programs(write_order, read_order)À quoi ressemble le passage de message ?De l'arithmétique simple
• reads_stale(results)Le lecteur peut-il voir le drapeau sans les données ?De l'arithmétique simple
• ordering_table()Quelles paires d'ordres sont sûres ?outcomesmp_programs
• study(bars)Quelles paires protègent un vrai prix SPY ?outcomesmp_programs

Sujet suivant : vous avez maintenant les outils pour bâtir une structure sans verrou et un vocabulaire pour décrire ce qu'elle garantit. Les garanties de progression nomment les trois niveaux, sans obstruction, sans verrou et sans attente, et testent chaque compteur que vous avez écrit contre un thread mis en pause pour toujours au pire moment.