一句话：提出声明式多核编程范式，程序员以顺序方式书写并显式标注代码片段的可交换条件，编译器据此自动并行化。
多核编程的现有抽象（如并发对象、事务内存）虽简化了编程，但仍需复杂工程。本文提出一种声明式编程风格：程序员像往常一样编写顺序程序，并显式表达代码片段在何种条件下可顺序交换（commutativity）。这种可交换条件为编译器利用可交换性与并行性的联系提供了新入口。作者给出了程序员顺序视角的语义，并在正确性条件下证明编译器转换后的并行执行与顺序语义等价；由于可串行化/线性化并不适用，他们提出作用域可串行化（scoped serializability），并用锁合成技术加以保证。进一步，论文将可交换块归约为逻辑规约，从而自动验证并合成可交换条件。作者在 Multicore OCaml 中实现了 Veracity 语言，在多种新基准程序上自动生成可交换条件，验证了并发加速随计算规模增加而出现，并将该工作应用于小型内存文件系统和众筹区块链智能合约的改编。
There is an ongoing effort to provide programming abstractions that ease the burden of exploiting multicore hardware. Many programming abstractions ( e.g. , concurrent objects, transactional memory, etc.) simplify matters, but still involve intricate engineering. We argue that some difficulty of multicore programming can be meliorated through a declarative programming style in which programmers directly express the independence of fragments of sequential programs. In our proposed paradigm, programmers write programs in a familiar, sequential manner, with the added ability to explicitly express the conditions under which code fragments sequentially commute. Putting such commutativity conditions into source code offers a new entry point for a compiler to exploit the known connection between commutativity and parallelism. We give a semantics for the programmer’s sequential perspective and, under a correctness condition, find that a compiler-transformed parallel execution is equivalent to the sequential semantics. Serializability/linearizability are not the right fit for this condition, so we introduce scoped serializability and show how it can be enforced with lock synthesis techniques. We next describe a technique for automatically verifying and synthesizing commute conditions via a new reduction from our commute blocks to logical specifications, upon which symbolic commutativity reasoning can be performed. We implemented our work in a new language called Veracity, implemented in Multicore OCaml. We show that commutativity conditions can be automatically generated across a variety of new benchmark programs, confirm the expectation that concurrency speedups can be seen as the computation increases, and apply our work to a small in-memory filesystem and an adaptation of a crowdfund blockchain smart contract.
@article{paperbot1413,
title = {Veracity: declarative multicore programming with commutativity},
author = {Adam Chen and Parisa Fathololumi and Eric Koskinen and Jared Pincus},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563349}
}