Locksynth：利用 ASP 推导并发数据结构同步代码

我们提出 Locksynth，一种自动推导涉及常数个共享堆内存写操作的并发数据结构破坏性更新所需同步的工具。Locksynth 是我们先前关于推导抽象同步代码工作的实现。设计并发数据结构需要从对顺序数据结构操作的前置理解出发推断正确的同步代码，此外还需理解共享内存模型与同步原语。将顺序数据结构转换为并发版本的推理可使用 Answer Set Programming（ASP）进行，我们已在先前工作中将该方法机械化。该推理涉及演绎与溯因，可简洁地建模于 ASP 中。我们假设给定数据结构操作的抽象顺序代码，以及描述并发行为的公理。此信息用于自动推导该数据结构的并发代码，例如涉及常数个破坏性更新操作的链表与二叉搜索树的字典操作。我们亦能推断涉及左/右树旋转的外部高度平衡二叉搜索树的正确锁集合（但不含代码合成）。Locksynth 执行推断正确锁集合所需的分析，并作为最后一步推导所合成数据结构的 C++ 同步代码。我们还提供了由 Locksynth 合成的 C++ 代码与来自 Synchrobench 微基准测试套件的手工版本的性能分析。据我们所知，我们的工具是首个采用 ASP 作为后端推理器来执行并发数据结构合成的。