Separation Logic

分离逻辑既指一种谓词逻辑的扩展，也指以此种逻辑进行断言的Hoare Logic扩展及其推理系统。

The key ideas of Separation Logic were devised by John Reynolds, inspired in part by older work by Burstall [1972]. Reynolds presented his ideas in lectures given in the fall of 1999. The proposed rules turned out to be unsound, but O’Hearn and Ishtiaq [2001] noticed a strong relationship with the logic of bunched implications [O’Hearn and Pym, 1999], leading to ideas on how to set up a sound program logic. Soon afterwards, the seminal publications on Separation Logic appeared at the CSL workshop [O’Hearn et al., 2001] and at the LICS conference [Reynolds, 2002].

“Today, the core definitions of Separation Logic may appear as the obvious thing to write, or even as the only thing that would make sense to write. Perhaps the best way to truly value the contribution of Separation Logic is to realize that, following the introduction of the first program logics in the late sixties [Floyd, 1967; Hoare, 1969; Dijkstra, 1975], people have tried for 30 years to verify programs without Separation Logic.”如今，分离逻辑的核心定义看似是理所当然的表述，甚至可能是唯一合理的表述。要真正理解分离逻辑的贡献，或许最好的方式是认识到：自上世纪六十年代末首批程序逻辑提出以来[Floyd, 1967; Hoare, 1969; Dijkstra, 1975]，人们在没有分离逻辑的情况下尝试进行程序验证已长达三十年。 (Charguéraud, 2023, p. 7)

Motivation

对于堆上的数据结构，如果仅使用谓词逻辑进行描述会非常复杂，难以scale。究其原因，通常对这类程序进行分析时，往往需要对数据结构间的共享 Sharing/别名 Aliasing情况进行限制，譬如：

$$\begin{gathered} (\exists \alpha ,\beta .\text{list}\alpha i\wedge \text{list}\beta j\wedge {\alpha }_0^{†}={\alpha }^{†}\cdot \beta ) \\ \wedge (\forall k.\text{reach}(i,k)\wedge \text{reach}(j,k)\Rightarrow k=\text{nil}), \end{gathered}$$

其中的reach是归纳定义的谓词。公式的后一部分表示i和j代表的链表不相交。

除了所关心的结构本身是否共享内存，一个严谨的证明还需要对程序没有涉及到的堆的其他位置的情况进行刻画。比如，通常这些内存地址应该不变：

$$\begin{array}{rl}& (\exists \alpha ,\beta .\text{list}\alpha i\wedge \text{list}\beta j\wedge {\alpha }_0^{†}={\alpha }^{†}\cdot \beta )\wedge \text{list}\gamma x\\ & \wedge (\forall k.\text{reach}(i,k)\wedge \text{reach}(j,k)\Rightarrow k=\text{nil})\\ & \wedge (\forall k.\text{reach}(x,k)\wedge (\text{reach}(i,k)\vee \text{reach}(j,k))\Rightarrow k=\text{nil}).\end{array}$$

分离逻辑可以解决上述问题，关键点在于这些情况均可用堆的「分离」刻画，且分离逻辑公式可以从堆的局部属性出发。

“The main difficulty is not one of finding an in-principle adequate axiomatization of pointer operations; rather there is a mismatch between simple intuitions about the way that pointer operations work and the complexity of their axiomatic treatments…when there is aliasing, arising from several pointers to a given cell, an alteration to a cell may affect the values of many syntactically unrelated expressions.” CSL’01

“主要难点并不在于找到指针操作在原则上完备的公理化描述，而在于指针运作方式的直观理解与其公理化处理的复杂性之间存在脱节……当出现多个指针指向同一存储单元的别名现象时，对单元的修改可能会影响许多语法上无关的表达式的值。”

Assertion Language

Syntax

在FOL的基础上增加：

Syntax	Intention
emp	empty heap
$e\mapsto e$	singleton heap
$p\ast p$	separating conjunction	分离与
$p⊸p$	separating implication	分离蕴涵

它们用于Structural Assertion (与Logical/Boolean Assertion区分）.

Semantics

对堆的建模有多种方式，比如可以假设堆地址和变量值不在一个domain。这里假设堆的地址都是整数（好处是可以支持指针算术运算），即

• Addresses $\subseteq$ Integers $\subseteq$ Values
• Heaps = ${\bigcup }_{A\subseteq Addresses}^{\text{fin}}(A\to \text{Values})$

此时程序的状态由标准的store s以及堆h组成。可以类似地在其上定义程序的小步操作语义，不过需要注意的是，对内存的load和store都需要先在s上求地址的值，如果这个值不是一个地址（不属于Addresses），程序abort。

上述语义的一个重要性质在于对堆进行限制后的执行。如果被排除的地址被解引用或释放，则程序abort，否则限制下的执行不更改被排除部分的堆：

• If $⟨c,(s,h)⟩{⇝}^{\ast }\mathbf{abort}$, then $⟨c,(s,h_0)⟩{⇝}^{\ast }\mathbf{abort}$.
• If $⟨c,(s,h)⟩{⇝}^{\ast }(s^{\prime },h^{\prime })$ then $⟨c,(s,h_0)⟩{⇝}^{\ast }\mathbf{abort}$ or $⟨c,(s,h_0)⟩{⇝}^{\ast }(s^{\prime },h_0^{\prime })$, where $h_0^{\prime }\perp h_1$ and $h^{\prime }=h_0^{\prime }\cdot h_1$.
• If $⟨c,(s,h)⟩\uparrow$ then either $⟨c,(s,h_0)⟩{⇝}^{\ast }\mathbf{abort}$ or $⟨c,(s,h_0)⟩\uparrow$.

分离与

$[p_0\ast p_1{]}_{\text{asrt}}sh\text{ iff }\exists h_0,h_1.h_0\perp h_1\text{ and }{h}_0\cdot h_1=h\text{ and }[p_0{]}_{\text{asrt}}s{h}_0\text{ and }[p_1{]}_{\text{asrt}}s{h}_1,$

分离与和逻辑与的区别：

1. $x\mapsto 3,y\ast y\mapsto 3,x$:
2. $x\mapsto 3,y\wedge y\mapsto 3,x$:

这种差异来源于$e\mapsto e$刻画的并不是全局的性质，而是局部性质：其模型h必须是只包含一个特定地址(s e)。如果对堆的其它位置没有约束，可以写作$e\mapsto e\ast true$，或者用语法糖写作$e\hookrightarrow e$

分离蕴涵

$[p_0⊸p_1{]}_{\text{asrt}}sh\text{ iff }\forall h^{\prime }.(h^{\prime }\perp h\text{ and }[p_0{]}_{\text{asrt}}s{h}^{\prime })\text{ implies }[p_1{]}_{\text{asrt}}s(h\cdot h^{\prime }).$

常见性质

分离逻辑是一种Substructural Logic.

1. 分离与有结合律、交换律，但没有Weakening和Contraction
2. emp是分离与的单位元
3. 分离与对析取有分配律，对合取只有一侧成立$(p_1\wedge p_2)\ast q\to (p_1\ast q)\wedge (p_2\ast q)$

满足特定条件的分离逻辑公式具有更好的性质：

• pure assertion: 不包含emp和$\mapsto$，此时分离与、分离蕴涵和相应的逻辑连接词等价
• intuitionistic assertion: 如果h满足，则h的扩展h’也满足
• strictly exact assertion: 公式在给定s下只被一个h满足

Specification Language

使用分离逻辑作为断言语言的Hoare Logic，此时三元组额外要求程序执行中不会abort

此时，霍尔逻辑中的Constancy规则（在结论的前后置条件都逻辑与上一个公式）不再可靠，取而代之的是重要的Frame规则：

$$\frac{\{p\}c\{q\}}{\{p\ast r\}c\{q\ast r\}}$$

where no variable occurring free in r is modified by c ($mod(c)\cap fv(r)=\varnothing$).

Frame规则的重要性在于允许使用局部的规约：

To understand how a program works, it should be possible for reasoning and specification to be confined to the cells that the program actually accesses¹. The value of any other cell will automatically remain unchanged

“When working in separation logic, specifications like {P} e {Q} are generally stated in a “small footprint” style where P mentions only the state e relies on for its execution. This intuition is backed by the celebrated frame rule, which says that if {P} e {Q} holds, any disjoint state is unaffected, namely {P ∗ F } e {Q ∗ F }.” (Chajed, 2022, p. 30)

特别地，分离逻辑的局部规约同时也保证了对堆的完全所有权，即在逻辑层面保证了不会有其他指令/部分对堆进行修改。实际上，分离与不仅可以表示堆的分离，也可以表示“资源”的分离——分离逻辑非常适合用于并发场景，见Concurrent Separation Logic

Related

• 数理逻辑
• 15-818A3 Introduction to Separation Logic
• SF 第6卷

Footnotes

1. memory footprint ↩