Artifact for the paper: Deductive Verification of Weak Memory Programs with View-based Protocols

See README.md for instructions<br>SHA-256 of the ZIP: `c3f9612c6a69250e43fa6769412df8bcef129a079bb97b77d5991ffaa184ce14`<br>Artifact of Paper: "Deductive Verification of Weak Memory Programs with View-based Protocols"<br>Abstract of Paper:Concurrent programming under weak memory concurrency faces substantial challenges to ensure correctness due to program behaviors that cannot be explained by thread interleaving, a.k.a sequential consistency. While several program logics are proposed to reason about weak memory concurrency, their usage has been limited to intricate manual proofs. On the other hand, the VerCors verifier provides a rich toolset for automated deductive verification for sequential consistency.<br>In this paper, we bridge this gap for automated deductive verification of weak memory concurrent programs with the VerCors deductive verification tool. We propose an approach to encode weak memory concurrency in VerCors. We develop VerCors-relaxed, where we extend the VerCors atomics support and bring concepts from several protocol automata to encode permission-based separation logics for weak memory concurrency models. To demonstrate the effectiveness of our approach, we encode the relaxed fragment of the SLR program logic, a recent state-of-the-art permission-based separation logic for weak memory concurrency in VerCors-relaxed, our extension of VerCors. We use the SLR encoding on VerCors-relaxed to automatically verify several examples from the literature within realistic performance.

操作说明详见README.md文件<br>ZIP包的SHA-256哈希值：`c3f9612c6a69250e43fa6769412df8bcef129a079bb97b77d5991ffaa184ce14`<br>本数据集对应论文：《基于视图协议的弱内存程序演绎验证》（"Deductive Verification of Weak Memory Programs with View-based Protocols"）<br>论文摘要：弱内存并发场景下的并发编程，由于程序行为无法通过线程交错（即顺序一致性（sequential consistency））来解释，因此在保障程序正确性方面面临极大挑战。尽管已有若干程序逻辑被提出用于弱内存并发的形式化推理，但此类逻辑的应用目前仅局限于复杂的人工证明流程。另一方面，VerCors验证器为顺序一致性的自动化演绎验证提供了功能丰富的工具集。<br>本文依托VerCors演绎验证工具，填补了弱内存并发程序自动化演绎验证领域的这一空白。我们提出了一种在VerCors框架内对弱内存并发进行编码的方法，并开发了扩展工具VerCors-relaxed：该工具拓展了VerCors的原子操作支持，并引入了多种协议自动机的相关概念，以针对弱内存并发模型构建基于权限的分离逻辑编码。<br>为验证所提方法的有效性，我们在本次开发的VerCors扩展版VerCors-relaxed中，对SLR程序逻辑的松弛片段完成了编码——SLR是当前主流的面向弱内存并发的基于权限的分离逻辑。随后我们借助VerCors-relaxed上的SLR编码，在符合实际性能要求的前提下，自动验证了来自现有学术文献的多个示例程序。