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.

翻译：现有的先进分离逻辑依赖于步进索引来建模语义复杂的特性，并支持对命令式高阶并发与分布式程序进行模块化推理。然而，步进索引本身存在固有代价：它将程序逻辑的恰当性定理限制在相当简单的安全属性类别内。本文探讨内涵精化是否以及如何成为一种可行的改进方法，用于强化高阶并发（及分布式）分离逻辑，从而证明非平凡的安全属性和活性属性。具体而言，我们引入了Trillium——一种与语言无关的分离逻辑框架，用于证明程序轨迹与模型之间的内涵精化关系。我们将Trillium实例化到一种并发语言中，开发了并发分离逻辑Fairis，通过模型的保活性精化，在公平调度假设下证明并发程序的活性属性。同时，我们将Trillium实例化到一种分布式语言中，得到分布式分离逻辑Aneris的扩展，用于证明分布式系统与TLA+模型之间的精化关系。