一句话：提出声明式框架，在弱内存一致性下对并发库进行组合式规约与验证。
并发库是并发编程的基础构件，涵盖锁、交换器、栈、队列和集合等，并以分层方式构建。已有工作多集中于顺序一致性（SC）环境下验证这些库，而在弱内存一致性（WMC）下如何规约和验证它们仍不清楚。本文提出一个通用的声明式框架，用于声明式地规约并发库，并组合式地验证库实现满足其规约。该框架能够编码 SC、(R)C11 和 TSO 等标准内存模型。作者还规约了互斥锁、读写锁、交换器、队列、栈和集合等多种并发库，并利用该框架验证了锁、交换器、队列和栈的多个弱一致实现。
Concurrent libraries are the building blocks for concurrency. They encompass a range of abstractions (locks, exchangers, stacks, queues, sets) built in a layered fashion: more advanced libraries are built out of simpler ones. While there has been a lot of work on verifying such libraries in a sequentially consistent (SC) environment, little is known about how to specify and verify them under weak memory consistency (WMC). We propose a general declarative framework that allows us to specify concurrent libraries declaratively, and to verify library implementations against their specifications compositionally. Our framework is sufficient to encode standard models such as SC, (R)C11 and TSO. Additionally, we specify several concurrent libraries, including mutual exclusion locks, reader-writer locks, exchangers, queues, stacks and sets. We then use our framework to verify multiple weakly consistent implementations of locks, exchangers, queues and stacks.
@article{paperbot666,
title = {On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models},
author = {Azalea Raad and Marko Doko and Lovro Rožić and Ori Lahav and Viktor Vafeiadis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290381}
}