Page 81 - 《软件学报》2025年第8期

3504 软件学报 2025 年第 36 卷第 8 期

证各个 GhostFunc 中都保证所有权, 生命周期等性质. 并且在验证出现问题时, 可分离出来进行排查验证. 我们在
本节用例子简单介绍 GhostFunc 状态和部分不变式性质.
为了清晰描述每个 GhostFunc 操作, 首先需要定义该 GhostFunc 系统的状态. 这里还是以 GhostArc 的系统状
态为例介绍. 状态的定义包括如下引用计数、数据、所有权、锁的状态等.
对于每个 GhostFunc, 内部都有部分的操作的接口, 我们在 GhostFunc 中证明操作的正确性, 因为在 unsafe
code module 中已经进行证明, 但仍需定义操作的前后置条件, 第一是为了更好地衔接 safe code module, 第二是在
Coq 中的实际证明中, 我们发现如果在上下文不完整的情况下, 编译选项会变得十分复杂和冗余, 给验证造成较大
的困扰. 同时我们显式地定义 Arc 的操作为 GhostArcOp 来描述 GhostArc 对外的接口.
下面 Coq 代码是以 GhostArc 中 clone 操作的前后置条件等为例介绍.
Record State(T : Type) : Type := {
ref_count : nat;
data : T;
ownership : gmap nat nat;
is_locked : bool;
}.
…
Inductive GhostArcOp(T : Type) : Type :=
| Clone(s : State T) : GhostArcOp T
| Drop(s : State T) : GhostArcOp T
| New(s : State T) (tid_src tid_dst : nat) : GhostArcOp T.
…
Definition pre_clone(s : State T) : iProp Σ :=
⌜s.ref_count > 0⌝.
Definition post_clone(s s' : State T) : iProp Σ :=
⌜s'.ref_count = s.ref_count + 1 ∧
s'.data = s.data ∧
s'.ownership = s.ownership ∧
s'.is_locked = s.is_locked⌝.
其中, State 为我们定义的 GhostArc 状态: ref_count 为引用计数, data 为数据, ownership : gmap 为拥有数据的线程
id 到引用计数的映射. 后面归纳定义 3 个对外操作的接口. 定义的 pre_clone 和 post_clone 分别为 clone 操作的前
后置条件, 前置条件为当前状态 s 的引用计数 s.ref_count 大于 0, 确保了对象可以被有效克隆, 也保证了 safe 代码
部分能够合理使用该 GhostFunc. 后置条件, 即被克隆后应满足应用计数增加、数据不变、所有权不变、锁定状
态不变, 实际上我们整个验证中, 并未涉及所有权转移的操作.
之后, 我们显式地定义 GhostArc 的接口.

Definition ghost_arc_clone(γ : gname) (s : State T) : iProp Σ :=
∃ s', ⌜pre_clone s⌝ ∗

⌜post_clone s s'⌝ ∗
own γ(· (Excl' s')) ∗
inv γ(valid_ref_count s' ∗ valid_ownership s' ∗ valid_locked s').

其中, γ : gname 是 GhostArc 对象的全局名称, 用于标识具体的 Arc 实例. s : State T 是当前的状态. pre_clone s 是克