Veracity: declarative multicore programming with commutativity
Veracity: declarative multicore programming with commutativity
复制标题
DOI：
10.1145/3563349
复制
发表时间：
2022-03
影响因子：
--
通讯作者：
A. Chen;Parisa Fathololumi;Eric Koskinen;Jared Pincus
中科院分区：
文献类型：
--
作者：
A. Chen;Parisa Fathololumi;Eric Koskinen;Jared Pincus
目前正在努力提供编程抽象，以减轻开发多核硬件的负担。许多编程抽象(例如，并发对象、事务内存等)简化问题，但仍涉及复杂的工程。我们认为，多核编程的一些困难可以通过声明式编程风格来改善，在这种风格中，程序员直接表达顺序程序片段的独立性。在我们提出的范例中，程序员以熟悉的顺序方式编写程序，并增加了显式表达代码片段顺序交换的条件的能力。将这种交换性条件放入源代码中为编译器提供了一个新的入口点，以利用交换性和并行性之间的已知联系。我们给出了程序员顺序观点的语义，并且在一个正确的条件下，我们发现编译器转换的并行执行等价于顺序语义。可串行化/可线性化并不适合这种情况，因此我们引入了作用域可串行化，并展示了如何使用锁合成技术来强制执行它。接下来，我们描述了一种自动验证和综合通勤条件的技术，它通过一种新的从通勤块到逻辑规范的简化，在此基础上可以执行符号可交换性推理。我们用一种名为Verity的新语言实现了我们的工作，该语言在多核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.