8 月 Murat Derimbas 发表关于 Herlihy 和 Wing 论文的博客，介绍线性化概念及相关内容。

• 程序正确性：抽象数据类型（ADT）如栈、队列、映射等定义操作，以队列为例，dequeue 应返回未出队的最早入队值，可通过测试执行历史来验证，需描述所有可能的有效执行历史，可用过渡公理法（TLA+语言支持），用状态机模型描述系统，包括有效初始状态和状态转换集（动作），每个步骤对应一个动作，整个状态机描述为规范。
• 用 TLA+建模计数器：计数器有 inc（增）、get（取）、reset（重置）操作，通过状态变量 op、rval、flag 建模，内部变量 c 记录重置后增量，不同行为展示了 stuttering 步骤等情况。
• 用 TLA+建模队列：队列有 enq（入队）、deq（出队）操作，通过 op、arg、rval 建模，内部变量 d 用序列记录入队值及顺序，Deq 和 Enq 动作描述状态转换，还需考虑并发情况，用函数将变量作用域限定到线程。
• 并发建模：并发程序中操作可重叠，需用状态机模型建模，每个线程独立，需建模线程局部变量，内部变量 d 需考虑相对操作顺序及更新。
• 线性化作为并发正确性条件：线性化在并发操作重叠时确定队列执行历史的正确性，能给出并发对象操作的意义，如某些队列观察执行历史可识别线性化点形成顺序执行历史，建模线性化队列需考虑操作的开始、生效、结束及内部变量。
• 用 TLA+建模线性化队列：通过三个动作建模线性化队列，内部变量 up 表示内部状态是否更新，需处理多线程情况，参数化动作到线程 id，有 LinearizableQueue.tla 模型。
• 示例队列实现：Python 实现的 LLLQueue（锁定链表队列）用锁保护链表存储数据，PlusCal 建模 enqueue 操作，用五个动作实现，通过 refinement mappings 验证线性化，需定义内部变量映射。
• refinement mappings：用 formal methods 验证低级别实现符合高级别规范，通过构造找到从实现到规范的对应行为，需定义细化映射函数，确保外部变量相同且状态转换符合规范，如 LLLQueue 到 LinearizableQueue 的映射。
• Herlihy 和 Wing 队列的 refinement mappings 问题：Herlihy & Wing 队列用数组实现，enqueue 分两步，dequeue 查找非空值并复制，其伪码和 C++实现展示原子操作，在 TLA+建模时存在 refinement mapping 难题，因为 enq 不是原子操作，状态依赖线程调度，不同映射选项均不符合 LinearizableQueue 规范，说明不是所有实现都存在这种映射，该队列元素非全序，Herlihy & Wing 用映射集方法，Lamport 引入 prophecy variables 解决，HWQueueProphecy 增加预言变量预测 dequeue 顺序，需满足正确预言存在和错误预言对应有效行为等要求，通过预言变量可进行 refinement mapping 但逻辑较复杂。
• 参考资料：包括多篇博客、论文、书籍（PDF）、网站及 GitHub 仓库等，提供丰富学习资源。