论文标题
回到期货
Back to Futures
论文作者
论文摘要
并发编程的常见方法始于语言自然是顺序的语言，并添加了新的结构，从而提供有限的并发访问，这是期货的例证。这种方法非常成功，但通常不能为并发结构提供令人满意的理论支持，并且很难提供一种良好的语义，使程序员一次使用这些构造中的多个构造。 我们采用了一种不同的方法，从基于咖喱途径的伴随逻辑解释的并发语言开始，我们添加了三个原子原始图，使我们能够编码顺序组成和各种形式的同步。最终的语言具有很高的表现力，使我们能够在同一框架中编码期货，叉/加入并行性和Monadic并发。值得注意的是，由于我们的语言基于伴随逻辑，因此我们能够对线性期货进行正式描述，这已被Blelloch和Reid-Miller用于复杂性分析。这种方法的统一性意味着我们可以同样以线性方式与许多其他并发原语一起工作，并且我们可以将其中几种形式的并发性混合在同一程序中以实现不同的目的。
Common approaches to concurrent programming begin with languages whose semantics are naturally sequential and add new constructs that provide limited access to concurrency, as exemplified by futures. This approach has been quite successful, but often does not provide a satisfactory theoretical backing for the concurrency constructs, and it can be difficult to give a good semantics that allows a programmer to use more than one of these constructs at a time. We take a different approach, starting with a concurrent language based on a Curry-Howard interpretation of adjoint logic, to which we add three atomic primitives that allow us to encode sequential composition and various forms of synchronization. The resulting language is highly expressive, allowing us to encode futures, fork/join parallelism, and monadic concurrency in the same framework. Notably, since our language is based on adjoint logic, we are able to give a formal account of linear futures, which have been used in complexity analysis by Blelloch and Reid-Miller. The uniformity of this approach means that we can similarly work with many of the other concurrency primitives in a linear fashion, and that we can mix several of these forms of concurrency in the same program to serve different purposes.
