利用会话类型从无锁性到进展性
编程语言
2013-12-11 v1 分布式、并行与集群计算
摘要
受 Kobayashi 无锁性类型系统的启发，我们为二元会话语言定义了一个行为类型系统以确保进展性。其核心思想是用代表执行紧迫性的优先级来注释会话类型中的动作，并验证进程是否以所需的优先级执行这些动作。与会话语言的相关系统相比，所提出的类型系统相对更简单，并为更广泛的进程建立了进展性保证。
引用
@article{arxiv.1312.2698,
title = {From Lock Freedom to Progress Using Session Types},
author = {Luca Padovani},
journal= {arXiv preprint arXiv:1312.2698},
year = {2013}
}
备注
In Proceedings PLACES 2013, arXiv:1312.2218