一句话：提出统一 futures、transactions 与 actors 的并发语言 Chocola，形式化语义并证明其保证。
程序员常在同一程序内混合使用多种并发模型，以在程序各部分选用最合适的模型。Clojure、Scala 和 Java 等语言虽支持这种需求，但组合方式往往是临时的，组合语义也未良定义；朴素组合 futures、transactions 与 actors 会破坏各模型原本提供的保证，违背程序员假设。本文提出统一语言 Chocola，将 futures、transactions 和 actors 整合，并尽可能在组合时维持三者的保证。作者形式化 Chocola 的语义并证明其提供的保证，同时将其实现为 Clojure 扩展。评估表明，该实现能以开发者相对较小的努力提升三个基准应用的性能。
Programmers often combine different concurrency models in a single program, in each part of the program using the model that fits best. Many programming languages, such as Clojure, Scala, and Java, cater to this need by supporting different concurrency models. However, existing programming languages often combine concurrency models in an ad hoc way, and the semantics of the combinations are not always well defined. This article studies the combination of three concurrency models: futures, transactions, and actors. We show that a naive combination of these models invalidates the guarantees they normally provide, thereby breaking the assumptions of programmers. Hence, we present Chocola : a unified language of futures, transactions, and actors that maintains the guarantees of all three models wherever possible, even when they are combined. We describe and formalize the semantics of this language and prove the guarantees it provides. We also provide an implementation as an extension of Clojure and demonstrated that it can improve the performance of three benchmark applications for relatively little effort from the developer.