第五章ProofGrid 分布式证明

概述

ProofGrid是 JasperGold 的分布式证明管理系统，可以将证明任务分发到本地机器或服务器集群（Server Farm）上并行执行，大幅缩短证明时间。

ProofGrid 基础概念

Server Farms

JasperGold Apps 支持以下配置：IBM Platform LSF、Oracle Grid Engine（OGE）、Runtime NetworkComputer（NC），以及 shell 脚本方式。

• Platform LSF 模式：不需要带 -I 的交互队列
• OGE 模式：使用 qsub 而不是 qrsh
• 自定义 shell：需要 wait-and-exit 规格，即用 LSF 的 -K 或 OGE 的 -sync yes 指定机器应等待、直到 job 完成才退出

Engine Race

运行属性证明时 JasperGold Apps 会创建 proof job，每个 proof job 对应一个在一个或多个属性上运行的引擎。Engine race 意味着多个引擎（多个 proof job）在同一时间处理同一个属性，彼此竞争。当其中一个引擎得到反例、witness、完全证明或触及某种限制（例如你指定的时间限制）时，竞赛结束，此时所有其他处理该属性的引擎都会停止工作。

Nice Licenses

JasperGold Apps 支持 "nice" 许可证管理：运行优先级较低的 JasperGold Apps 实例，这些实例会把许可证交还给优先级更高的实例。nice 会话在失去许可证时以退出码 5 退出，你可以据此写脚本，在许可证可用时重启工具。

ProofGrid Manager GUI

Proof Threads View

显示每个属性的证明线程列表，包括：

• 正在运行的引擎
• 每个引擎的运行时间和状态
• 线程进度

Engine Graph

实时绘制引擎进展曲线：

• Progress indicators：Property Table 中的进度指示
• Plateaus：曲线平坦表示引擎没有新进展
• Spikes：正尖峰表示引擎取得突破
• Spikes / Negative Spikes：对抽象引擎（A*、C、I、K、N）而言，尖峰与负尖峰都是证明进展健康的标志——这些引擎尝试一种抽象、取得进展（尖峰），放弃后转向新的抽象（负尖峰）

Summary View

ProofGrid 运行的总体统计：已证明/失败/运行中的属性数量。

配置指南

Per-Property Time Limit

set_prove_per_property_time_limit 60s

为每个属性设置合理的时间限制，避免单个属性占用过多资源。

Focused Proof

如果有端到端的高价值断言，考虑为每个这样的属性专门分配一个 proof thread，避免与其他断言共享 proof thread 而损失效率。对这类高价值断言的证明，使用引擎 L、带定制 bug-hunting 设置的引擎 B，以及 B swarm。

# 聚焦属性 P
# 主证明
prove -property P -engine_mode {Ht B K AB AM} -bg

# 引擎 L
prove -property {P cov1 cov2 cov3 ...} -engine_mode L -per_engine_max_jobs 3 -bg

# 引擎 B
set_engineB_trace_attempt_time_limit 300
set_engineB_trace_attempt_time_limit_increment 120
set_engineB_trace_attempt_increment 4
prove -property P -engine_mode B -bg

# B swarm
set_engineB_trace_attempt_time_limit 0
set_engineB_trace_attempt_increment 10
prove -property P -engine_mode B -bg -first_trace_attempt 16
prove -property P -engine_mode B -bg -first_trace_attempt 18
prove -property P -engine_mode B -bg -first_trace_attempt 20

配置命令

# 指定 proof engine job 在哪种 grid 上运行
# 可选值：local | shell | lsf | oge | nc | cluster
set_proofgrid_mode lsf

# 设置并行任务数（默认 0 表示不限）
set_proofgrid_max_jobs 16

# 每个引擎的最大 job 数
set_proofgrid_per_engine_max_jobs 3

# 指定不会被交还的特权许可证数量（其余默认为 nice）
set_proofgrid_per_engine_privileged_jobs 5

# 启用 ProofGrid Manager（默认关闭）
set_proofgrid_manager on

其他常用的 ProofGrid 相关命令还有：set_proofgrid_cluster、set_proofgrid_extra_args、set_proofgrid_max_local_jobs、set_proofgrid_pending_time_limit、set_proofgrid_restarts、set_proofgrid_shell、set_proofgrid_skip_abandoned、set_proofgrid_socket_communication，以及 prove -per_engine_max_jobs。

使用流程

1. 配置 ProofGrid 参数（服务器、任务数、时间限制）
2. 启动证明（prove -all）
3. 在 ProofGrid Manager 中监控进度
4. 观察 Engine Graph，识别出现 plateau 的引擎——即长时间无法推进到新的 trace attempt
5. 按文档给的两种情形处置：
   • 有别的引擎跑得更好 → 停掉停滞的那个，让进展好的继续。文档举的例子是 Ht 停在 trace attempt 49、而 B 进展更好，此时应当停 Ht 留 B
   • 所有引擎都推不动 → 先估算按当前速度到达目标 bound 还要多久；如果不现实，就停掉证明，改用抽象、mutation 等手段之后再重启。文档举的例子是引擎 K 停在 64、目标 bound 是 100，算下来时间不可接受

ProofGrid 分布式证明界面

ProofGrid 分布式证明方法论

什么时候需要 ProofGrid

单机证明遇到以下情况时考虑 ProofGrid：

• 属性数量大（几百上千个），单机串行跑太慢
• 单个属性就需要很长时间（小时级）
• 项目回归周期短，需要快速跑完所有证明
• 有多个 CPU 核/服务器可用

ProofGrid 的工作原理

ProofGrid 用来在本地机器、server farm 或主机集群上派生多个 proof engine job。它的并行模型不是"把属性列表切分给各节点"，而是围绕 engine race 组织的：

1. 运行属性证明时，工具创建多个 proof job，每个 job 对应一个在一个或多个属性上运行的引擎
2. 多个引擎在同一时间处理同一个属性，互相竞争
3. 某个引擎率先得到反例、witness、完全证明或触及限制时，竞赛结束
4. 此时所有其他处理该属性的引擎都停止工作，资源转向其余属性

随着许可证变得可用，ProofGrid 会动态增加 job 数量直到你设定的上限；如果你调低 job 上限，工具也会相应地交还许可证。proofgrid_max_jobs、proofgrid_per_engine_max_jobs 以及可用许可证数量共同限制 ProofGrid 能启动的 job 数。若 engine_mode 列表中的引擎数超过当前的 proofgrid_max_jobs，工具会忽略超出的引擎并发出警告。

使用策略

• 优先让 Proof Orchestration 处理：默认设置下最多使用 2 个许可证（local 模式为 1）和 10 个 job（local 模式为 4）
• 对高价值断言用 Focused Proof：为每个端到端断言专门分配一个 proof thread，避免与其他断言共享而损失效率
• Proof Threads View：查看 ProofGrid 状态，了解哪些引擎在处理哪些属性、以及它们随时间的进展
• Engine Graph：观察 plateau 与 spike，判断各引擎的进展是否健康