Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement.
Proceedings of the ACM on Programming Languages(2024)
摘要
Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features
and to support modular reasoning about imperative higher-order concurrent and distributed programs. Step-
indexing comes, however, with an inherent cost: it restricts the adequacy theorem of program logics to a fairly
simple class of safety properties.
In this paper, we explore if and how intensional refinement is a viable methodology for strengthening
higher-order concurrent (and distributed) separation logic to prove non-trivial safety and liveness properties.
Specifically, we introduce Trillium, a language-agnostic separation logic framework for showing intensional
refinement relations between traces of a program and a model. We instantiate Trillium with a concurrent
language and develop Fairis, a concurrent separation logic, that we use to show liveness properties of concurrent
programs under fair scheduling assumptions through a fair liveness-preserving refinement of a model. We also
instantiate Trillium with a distributed language and obtain an extension of Aneris, a distributed separation
logic, which we use to show refinement relations between distributed systems and TLA+ models.
更多查看译文
关键词
Distributed systems,concurrency,formal verification,higher-order logic,refinement,separation logic
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要