一句话：提出 Trillium 分离逻辑框架，以内涵精化证明高阶并发与分布式程序的安全和活性性质。
现有高阶并发与分布式分离逻辑常依赖 step-indexing 来建模复杂语义并支持模块化推理，但这会使程序逻辑的 adequacy 定理局限于较简单的安全性质。本文提出 Trillium，一个语言无关的分离逻辑框架，用于建立程序 trace 与模型之间的内涵精化关系，从而强化高阶并发及分布式分离逻辑以证明非平凡的安全与活性性质。作者将 Trillium 实例化到并发语言，得到 Fairis 并发分离逻辑，并通过保持活性的公平精化在公平调度假设下证明并发程序活性；还将其实例化到分布式语言，扩展 Aneris 分布式分离逻辑，用以证明分布式系统与 TLA+ 模型之间的精化关系。
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. Stepindexing 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.
@article{paperbot2600,
title = {Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement},
author = {Amin Timany and Simon Oddershede Gregersen and Léo Stefanesco and Jonas Kastberg Hinrichsen and Léon Gondelman and Abel Nieto and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632851}
}