163 lines
12 KiB
Plaintext
163 lines
12 KiB
Plaintext
Q: Linearizability 解决什么问题？
|
||
|
||
A: 要解决的是对一致性模型的需求：即在面对多客户端并发请求、请求丢失与重传、通信延迟、服务器复制、服务器故障与恢复、以及服务器分片时，对网络服务在客户端可见行为上的正确性定义。一致性模型帮助程序员设计应用（客户端），使其表现出预期行为，也帮助服务设计者判断具体设计决策是否合适。
|
||
|
||
下面是一个 linearizability 能帮助回答的问题示例。假设有一个复制存储服务（如 GFS）。客户端 C1 对某 key 发送一次 write RPC 并收到 "success" 回复；之后客户端 C2 对同一 key 发送 read RPC 并收到一个值；没有其他客户端修改该 key；C2 是否保证能看到 C1 的写入？该问题的答案对存储服务设计很重要，因为它影响副本是否能服务读、服务器崩溃时更新是否必须保留、缓存是否必须严格保持最新等。
|
||
|
||
Linearizability 的答案是：是的，C2 必须看到 C1 的写入。因此，linearizable 的存储系统往往涉及复杂且昂贵的复制、崩溃恢复、缓存等管理。
|
||
|
||
Q: Linearizability 的定义是什么？
|
||
|
||
A: Linearizability 建立在“历史”（histories）上：即客户端操作的轨迹，并标注每个客户端操作开始（被客户端发起）的时间以及客户端认为该操作完成的时间。Linearizability 告诉你某条历史是否合法。若某服务能产生的每条历史都是 linearizable 的，我们就说该服务是 linearizable 的。
|
||
|
||
历史中有一个事件表示客户端开始某操作，另一个事件表示客户端认为该操作已完成。因此历史把客户端之间的并发和网络延迟显式化。通常开始和结束事件对应与服务器交换的请求和响应消息。
|
||
|
||
若你能为每个操作指定一个“线性化点”（linearization point）（一个时间），使得每个操作的点都落在其开始与结束事件之间，且历史的响应值与按这些点的顺序一次执行一个操作得到的结果相同，则该历史是 linearizable 的。若不存在满足这两条要求的线性化点分配，则该历史不是 linearizable 的。
|
||
|
||
Q: 为什么 linearizability 是理想的一致性模型？
|
||
|
||
A: 因为它相对“强”，即禁止许多可能给应用程序员带来问题的“异常”行为。一致性保证越强的服务，越容易让程序员据此设计。
|
||
|
||
例如，假设应用的一部分计算出一个值、写入存储系统，然后在存储系统中设置一个标志表示计算好的值已就绪：
|
||
|
||
v = compute...
|
||
put("value", v)
|
||
put("done", true)
|
||
|
||
在另一台机器上，程序检查 "done" 以判断值是否可用，若可用则使用：
|
||
|
||
if get("done") == true:
|
||
v = get("value")
|
||
print v
|
||
|
||
若实现 put() 和 get() 的存储系统是 linearizable 的，上述程序会按预期工作。
|
||
|
||
在许多较弱的一致性模型下，上述程序不会如人所愿。例如，提供“最终一致性”（eventual consistency）的存储系统可能重排两次 put（导致 "done" 为 true 而 "value" 尚不可用），或对某次 get() 返回陈旧（旧）值。
|
||
|
||
Q: 在试图证明某条历史是 linearizable 时，如何决定每个操作的线性化点放在哪里？
|
||
|
||
A: 思路是：为了说明某次执行是 linearizable 的，你（人）需要找到放置那些小橙线（线性化点）的位置。也就是说，要说明一条历史是 linearizable 的，需要找到一组线性化点（进而一个操作顺序）的分配，使其满足以下要求：
|
||
|
||
* 所有函数调用在从调用到响应之间的某个时刻都有一个线性化点。
|
||
|
||
* 所有函数在其线性化点处看起来是瞬时发生的，行为符合顺序定义。
|
||
|
||
因此，有些线性化点的放置是无效的，因为它们落在请求时间范围之外；另一些无效是因为违反了顺序定义（对 key/value 存储而言，违反即某次读没有观察到最近一次写入的值，其中“最近”指线性化点顺序）。
|
||
|
||
对复杂历史可能需尝试多种线性化点分配才能找到一种证明该历史是 linearizable 的。若全部尝试后仍无一种成立，则该历史不是 linearizable 的。
|
||
|
||
Q: 为什么不以客户端发送命令的时间作为线性化点？即让系统按客户端发送的顺序执行操作？
|
||
|
||
A: 很难构建保证这种行为的系统——开始时间是客户端代码发出请求的时间，但服务可能因网络延迟很久后才收到请求。也就是说，请求到达服务的顺序可能与开始时间的顺序大不相同。服务原则上可以延迟执行每个到达的请求，以防更早发出的请求稍后到达，但网络延迟无界，很难知道等待多久。而且这会增加每个请求的延迟，可能很多。话虽如此，我们后面会看的 Spanner 使用了相关技术。
|
||
|
||
像 linearizability 这样的正确性规范需要在“足够宽松以便高效实现”和“足够严格以便为应用程序提供有用保证”之间取得平衡。“看起来按调用顺序执行操作”过于严格难以高效实现，而 linearizability 的“看起来在调用与响应之间的某个时刻执行”是可实现的，尽管对应用程序员不如前者直观。
|
||
|
||
Q: 服务如何实现 linearizability？
|
||
|
||
A: 若服务以单台服务器实现，且无复制、无缓存、无内部并行，则服务按请求到达顺序一次执行一个客户端请求就几乎足够。一个复杂之处来自因认为网络丢包而重发请求的客户端：对有副作用的请求，服务必须确保每个客户端请求只执行一次。复制、容错和缓存会带来更多设计复杂度。
|
||
|
||
Linearizability 的一个好处是：服务在并发（时间上重叠）操作的执行顺序上有自由度。具体而言，若客户端 C1 和 C2 的操作并发，服务器可以先执行 C2 的操作即使 C1 先于 C2 开始。反之，若 C1 在 C2 开始前就结束了，linearizability 要求服务表现得像先执行了 C1 再执行 C2（即 C2 的操作必须观察到 C1 操作的效果，若有）。
|
||
|
||
Q: 还有哪些一致性模型？
|
||
|
||
A: 可查阅
|
||
|
||
eventual consistency
|
||
causal consistency
|
||
fork consistency
|
||
serializability
|
||
sequential consistency
|
||
timeline consistency
|
||
|
||
数据库、CPU 内存/缓存系统和文件系统等领域还有其它模型。
|
||
|
||
一般而言，不同模型在“对应用程序员是否直观”和“能获得多少性能”上不同。例如，eventual consistency 允许很多异常结果（例如即使写已完成，后续读也可能看不到），但在分布式/复制场景下可以实现比 linearizability 更高的性能。
|
||
|
||
Q: 为何用 linearizability 作为一致性模型，而不是其他如 eventual consistency？
|
||
|
||
A: 人们确实常构建提供比 linearizability 更弱一致性的存储系统，例如 eventual 和 causal consistency。
|
||
|
||
Linearizability 对应用编写者有一些好处：
|
||
|
||
* 读总是能观察到最新数据。
|
||
* 若无并发写，所有读者看到相同数据。
|
||
* 在多数 linearizable 系统上可以加入类似 test-and-set 的小事务（因为多数 linearizable 设计最终会对每个数据项一次执行一个操作）。
|
||
|
||
像 eventual 和 causal consistency 这样的较弱方案能获得更高性能，因为它们不要求所有数据副本立即更新。这种更高性能往往是决定因素。对某些应用弱一致性没有问题，例如只存从不更新的数据（如图片或视频）。
|
||
|
||
但弱一致性会给应用编写者带来一些复杂度：
|
||
|
||
* 读可能观察到过时（stale）数据。
|
||
* 读可能观察到乱序的写。
|
||
* 若你先写再读，可能看不到自己的写，而是看到陈旧数据。
|
||
* 对同一项的并发更新不是一次执行一个，因此难以实现 test-and-set 或原子自增之类的小事务。
|
||
|
||
Q: Linearizability 似乎并不特别“强”，因为即使同时执行两条命令也可能读到不同数据；有没有更强的概念？
|
||
|
||
A: 确实，linearizability 让人联想到在程序里用线程却不用锁。这样也能正确编程，但需要小心。
|
||
|
||
更强的一致性概念之一是事务（transactions），见于很多数据库，会 effectively 锁住所用数据。对读写多个数据项的程序，事务比 linearizability 更易编程。“Serializability”是提供事务的一种一致性模型的名称。
|
||
|
||
但事务系统比 linearizable 系统明显更复杂、更慢、更难做容错。
|
||
|
||
Q: 若存在并发 put()，并发 get() 可能看到不同值，这是否有问题？
|
||
|
||
A: 在存储系统语境下通常没问题。例如，若我们讨论的是我的头像照片，而两个人在我更新照片的同时请求查看，他们看到不同照片（旧或新）是合理的。
|
||
|
||
另一种看法是：这与程序员在多核计算机上已熟悉的行为相同：对正在被写入的内存位置，来自不同核的并发 load 不保证都看到同一值。
|
||
|
||
Q: 现实中有哪些 linearizable 存储系统的例子？以及弱一致性保证的存储系统？
|
||
|
||
A: Google 的 Spanner 和 Amazon 的 S3 是提供 linearizability 的存储系统。
|
||
|
||
Google 的 GFS、Amazon 的 Dynamo 和 Cassandra 提供较弱一致性；它们大概最好归为 eventually consistent。
|
||
|
||
Q: 人们如何确保分布式系统正确？
|
||
|
||
A: 常用做法是充分测试，例如使用 Porcupine 等 linearizability checker。
|
||
|
||
形式化方法也很常见；可参考以下示例：
|
||
|
||
https://arxiv.org/pdf/2210.13661.pdf
|
||
|
||
https://assets.amazon.science/67/f9/92733d574c11ba1a11bd08bfb8ae/how-amazon-web-services-uses-formal-methods.pdf
|
||
|
||
https://dl.acm.org/doi/abs/10.1145/3477132.3483540
|
||
|
||
https://www.ccs.neu.edu/~stavros/papers/2022-cpp-published.pdf
|
||
|
||
https://www.cs.purdue.edu/homes/pfonseca/papers/eurosys2017-dsbugs.pdf
|
||
|
||
https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf
|
||
|
||
Q: 形式化证明一个服务正确有多难？
|
||
|
||
A: 对复杂程序证明重要定理很难——比普通编程难得多。
|
||
|
||
可以通过本课程的实验体会一下：
|
||
|
||
https://6826.csail.mit.edu/2020/
|
||
|
||
Q: 团队如何判断产品已经测试得足够充分可以交付给客户？
|
||
|
||
A: 在公司把钱花光破产之前开始交付产品并获取收入是明智的。人们会在此之前尽可能多测试，并通常尝试说服少数早期客户使用产品（并帮助暴露 bug），同时接受可能不正确的风险。当产品功能足够满足多数客户且没有已知重大 bug 时，或许就可以交付了。
|
||
|
||
除此之外，明智的客户也会对自己依赖的软件做测试。没有严肃的组织会指望任何软件完全没有 bug。
|
||
|
||
Q: Linearizability checker 如何工作？
|
||
|
||
A: 简单的 linearizability checker 会尝试所有可能的顺序（或线性化点的选择），看是否存在符合 linearizability 定义规则的合法顺序。因为这对大历史会太慢，聪明的 checker 会避免检查显然不可能的顺序（例如若提议的线性化点在操作开始时间之前）、在可能时将历史分解为可分别检查的子历史、并用启发式优先尝试更可能的顺序。
|
||
|
||
以下论文描述了相关技术；据我所知 Knossos 基于第一篇，Porcupine 加入了第二篇的思路：
|
||
|
||
http://www.cs.ox.ac.uk/people/gavin.lowe/LinearizabiltyTesting/paper.pdf
|
||
https://arxiv.org/pdf/1504.00204.pdf
|
||
|
||
Q: 有没有用 Porcupine 或类似测试框架测试过的真实系统例子？
|
||
|
||
A: 这类测试很常见——例如可参见 https://jepsen.io/analyses；Jepsen 是测试过多种存储系统正确性（以及在适用时的 linearizability）的机构。
|
||
|
||
针对 Porcupine，例如：
|
||
|
||
https://www.vldb.org/pvldb/vol15/p2201-zare.pdf
|