A Concurrent Language with a Uniform Treatment of Regions and Locks

Bestow and Atomic: Concurrent Programming using Isolation, Delegation and Grouping

Any non-trivial concurrent system warrants synchronisation, regardless of the concurrency model. Actor-based concurrency serialises all computations in an actor through asynchronous message passing. In contrast, lock-based concurrency serialises some computations by following a lock--unlock protocol for accessing certain data. Both systems require sound reasoning about pointers and aliasing to exclude data-races. If actor isolation is broken, so is the single-thread-of-control abstraction. Similarly for locks, if a datum is accessible outside of the scope of the lock, the datum is not governed…

使用锁不变式证明逻辑原子性

Proving Logical Atomicity using Lock Invariants

本文比较原子性锁规范与早期基于锁不变式的规范，证明后者仍可验证细粒度锁数据结构的逻辑原子性，但证明更复杂，并在 VST 中应用于 C 实现。

Safe Non-blocking Synchronization in Ada 202x

The mutual-exclusion property of locks stands in the way to scalability of parallel programs on many-core architectures. Locks do not allow progress guarantees, because a task may fail inside a critical section and keep holding a lock that blocks other tasks from accessing shared data. With non-blocking synchronization, the drawbacks of locks are avoided by synchronizing access to shared data by atomic read-modify-write operations. To incorporate non-blocking synchronization in Ada~202x, programmers must be able to reason about the behavior and performance of tasks in the absence of protected …

Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis

Verification of concurrent data structures is one of the most challenging tasks in software verification. The topic has received considerable attention over the course of the last decade. Nevertheless, human-driven techniques remain cumbersome and notoriously difficult while automated approaches suffer from limited applicability. The main obstacle for automation is the complexity of concurrent data structures. This is particularly true in the absence of garbage collection. The intricacy of lock-free memory management paired with the complexity of concurrent data structures makes automated veri…

Concurrent Separation Logic Meets Template Games

An old dream of concurrency theory and programming language semantics has been to uncover the fundamental synchronization mechanisms which regulate situations as different as game semantics for higher-order programs, and Hoare logic for concurrent programs with shared memory and locks. In this paper, we establish a deep and unexpected connection between two recent lines of work on concurrent separation logic (CSL) and on template game semantics for differential linear logic (DiLL). Thanks to this connection, we reformulate in the purely conceptual style of template games for DiLL the asynchron…

一种用于验证细粒度并发模块完全正确性的灵活规约方法

A flexible specification approach for verifying total correctness of fine-grained concurrent modules

提出名为 Sassy 的灵活规约方法，通过将义务创建操作作为参数传递给阻塞操作，克服了传统锁获取证明规则的局限，并利用扩展的 HeapLang 和安全分离逻辑，在细粒度并发设置中实现了终止性的组合性推理与机器检查验证。

验证无锁搜索结构模板

Verifying Lock-free Search Structure Templates

本文提出并验证了覆盖链表和跳表实现的通用无锁搜索结构模板算法，在Iris中机械化线性化证明，并利用后见之明论证简化未来依赖线性化点的推理，减少证明工作量。

An Asynchronous soundness theorem for concurrent separation logic

Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program $C$, we associate a pair of asynchronous transition systems $[C]_S$ and $[C]_L$ which describe the operational behavior of the Code when confronted to its Environment or Frame --- both at the level of machine states ($S$) and of machine instructions and locks ($L$). We then establish that every derivation tree $π$ of a judgment $Γ\vdash\{P\…

A Variant of Concurrent Constraint Programming on GPU

The number of cores on graphical computing units (GPUs) is reaching thousands nowadays, whereas the clock speed of processors stagnates. Unfortunately, constraint programming solvers do not take advantage yet of GPU parallelism. One reason is that constraint solvers were primarily designed within the mental frame of sequential computation. To solve this issue, we take a step back and contribute to a simple, intrinsically parallel, lock-free and formally correct programming language based on concurrent constraint programming. We then re-examine parallel constraint solving on GPUs within this fo…

Modular termination verification with a higher-order concurrent separation logic (Intermediate report)

We report on intermediate results of our research on reasoning about liveness properties in addition to deep correctness properties for an imperative, concurrent programming language with a higher-order store. At present, we focus on one particular liveness property, namely termination. By guaranteeing termination we can strengthen statements of partial correctness to total correctness. This is achieved by the classic approach of turning termination into a safety property. In particular we extend the programming language under consideration with call permissions, which have been shown to enabl…

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory

Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistency. So far, this has lead to the design of a number of persistent concurrent data structures, built to satisfy an associated notion of correctness: durable linearizability. In this paper, we transfer the principle of durable concurrent correctness to the area of software transactional memory (STM). S…