Probabilistic Resource-Aware Session Types
Probabilistic Resource-Aware Session Types
复制标题
DOI：
10.1145/3571259
复制
发表时间：
2020-11
影响因子：
--
通讯作者：
Ankush Das;Di Wang;Jan Hoffmann
中科院分区：
文献类型：
--
作者：
Ankush Das;Di Wang;Jan Hoffmann
会话类型保证消息传递进程遵守预定义的通信协议。以前关于会话类型的工作主要集中在确定性语言上，但许多消息传递系统，如马尔可夫链和随机分布式算法，都是概率的。为了实现和分析这类系统，本文发展了概率会话类型的元理论，并将应用重点放在自动预期资源分析上。概率会话类型描述消息上的概率分布，是直觉(二进制)会话类型的保守扩展。为了在概率信道上发送，处理必须利用来自概率分支的内部随机性或来自在概率信道上接收的外部随机性。对预期资源范围的分析与类型系统顺利集成，是自动摊销资源分析的变体。类型推理依赖于线性约束求解来自动导出各种成本度量的符号界限。技术贡献包括元理论，它基于一种新的嵌套多重宇宙语义，以及一种类型重建算法，该算法允许灵活地混合不同来源的随机性，而不会给程序员带来复杂类型注释的负担。该类型系统已在NomosPro语言中实现，具有线性时间类型检查功能。实验表明，NomosPro可应用于随机分布式算法的代价分析、马尔可夫链分析、摊余数据结构的概率分析和数字合同等领域。通过(I)实现两次广播和有界重传协议，其中消息以固定的概率被丢弃，以及(Ii)验证具有状态和420个转变的马尔可夫链的极限分布，还表明NOMOS Pro是可伸缩的。
Session types guarantee that message-passing processes adhere to predefined communication protocols. Prior work on session types has focused on deterministic languages but many message-passing systems, such as Markov chains and randomized distributed algorithms, are probabilistic. To implement and analyze such systems, this article develops the meta theory of probabilistic session types with an application focus on automatic expected resource analysis. Probabilistic session types describe probability distributions over messages and are a conservative extension of intuitionistic (binary) session types. To send on a probabilistic channel, processes have to utilize internal randomness from a probabilistic branching or external randomness from receiving on a probabilistic channel. The analysis for expected resource bounds is smoothly integrated with the type system and is a variant of automatic amortized resource analysis. Type inference relies on linear constraint solving to automatically derive symbolic bounds for various cost metrics. The technical contributions include the meta theory that is based on a novel nested multiverse semantics and a type-reconstruction algorithm that allows flexible mixing of different sources of randomness without burdening the programmer with complex type annotations. The type system has been implemented in the language NomosPro with linear-time type checking. Experiments demonstrate that NomosPro is applicable in different domains such as cost analysis of randomized distributed algorithms, analysis of Markov chains, probabilistic analysis of amortized data structures and digital contracts. NomosPro is also shown to be scalable by (i) implementing two broadcast and a bounded retransmission protocol where messages are dropped with a fixed probability, and (ii) verifying the limiting distribution of a Markov chain with 64 states and 420 transitions.