Modular verification of a non-blocking stack
Modular verification of a non-blocking stack
复制标题
非阻塞堆栈的模块化验证
DOI：
10.1145/1190216.1190261
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
P. O'Hearn
中科院分区：
文献类型：
--
作者：
Matthew J. Parkinson;R. Bornat;P. O'Hearn
本文对包括并发算法在内的程序的模块化证明技术的发展做出了贡献。我们给出了一个提供共享栈的非阻塞并发算法的证明。对于该算法至关重要的线程间干扰在证明以及对在栈上执行入栈和出栈的模块化操作的规范中被限定。这是通过分离逻辑机制实现的。其结果是线程间干扰不会污染栈的客户端的规范或验证。
This paper contributes to the development of techniques for the modular proof of programs that include concurrent algorithms. We present a proof of a non-blocking concurrent algorithm, which provides a shared stack. The inter-thread interference, which is essential to the algorithm, is confined in the proof and the specification to the modular operations, which perform push and pop on the stack. This is achieved by the mechanisms of separation logic. The effect is that inter-thread interference does not pollute specification or verification of clients of the stack.