带超时分层MCS锁的正确性
分布式、并行与集群计算
2017-01-02 v1
摘要
本手稿作为我们发表于第22届ACM SIGPLAN并行编程原理与实践研讨会论文集的题为“一种面向多级NUMA系统的高效可中止锁协议”中描述的带超时分层MCS锁(HMCS-T)的正确性证明。HMCS-T是一个极为复杂的协议。系统是有状态的；先前获取尝试的值影响后续获取尝试。此外，后继、前驱、祖先与后代的状态影响协议所遵循的步骤。使协议完全非阻塞的能力导致对\texttt{next}字段的修改，这使得在获取与释放上均偏离原始MCS锁协议。在多处，无条件字段更新被SWAP或CAS操作取代。我们采用多步方法证明HMCS-T的正确性。为展示HMCS-T锁的正确性，我们使用Spin模型检测。模型检测即使模拟少量线程也会引起组合爆炸。首先，我们理解证明树中单级锁安全属性所需的最小充分配置。我们构建表示这些配置的HMCS-T锁。我们对这些配置进行模型检测，证明了HMCS-T锁组件的正确性。最后，基于这些事实，我们逻辑论证HMCS-T<n>的正确性。
引用
@article{arxiv.1612.09576,
title = {Correctness of Hierarchical MCS Locks with Timeout},
author = {Milind Chabbi and Abdelhalim Amer and Shasha Wen and Xu Liu},
journal= {arXiv preprint arXiv:1612.09576},
year = {2017}
}