Thread modularity at many levels: a pearl in compositional verification
Thread modularity at many levels: a pearl in compositional verification
复制标题
多层次的线程模块化：组合验证中的一颗明珠
DOI：
10.1145/3009837.3009893
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
A. Podelski
中科院分区：
文献类型：
--
作者：
Jochen Hoenicke;R. Majumdar;A. Podelski
并发程序正确性的线程模块证明基于每个线程的归纳和无干扰注释。众所周知，相应的证明系统是不完备的(除非增加辅助变量)。我们描述了一个证明系统的层次结构，其中每个级别k对应于线程模块化的一个通用概念(级别1对应于原始概念)。严格来说，每个级别都比前一个级别更具表现力。此外，每个级别精确地捕获可以使用具有k个全称量词的统一Ashcroft不变量来证明的程序。我们通过给出TLB一致性的Mach击落算法的合成证明，证明了该层次结构的有效性。我们在级别2给出了一个证明，证明了该算法对于任意数量的CPU是正确的。然而，对于不涉及辅助状态的第一级算法，目前还没有证明。
A thread-modular proof for the correctness of a concurrent program is based on an inductive and interference-free annotation of each thread. It is well-known that the corresponding proof system is not complete (unless one adds auxiliary variables). We describe a hierarchy of proof systems where each level k corresponds to a generalized notion of thread modularity (level 1 corresponds to the original notion). Each level is strictly more expressive than the previous. Further, each level precisely captures programs that can be proved using uniform Ashcroft invariants with k universal quantifiers. We demonstrate the usefulness of the hierarchy by giving a compositional proof of the Mach shootdown algorithm for TLB consistency. We show a proof at level 2 that shows the algorithm is correct for an arbitrary number of CPUs. However, there is no proof for the algorithm at level 1 which does not involve auxiliary state.
影响因子：
0.8
作者：
Alastair F. Donaldson;A. Kaiser;D. Kroening;Michael Tautschnig;T. Wahl
通讯作者：
Alastair F. Donaldson;A. Kaiser;D. Kroening;Michael Tautschnig;T. Wahl