本库提供代码来定义和验证对象或系统根据其如何响应一组可能并发（即部分有序）的操作的正确性。

通过参考实现定义正确性

SequentialSpec 是一个用于通过“参考实现”定义正确性的特质（例如，“此系统应像队列一样运行”）。此库包含可重用的实现，例如 Register 用于类似寄存器的语义和用于标准库的 [Vec] 用于类似堆栈的语义。自己实现此特质也非常简单——只需定义两个 enum 用于调用和返回。然后将这些（作为 SequentialSpec::Op 和 SequentialSpec::Ret 分别）与实现 SequentialSpec::invoke 的状态类型相关联。

验证并发系统实现

可以使用 ConsistencyTester 对预期的 一致性模型（如 LinearizabilityTester）进行验证。在这种情况下，操作相对于一个抽象的类似线程的调用者是顺序的（想想阻塞 I/O），该调用者由一个独特的“线程 ID”识别（有时在文献中称为“进程 ID”，但由于它们被认为是单线程的，因此线程 ID 对大多数开发者来说可能更有直观性）。

进一步阅读

有关指定并发系统语义的更多背景信息，请参阅以下出版物：

• "非事务性分布式存储系统中的一致性"，作者Viotti和Vukolić
• "最终一致性原理"，作者Burckhardt
• "软件基础卷2：编程语言基础"，作者Pierce等