文件名称：linearizability-checker:快速线性化检查器
文件大小：438.22MB
文件格式：ZIP
更新时间：2024-06-18 18:47:49
C++
线性化检查器 是并发数据类型的公认正确性标准，它对应于分布式系统的之一，即一致性。 线性化背后的直觉是所谓的历史中的所有操作都可以沿着时间线重新排序，以便给定的顺序规范成立。 给定历史和顺序规范，线性化检查器检查是否存在这种重新排序。 一般来说，检查线性化是，因此编写一个有效的线性化检查器本质上是困难的。 这是通过实验比较各种技术以找出在实践中有效的方法的动机 - 此源代码存储库的目的。 在我们的实验中，我们从英特尔的(TBB) 库、西门子的(EMBB) 库和使用的分布式键值存储收集了历史记录。 简而言之，我们工作的结果是一个线性化检查器，它可以检查当前实现超时或内存不足的 CP 分布式系统。 例子 考虑以下寄存器读写操作的历史H ： write(1) read() : 2 |----------| |------