Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic
Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic
复制标题
DOI：
10.1145/2818638
复制
发表时间：
2016-01-01
影响因子：
1.3
通讯作者：
Birkedal, Lars
中科院分区：
文献类型：
--
作者：
Dodds, Mike;Jagannathan, Suresh;Birkedal, Lars
同步构造是任何可靠并发程序的核心。许多这样的结构是标准的（e。例如，在一个实施例中，锁、队列、堆栈和散列表）。但是，许多并发应用程序需要具有特殊用途行为的自定义同步构造。这些结构对核查提出了重大挑战。像标准构造一样，它们依赖于微妙的活泼行为，但与标准构造不同的是，它们可能没有很好理解的抽象接口。由于它们是自定义构建的，因此这些构造也更有可能不可靠。我们的目标是一个用于自动并行化的通道库，以强制执行程序语句之间的顺序行为。我们的高级规范捕获了正确执行所必需的条件;这些条件反映了确保顺序行为所必需的程序依赖性。我们将高层规范与低层库实现连接起来，以证明客户的需求得到了满足。值得注意的是，我们可以在不打破抽象边界的情况下推理程序和库的正确性。为了实现这一点，我们使用了一种基于分离逻辑的程序逻辑，称为iCAP（非谓词并发抽象谓词）。iCAP支持关于种族的高级抽象和低级推理。我们用它来说明我们的高级通道规范抽象了三个不同的，越来越复杂的低级实现的库。iCAP对高阶推理的支持使我们能够证明顺序依赖性是受尊重的，而iCAP的下一代语义模型使我们能够避免循环依赖性的丑陋问题。
Synchronization constructs lie at the heart of any reliable concurrent program. Many such constructs are standard (e. g., locks, queues, stacks, and hash-tables). However, many concurrent applications require custom synchronization constructs with special-purpose behavior. These constructs present a significant challenge for verification. Like standard constructs, they rely on subtle racy behavior, but unlike standard constructs, they may not have well-understood abstract interfaces. As they are custom built, such constructs are also far more likely to be unreliable.This article examines the formal specification and verification of custom synchronization constructs. Our target is a library of channels used in automated parallelization to enforce sequential behavior between program statements. Our high-level specification captures the conditions necessary for correct execution; these conditions reflect program dependencies necessary to ensure sequential behavior. We connect the high-level specification with the low-level library implementation to prove that a client's requirements are satisfied. Significantly, we can reason about program and library correctness without breaking abstraction boundaries.To achieve this, we use a program logic called iCAP (impredicative Concurrent Abstract Predicates) based on separation logic. iCAP supports both high-level abstraction and low-level reasoning about races. We use this to show that our high-level channel specification abstracts three different, increasingly complex low-level implementations of the library. iCAP's support for higher-order reasoning lets us prove that sequential dependencies are respected, while iCAP's next-generation semantic model lets us avoid ugly problems with cyclic dependencies.