Veracity：具有交换性的声明式多核编程
Veracity: Declarative Multicore Programming with Commutativity
摘要：
人们一直在努力提供编程抽象，以减轻利用多核硬件的负担。许多编程抽象（例如，并发对象、事务存储器等）简化问题，但仍然涉及复杂的工程。我们认为，一些困难的多核编程可以改善通过声明式编程风格，程序员直接表示独立的顺序程序的片段。在我们提出的范例中，程序员以熟悉的顺序方式编写程序，并增加了明确表达代码片段顺序交换条件的能力。将这样的交换性条件放入源代码中为编译器提供了一个新的切入点，以利用交换性和并行性之间的已知联系。我们给出了一个语义程序员的顺序的角度来看，在正确的条件下，发现编译器转换的并行执行是等价的顺序语义。可串行化/可线性化不适合这种情况，因此我们引入了作用域可串行化，并展示了如何使用锁合成技术来实现它。接下来，我们描述了一种技术，通过一个新的减少从我们的交换块的逻辑规范，符号交换推理可以执行自动验证和合成的交换条件。我们用一种名为Veracity的新语言实现了我们的工作，该语言在多核OCaml中实现。我们证明了交换性条件可以在各种新的基准程序中自动生成，确认了并发加速可以随着计算的增加而被看到的期望，并将我们的工作应用于小型内存文件系统和众筹区块链智能合约的适应。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
