Projet final : une diffusion de données de marché sans verrou avec preuves de ses invariants

Le projet final est une diffusion : un producteur publie des ticks SPY et plusieurs consommateurs les lisent tous, sans aucun verrou. Tout ce que vous avez construit se retrouve ici. Une queue que seul le producteur déplace, un curseur privé par consommateur pour que personne ne se dispute, un ordre d'écriture qui décide ce qu'un lecteur peut voir, et un explorateur qui transforme « ça a l'air de marcher » en énoncé sur chaque ordonnancement.

Le flux est un journal qui ne fait que grandir. La position p contient tick<p> et tail dit combien de positions sont publiées. Seul le producteur écrit les ticks et la queue, donc rien ne se dispute côté producteur. Chaque consommateur possède un curseur, la prochaine position qu'il lira, et personne d'autre ne l'écrit. C'est tout le truc d'une diffusion : les consommateurs n'écrivent jamais rien que les autres lisent, donc ajouter un consommateur ne coûte rien aux autres. Le seul fait partagé est la queue, et la seule question est dans quel ordre le producteur écrit le tick et déplace la queue. La déplacer après les données : un lecteur qui voit la nouvelle queue trouve les données. La déplacer avant : un lecteur peut voir une position pas encore écrite.

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 sondage prend deux tours. Le premier lit la queue. Le second lit le curseur du consommateur et, si le curseur est derrière la queue, lit le tick, avance le curseur et note ce qu'il a obtenu. Rien ne peut changer la position sous ses pieds, car seul ce consommateur écrit son curseur. Ce qui peut mal tourner, c'est le contenu du tick : un lecteur qui arrive après le déplacement de la queue mais avant l'arrivée des données ne lit rien. Le sondage le note None, pour que le vérificateur le voie.

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}

Que signifie « correct » pour le flux ? Trois énoncés sur l'état final. Déchiré : chaque tick reçu par un consommateur égale le tick mis à cette position (un tick manquant reçu comme None est déchiré). Trou : chaque consommateur a reçu les positions 0, 1, 2, ... sans trou. Dépassement : aucun curseur n'est au-delà de la queue. verify explore chaque ordonnancement d'un producteur et des consommateurs et compte ceux qui brisent chacun. L'explorateur est la preuve : il ne peut pas échantillonner l'exécution chanceuse, il les visite toutes.

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}

Le même programme, 3 150 ordonnancements, et une seule inversion de deux lignes fait passer de « aucun brisé » à 869 brisés. La plupart sont des ordonnancements que quelques milliers d'exécutions de test ne rencontreraient presque jamais. C'est l'argument pour explorer au lieu de tester, et c'est toute la compétence en un tableau : un modèle assez petit pour être énuméré, un vérificateur d'invariants et un verdict sur chaque ordonnancement.

Le labo suit le cours : le flux vide, le producteur dans ses deux ordres, le sondage du consommateur, le vérificateur des trois invariants, le vérificateur qui explore tous les ordonnancements, un rejeu d'une exécution calme où chaque consommateur reçoit les ticks dans l'ordre, et l'étude sur les clôtures SPY.

• Fonction · questionS'appuie sur
• make_feed(consumers)Qu'est-ce qui est partagé ?De l'arithmétique simple
• publish(shared, tick, safe)Données d'abord, ou queue d'abordDe l'arithmétique simple
• poll(shared, c)Le tick suivant du consommateur cDe l'arithmétique simple
• violations(final)Quels invariants sont brisés ?De l'arithmétique simple
• verify(ticks, polls, safe)Le flux est-il correct sous tous les ordonnancements ?explore_allviolations
• drain(ticks, polls)Que reçoit chaque consommateur ?run_prefix
• study(bars)Sûr, dangereux et calme sur SPYverifydrain

La compétence sans verrou est terminée. Vous savez construire les pièces (atomiques, compare-and-swap, piles et files), nommer les dangers (courses, ABA, récupération), et surtout vérifier une conception sur chaque ordonnancement au lieu de se fier à une exécution qui a réussi par hasard. L'étape suivante est la même discipline sur du vrai matériel, dans les sujets d'atomiques C++.