Un tampon circulaire à un producteur et un consommateur

La file sans verrou la plus simple n'a pas besoin de comparer-et-échanger. Donnez à chaque position un seul écrivain : le producteur seul écrit la queue, le consommateur seul écrit la tête. Une lecture périmée de la position de l'autre côté est toujours sûre, donc un tampon circulaire peut passer des ticks entre deux threads sans verrou. L'explorateur le prouve sur 291 ordonnancements, et le montre en défaut dans 458 des 1 072 dès qu'un second producteur s'ajoute.

Un tampon circulaire garde deux compteurs qui ne font que croître. Le producteur écrit la case tail % capacity puis publie en augmentant tail ; le consommateur lit la case head % capacity puis la libère en augmentant head. Le tampon est plein quand tail - head == capacity et vide quand head == tail. Pourquoi est-ce sûr sans verrou ? Le producteur est le seul écrivain de tail, il peut donc en garder une copie locale. Il lit head pour chercher de la place, et si cette valeur est périmée, la tête périmée est plus petite que la vraie, donc le producteur croit le tampon plus plein qu'il ne l'est et, au pire, abandonne un élément, sans jamais écraser une case non lue. La tail périmée du consommateur est elle aussi plus petite, donc au pire il voit le tampon vide. C'est le principe de l'écrivain unique.

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}

Trois tours du producteur poussent le premier tick : il lit la tête, range l'élément dans slot0 et publie tail: 1. Après trois tours du consommateur, head: 1 et popped: (7,). Sur la dernière ligne, le producteur a poussé les deux éléments (slot0: 7, slot1: 8) et le consommateur a pris le premier ; le thread 1 est encore vivant car il lui reste une tentative.

Que doit promettre une file ? Deux choses. Les éléments sortis sont les éléments entrés, dans le même ordre et sans trou : popped est un préfixe de pushed (propriété FIFO). Et rien n'est sorti qui n'ait été poussé : len(popped) <= len(pushed). Les threads consignent ce qu'ils poussent et sortent au tour même qui termine l'opération, si bien que violations peut vérifier les deux sur n'importe quel état final. verify exécute alors tout le programme sous chaque ordonnancement avec explore_all et compte les ordonnancements qui violent chaque invariant. Un dictionnaire broken vide sur tous les ordonnancements est une preuve, pour cette taille de programme.

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 producteur de deux éléments dans un tampon de deux cases, lu par un consommateur à deux tentatives, a 101 ordonnancements et aucun ne viole d'invariant. Avec un tampon d'une seule case, le producteur doit abandonner un élément quand le consommateur est lent, mais il reste correct : 25 ordonnancements, aucune violation. La liste sortie (8,) après que (7, 8) a été poussé est bien une violation de l'ordre.

L'argument de sûreté repose sur un fait : tail a un seul écrivain. Ajoutez un second producteur et deux threads gardent chacun leur idée de la queue. Tous deux lisent le même head, calculent la même case, et la seconde écriture écrase la première. L'explorateur le trouve : 458 des 1 072 ordonnancements de deux producteurs (un tick chacun) finissent avec un popped qui n'est pas un préfixe de pushed. Le remède n'est pas un correctif de ce tampon mais une autre structure, une file multi-producteurs, que les sujets suivants bâtissent avec comparer-et-échanger.

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}

Toute la leçon tient en deux nombres : un écrivain par position suffit à la justesse sur 291 ordonnancements, et deux écrivains sur la même position se trompent dans 43 % de 1 072. L'explorateur n'a pas deviné ; il a exécuté tous les entrelacements.

Le labo suit le cours : le tampon vide, les threads producteur et consommateur, la vérification des deux invariants, le vérificateur qui lance l'explorateur et l'étude qui envoie des cours de clôture SPY dans le tampon avec un puis deux producteurs.

• Fonction · questionS'appuie sur
• initial_state()À quoi ressemble un tampon vide ?De l'arithmétique simple
• ring_producer(items, capacity)Comment le producteur pousse-t-il ?De l'arithmétique simple
• ring_consumer(attempts, capacity)Comment le consommateur sort-il ?De l'arithmétique simple
• violations(final)Quels invariants cet état viole-t-il ?De l'arithmétique simple
• verify(producers, attempts, capacity)Le tampon est-il juste sous tous les ordonnancements ?explore_allviolations
• study(bars)Qu'est-ce qui casse avec un second producteur ?verify

Sujet suivant : l'astuce de l'écrivain unique a une limite, et le comparer-et-échanger aussi. Le problème ABA et les pointeurs étiquetés bâtit une pile sans verrou sur comparer-et-échanger, montre un ordonnancement où l'échange réussit alors que la pile a changé en dessous, et le répare avec une étiquette de version.