使用锁不变式证明逻辑原子性
摘要：对于并发分离逻辑中的数据结构，逻辑原子性已被广泛接受为规范格式。虽然既有无锁数据结构也有基于锁的数据结构已根据逻辑原子性规范进行了验证，但大多数基于锁的数据结构的验证都是以原子锁规范作为起点。本文将这种方法与基于旧的基于锁不变性的锁规范的方法进行了比较。我们展示了即使使用这些旧的规范，我们仍然可以证明细粒度锁定的数据结构的逻辑原子性规范，但这些证明要比使用原子锁规范的证明复杂得多。我们的证明技术已在验证软件工具链中实现，并依赖于旧的锁规范用于其完备性证明，并应用于基于C的锁定并发数据结构的实现。
作者：Roshan Sharma, Shengyi Wang, Alexander Oey, Anastasiia Evdokimova, Lennart Beringer, William Mansky
论文ID：2304.13898
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-28