piCoq: parallel regression proving for large-scale verification projects
piCoq: parallel regression proving for large-scale verification projects
复制标题
piCoq：大规模验证项目的并行回归证明
DOI：
10.1145/3213846.3213877
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Gligoric, Milos
中科院分区：
文献类型：
--
作者：
Palmskog, Karl;Celik, Ahmet;Gligoric, Milos
使用证明助手的大型验证项目通常包含许多必须在每次新项目修订时检查的证明。虽然证明检查有时可以在粗粒度文件级别并行化以节省时间，但LCF系列中的一些证明助手（如Coq）最近的更改支持在证明级别实现细粒度并行化。然而，这些并行技术目前还没有与回归证明选择集成，回归证明选择是一种只检查受变化影响的证明子集的技术。我们提出的技术混合了并行证明检查和选择的力量，以加速验证项目中的回归证明，适合在用户自己的机器上使用，也适合在涉及持续集成服务的工作流中使用。我们在一个支持Coq项目的工具piCoq中实现了这些技术。piCoq可以跟踪文件、定义和引理之间的依赖关系，并仅对那些受两个项目修订之间变化影响的文件或证明执行并行检查。我们应用piCoq对几个大型开源项目的多次修订执行回归证明，并测量了证明检查时间。虽然使用证明级并行性和文件选择可以获得可观的收益，但我们的结果表明，证明级并行性和证明选择始终比从头开始的顺序检查和使用证明选择的顺序检查快得多。特别是，4路并行化比前者快28.6倍，比后者快2.8倍。
Large-scale verification projects using proof assistants typically contain many proofs that must be checked at each new project revision. While proof checking can sometimes be parallelized at the coarse-grained file level to save time, recent changes in some proof assistant in the LCF family, such as Coq, enable fine-grained parallelism at the level of proofs. However, these parallel techniques are not currently integrated with regression proof selection, a technique that checks only the subset of proofs affected by a change. We present techniques that blend the power of parallel proof checking and selection to speed up regression proving in verification projects, suitable for use both on users' own machines and in workflows involving continuous integration services. We implemented the techniques in a tool, piCoq, which supports Coq projects. piCoq can track dependencies between files, definitions, and lemmas and perform parallel checking of only those files or proofs affected by changes between two project revisions. We applied piCoq to perform regression proving over many revisions of several large open source projects and measured the proof checking time. While gains from using proof-level parallelism and file selection can be considerable, our results indicate that proof-level parallelism and proof selection is consistently much faster than both sequential checking from scratch and sequential checking with proof selection. In particular, 4-way parallelization is up to 28.6 times faster than the former, and up to 2.8 times faster than the latter.
登录
查看更多内容
证明通用：证明开发的通用工具
DOI：
10.1007/3-540-46419-0_3
发表时间：
2000
期刊：
Nord. J. Comput.
影响因子：
--
作者：
David Aspinall
通讯作者：
David Aspinall
标准 ML 的单独编译
DOI：
10.1145/178243.178245
发表时间：
1994
期刊：
--
影响因子：
--
作者：
A. Appel;David B. MacQueen
通讯作者：
David B. MacQueen
Coq 文档的异步处理：从内核到用户界面
DOI：
10.1007/978-3-319-22102-1_4
发表时间：
2015
期刊：
--
影响因子：
--
作者：
Bruno Barras;C. Tankink;Enrico Tassi
通讯作者：
Enrico Tassi
影响因子：
0.8
作者：
Boldo, Sylvie;Lelay, Catherine;Melquiond, Guillaume
通讯作者：
Melquiond, Guillaume
DOI：
10.1007/s10009-017-0457-2
发表时间：
2016-04
影响因子：
1.5
作者：
A. Faithfull;Jesper Bengtson;Enrico Tassi;C. Tankink
通讯作者：
A. Faithfull;Jesper Bengtson;Enrico Tassi;C. Tankink