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+模型之间的精化关系。