一句话:系统刻画公平性假设下的三种无锁性语义,并给出仅假设 justness 时完备的会话类型系统。
会话类型系统常以无锁性等活性性质为目标,但此类结论高度依赖对并发执行路径的公平性假设。本文在一个最小会话演算上系统考察所有已知公平性假设,精确识别出三种语义上互异、且各自都有可靠(sound)会话类型系统的无锁性概念。随后,作者在标准全局会话类型方法中引入一个通用 merge 算子,得到对其中最强概念完备(complete)的会话类型系统,而该概念仅假设执行路径的 justness,即并发系统中最弱的公平性假设。该工作厘清了公平性假设与无锁性语义之间的关系,并在如此弱的公平性前提下首次实现会话类型的完备性。
We investigate how different fairness assumptions affect results concerning lock-freedom, a typical liveness property targeted by session type systems. We fix a minimal session calculus and systematically take into account all known fairness assumptions, thereby identifying precisely three interesting and semantically distinct notions of lock-freedom, all of which having a sound session type system. We then show that, by using a general merge operator in an otherwise standard approach to global session types, we obtain a session type system complete for the strongest amongst those notions of lock-freedom, which assumes only justness of execution paths, a minimal fairness assumption for concurrent systems.