权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

SHF:Small: Enriching Session Types for Practical Concurrent Programming

SHF:Small：丰富实用并发编程的会话类型

基本信息

批准号：
1718267
负责人：
Frank Pfenning
金额：
$ 45万
依托单位：
Carnegie-Mellon University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2017
资助国家：
美国
起止时间：
2017-07-15 至 2020-06-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1718267&HistoricalAwards=false
关键词：
SHF Small Enriching Session Types

项目摘要

Concurrent programming is becoming increasingly prevalent because of the distributed nature of many applications and the prospect of performance gains. However, concurrent programming is also notoriously error-prone because of the presence of data races and deadlocks. A promising approach to concurrent programing is message-passing concurrency, due to its higher-level of abstraction. Message-passing concurrency has been adopted by various practical programming languages, such as Erlang, Go, and Rust. Servo, for example, is an experimental browser engine developed in Rust that exploits message-passing concurrency for tasks, such as DOM traversal, layout painting, and JavaScript execution. This research project studies the application of session types to practical message-passing concurrency, while addressing the pitfalls of data races and deadlocks. Session types allow the expression and compile-time checking of the protocols of message exchange. The project's intellectual merits are to lift the expressiveness of session types to accommodate today's concurrent communication patterns, while remaining truthful to their logical foundation. The project's broader significance and importance are its provision of both a foundational and practical view on concurrent programming, the development of curricular material at the sophomore-level, and a session type extension for Rust.The logical foundation of this research project is the recently discovered Curry-Howard isomorphism between intuitionistic linear logic and session types, which relates linear propositions to session types, sequent calculus proofs to concurrent processes, and cut reduction to message-passing communication. Existing work building on this foundation provides strong guarantees, but also narrows the applicability of session types. The aim of this research is two-fold: (i) to increase the applicability of session types, while keeping their logical foundation intact, and (ii) to demonstrate practicality of the resulting techniques to real-world software development. For (ii), the project explores the application of the techniques resulting from (i) to the Servo code base. For (i), the project first explores the introduction of shared channels to support programs that demand sharing by the nature of circumstances or for performance considerations. Key concerns in this exploration are the prevention of data races along shared channels to guarantee session fidelity and the assurance of a form of global progress. In its simplest form, global progress will lack deadlock freedom, a property holding in the purely linear setting. In a second phase, a logical interpretation of deadlock prevention is derived. In a third phase, the project explores the enrichment of session types with dependent typing for the expression and verification of properties that are not primarily protocol-related. In all cases, proofs of soundness as well as a prototype of a session-typed concurrent programming language accommodating the developed techniques are given.

由于许多应用程序的分布式特性和性能提高的前景，并发编程正变得越来越流行。然而，并发编程也是出了名的容易出错，因为存在数据竞争和死锁。一种很有前途的并发编程方法是消息传递并发，因为它具有更高的抽象级别。消息传递并发性已经被各种实用的编程语言所采用，如Erlang，Go和Rust。例如，Servo是一个在Rust中开发的实验性浏览器引擎，它利用了DOM遍历、布局绘制和JavaScript执行等任务的消息传递并发性。这个研究项目研究会话类型在实际消息传递并发中的应用，同时解决数据竞争和死锁的陷阱。会话类型允许消息交换协议的表达式和编译时检查。该项目的智力价值是提升会话类型的表达能力，以适应当今的并发通信模式，同时保持其逻辑基础的真实性。该项目的更广泛的意义和重要性在于它提供了并发编程的基础和实用观点，在走廊级别开发课程材料，以及Rust的会话类型扩展。该研究项目的逻辑基础是最近发现的直觉线性逻辑和会话类型之间的Curry-Howard同构，它将线性命题与会话类型联系起来，并发进程的并行演算证明，消息传递通信的裁减。在此基础上建立的现有工作提供了强有力的保证，但也缩小了会话类型的适用性。本研究的目的是双重的：（i）增加会话类型的适用性，同时保持其逻辑基础不变，以及（ii）展示所得到的技术在现实世界的软件开发中的实用性。对于（ii），该项目探讨了从（i）到伺服代码库的技术的应用。对于（i），该项目首先探讨了引入共享渠道，以支持因环境性质或绩效考虑而需要共享的计划。这种探索的关键问题是防止沿着共享通道的数据竞争，以保证会话保真度和保证某种形式的全球进展。在其最简单的形式中，全局进程将缺乏死锁自由，这是一个在纯线性设置中保持的属性。在第二阶段，死锁预防的逻辑解释。在第三阶段，该项目探索了丰富的会话类型与依赖类型的表达和验证的属性，主要是不相关的协议。在所有的情况下，证明的合理性，以及一个原型的会话类型的并发编程语言，容纳开发的技术。