最简单的无锁队列根本不需要比较并交换。让每个位置只有一个写者:只有生产者写 tail,只有消费者写 head。对另一侧位置读到旧值永远是安全的,因此环形缓冲区可以不加锁地在两个线程间传递 tick。探索器在 291 种调度上证明了这一点,并显示一旦加入第二个生产者,1,072 种调度中有 458 种会出错。
每个位置只有一个写者的环
环形缓冲区有两个只增不减的计数器。生产者写槽位 tail % capacity,然后通过增大 tail 来发布;消费者读槽位 head % capacity,然后通过增大 head 来释放它。tail - head == capacity 时缓冲区满,head == tail 时为空。为什么不加锁也安全?生产者是 tail 的唯一写者,所以可以在局部变量里留一份副本。它读 head 来找空位,即使读到的值过期了,过期的 head 比真实的小,生产者只会误以为缓冲区更满,最坏丢弃一个元素,绝不会覆盖未读的槽位。消费者读到的过期 tail 也偏小,最坏只是看到缓冲区为空。这就是单写者原则。
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}生产者的三个回合推入第一个 tick:读 head,把元素存进 slot0,发布 tail: 1。消费者三个回合之后,head: 1、popped: (7,)。最后一行里生产者已推入两个元素(slot0: 7、slot1: 8),消费者取走了第一个;线程 1 还活着,因为它还剩一次尝试。
在所有调度上检查不变量
队列必须承诺什么?两件事。取出的元素就是放入的元素,顺序相同且没有空缺:popped 是 pushed 的前缀(FIFO 性质)。并且不会取出从未放入的东西:len(popped) <= len(pushed)。线程在完成操作的那个回合里记录自己放入和取出了什么,所以 violations 可以在任何终态上检查这两条。然后 verify 用 explore_all 在每种调度下运行整个程序,统计破坏每条不变量的调度数。所有调度下 broken 都为空,就是对该规模程序的证明。
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}两个元素的生产者推入两个槽位的缓冲区,由尝试两次的消费者读取,共有 101 种调度,没有一种破坏不变量。只有一个槽位时,消费者慢的话生产者必须丢弃一个元素,但仍然是正确的:25 种调度,没有违例。在 (7, 8) 已推入之后取出 (8,),正如预期,是顺序违例。
每个共享变量恰好只有一个线程写它,读它的线程可以任意多。只有一个写者,该变量上就没有竞态;读到旧值的读者只要旧值只会偏向安全一侧,就依然安全。
什么会破坏它:第二个生产者
安全性的论证依赖一个事实:tail 只有一个写者。加入第二个生产者,两个线程各自保存自己对 tail 的认识。两者读到同一个 head,算出同一个槽位,后一次写入覆盖前一次。探索器找到了它:两个生产者(各推一个 tick)的 1,072 种调度中,有 458 种以不是 pushed 前缀的 popped 结束。补救办法不是给这个环打补丁,而是换另一种结构,也就是后面几个主题用比较并交换构建的多生产者队列。
print(verify([(7,), (8,)], 2, 2)){'schedules': 1072, 'broken': {'order': 458}, 'pushed': 2, 'popped': 1}这台机器按顺序执行每个操作。在真实处理器上,生产者必须用 release 存储发布 tail,消费者必须用 acquire 加载读它,否则消费者可能先看到新的 tail、后看到元素(上一个主题里的过期数据)。还要把 head 和 tail 放在不同的缓存行上,否则两个线程会争抢同一行(伪共享)。
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}整个教训就在两个数里:每个位置一个写者,在 291 种调度上都正确;同一位置有两个写者,则在 1,072 种调度的 43% 上出错。探索器不是猜的,而是跑了每一种交错。
你要实现什么
实验沿着本讲走:空环、生产者和消费者线程、对两条不变量的检查、运行探索器的验证函数,以及用一个和两个生产者把 SPY 收盘价送过环形缓冲区的研究。
- 函数 · 问题依赖
- initial_state()空环是什么样子?简单算术
- ring_producer(items, capacity)生产者如何推入?简单算术
- ring_consumer(attempts, capacity)消费者如何取出?简单算术
- violations(final)这个状态破坏了哪些不变量?简单算术
- verify(producers, attempts, capacity)环在所有调度下都正确吗?explore_allviolations
- study(bars)有第二个生产者时什么会出错?verify
下一个主题:单写者的技巧有局限,比较并交换也有。ABA 问题与带标签指针会基于比较并交换构建一个无锁栈,展示一种调度:栈在下面已经变了,交换却成功了;然后用版本标签修复它。
实验:评分内容
6 个任务 · 100 分- 空环5 分
- 生产者20 分
- 消费者20 分
- 不变量10 分
- 在所有调度上验证15 分
- 基于 SPY 表的研究30 分