真实性：具有可交换性的声明式多核编程
摘要：通过一种声明式编程风格，表达并行程序的独立性，可以减轻多核硬件开发的负担。在该推荐的范式中，程序员以熟悉的顺序方式编写代码，并明确地表达其中代码片段的顺序交换条件。将这样的顺序交换条件放入源代码中，为编译器提供了一种利用顺序交换和并行性之间已知联系的新入口。我们为程序员的顺序视角给出了一个语义，并在正确条件下发现，经过编译器转换的并行执行与顺序语义是等效的。串行化/线性化不适合此条件，因此我们引入了作用域可串行化，并展示了如何通过锁合成技术强制执行它。 接下来，我们描述了一种通过从顺序交换区块到逻辑规范的新约简来自动验证和合成交换条件的技术，从而可进行符号交换性推理。我们在一种名为Veracity的新语言中实现了我们的工作，该语言采用Multicore OCaml实现。我们展示了在各种新的基准程序中可以自动生成交换条件，确认了随着计算量的增加可以看到并发加速的预期，并将我们的工作应用于一个小型内存文件系统和一个众筹区块链智能合约的改编。
作者：Adam Chen, Parisa Fathololumi, Eric Koskinen, Jared Pincus
论文ID：2203.06229
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-05-02