设计保证与可信性模型
July 22, 2026 · View on GitHub
GhostScope 把运行中程序的机器状态转换为源码感知的观测结果。本文档定义这些结果在什么条件下应当可信,以及实现必须持续维护哪些不变量。
这是一份规范性的设计契约。架构文档说明当前实现如何保证这些不变量,使用限制说明支持范围之外或会显式降级的行为。未来才准备提供的保证应写入未来规划,而不是本文档。
在支持范围内违反不变量属于正确性缺陷,而不是“使用限制”。项目处于早期开发阶段意味着仍可能存在缺陷,但不能因此让已知的不支持路径返回看似合理、实际没有证据的数据。
支持范围
- 官方发布产物和正确性测试面向 Linux x86_64。运行时构建会拒绝其他构建目标,trace setup 也会拒绝不是 64 位小端 x86_64 ELF 的目标文件。
- 源码级值依赖与目标模块对应的 DWARF。内嵌 DWARF 直接来自目标模块;独立调试文件默认严格检查可用的
.gnu_debuglinkCRC 和 Build ID 证据。 - C 语言的端到端覆盖最完整。C++ 仍主要按 DWARF 布局访问;Rust 则在 验证目标 DWARF 后,为部分标准库类型提供语义适配。当前覆盖范围见 源语言支持现状,能力边界见 使用限制。
- 内核必须提供所需的 eBPF、uprobe 和事件传输能力,GhostScope 也必须具备使用这些设施的权限。
--allow-loose-debug-match 会显式退出独立调试文件的严格匹配。启用后 GhostScope 会对不匹配发出警告,但用户同时也削弱了源码语义解释所依赖的证据。如果一个显式指定的调试文件既没有可用 CRC,也没有可比较的 Build ID,系统同样无法证明它与目标模块一致;相应 warning 表示这成为用户提供的信任假设,不属于严格证据范围。
信任边界
GhostScope 依赖 Linux 内核、eBPF verifier 和 helper、目标模块及编译器生成的 DWARF,以及 /proc 暴露的进程信息。系统会尽可能验证并缩小这些输入的范围,但无法证明编译器生成的 DWARF 在语义上一定正确。
一个事件表示 uprobe 命中时的一次瞬时观测,而不是整个进程的原子快照。寄存器和当前线程栈帧对应命中时刻;在一个事件依次采集多个字段期间,其他线程仍可能修改共享内存。
只读也不等于零影响。Linux uprobe 会安装 trap 点,目标线程每次命中时会同步承担 uprobe 和 eBPF 的执行开销。GhostScope 不会像调试器一样控制目标暂停,也不会主动写入应用状态,但不能保证运行时序完全不变。
不变量
SCOPE-1:支持平台必须明确
保证。 官方构建和正确性声明的范围是 Linux x86_64。
保证机制。 platform crate 使用 Linux x86_64 编译期守卫,使运行时构建在其他目标上失败;安装器拒绝不支持的主机或请求架构;trace setup 在语义解释前验证 -t 目标、-p 进程可执行文件和实际加载的 DWARF 模块。发布产物按 x86_64 构建和命名,架构相关的寄存器、ABI、TLS 与 unwind 行为也在该环境中验证。
失败边界。 不支持的主机无法构建或安装;不支持的目标文件会在 DWARF 解释或 uprobe 附加之前让 setup 失败。在完成平台映射和端到端测试之前,其他架构不能被描述为已支持。
SAFE-1:观测不能控制目标程序
保证。 GhostScope 不提供主动修改应用可见变量、内存或控制流的操作,也不会为了交互式检查、单步或继续执行而暂停进程。
保证机制。 脚本语言只提供观测能力,生成的 eBPF 程序使用目标读取、内部 map 和事件输出操作,内核 verifier 对加载程序施加约束。
失败边界。 Uprobe trap 和 eBPF 执行仍然会扰动调度和延迟。任何写入目标内存或改变控制流的能力都会改变这份契约,不能作为普通追踪功能引入。
IDENT-1:每个观测结果必须符合请求的目标范围
保证。 每个事件必须能够归属于产生它的 trace 和运行时目标范围。当请求的 PID、模块或地址空间解释不可用时,GhostScope 不能静默改用另一个范围。
启动模式定义了目标范围:
-p <pid>选择该进程及其已加载模块形成的进程视图。-t <path>选择以目标模块为中心的多进程视图。-t <path> -p <pid>在指定模块内解析 trace 目标,并把运行时事件限定到指定进程。
保证机制。 Trace ID、PID/TID 元数据、PID 过滤、感知 PID namespace 的进程发现、模块 Cookie 和运行时模块偏移,把身份信息贯穿附加、采集和展示过程。
失败边界。 无法观察进程、缺少模块映射或目标存在歧义时,必须让 setup 失败,或者明确标记依赖该信息的语义操作不可用,不能回退到无关范围。
SEM-1:源码语义必须具有完整证据链
保证。 只有在目标模块和 probe PC 能够连接到适用的 DWARF 作用域、类型、位置以及运行时读取计划时,GhostScope 才会展示源码级值。
证据链为:
目标范围 -> 运行时模块 -> 模块内 PC -> DWARF 作用域/类型/位置
-> 类型化读取计划 -> 运行时读取结果 -> 展示结果
保证机制。 严格调试文件匹配、模块感知的 PC 上下文、ASLR/PIE 重定位、词法与 inline 作用域解析、类型化 lowering 和运行时读取状态,共同保持每一步的含义。
失败边界。 任意一步无法成立时,GhostScope 必须报告不支持的位置、OptimizedOut、读取错误、ExprError 或其他明确的不可用状态。不能改用其他作用域里的同名变量,不能猜测地址,也不能把未验证的值展示为有效值。
FAIL-1:已知的不确定性必须显式呈现
保证。 已知的编译、附加、读取、unwind、解析或归因失败,必须对用户或自动化调用方保持可见。
保证机制。 Setup 和 lowering 失败以错误返回;运行时表达式与内存读取失败使用结构化协议状态;调用栈使用带原因的 complete、truncated 和 stopped 状态。
失败边界。 Best-effort 行为只有在缺失部分被明确标记时才能返回部分结果。仅记录 warning,同时输出一个看似完整但并不受支持的值,不满足这个不变量。
LOSS-1:可检测的事件丢失不能静默发生
保证。 Trace 成功启动不代表事件流无损。当 eBPF 输出 helper 拒绝事件时,GhostScope 会按 trace 统计失败次数,并向 CLI 和 TUI 用户报告区间增量与累计丢失量。
保证机制。 RingBuf 或 PerfEventArray 输出失败时,生成的程序会更新丢失计数;运行时定期读取并报告这些计数。
失败边界。 这些计数覆盖内核输出 helper 的失败。它们不能说明具体丢失了哪些事件,也不能证明该计量点之外没有丢失,例如附加之前或关闭之后的事件。任何非零报告都表示对应观测区间不完整。
COST-1:单事件工作量必须有界,总体影响取决于负载
保证。 生成的 eBPF 执行、trace 事件大小、内存读取和 backtrace 深度,都受到 verifier 兼容限制或可配置上限约束。达到语义或资源边界时,必须拒绝 trace,或者产生明确的截断/不可用状态。
保证机制。 编译器限制事件大小和读取范围,verifier 检查 eBPF 控制流,传输层具有配置容量,DWARF unwind 使用深度和 tail-call 预算。
失败边界。 GhostScope 不承诺固定的总体开销。即使单次执行有界,把探针放在热点路径上仍可能显著拖慢目标。操作方必须把命中频率和每次事件负载纳入开销预算。
结果状态
这些不变量导出四种不同结果:
| 结果 | 含义 |
|---|---|
| 完整 | 请求的操作在支持范围内完整执行。 |
| 显式部分结果 | 部分请求数据不可用或被截断,事件携带相应状态。 |
| 拒绝 | Setup、编译、验证或附加过程无法建立所需条件。 |
| 事件流不完整 | 检测到一个或多个事件丢失;已收到的事件仍可能有效,但对应区间并不完整。 |
这些状态不能被合并成一个笼统的成功路径。
验证要求
测试是这份契约的证据,而不是契约本身的定义。当前主要证据分布如下:
| 不变量 | 主要证据 |
|---|---|
SCOPE-1 | x86_64 release workflow、平台相关单元测试、安装器拒绝和不支持目标 ELF 测试 |
SAFE-1 | 脚本/编译器操作面、eBPF helper 使用范围、经过 verifier 的加载测试 |
IDENT-1 | PID 专属执行测试和容器拓扑测试 |
SEM-1 | PC 上下文、标量、全局变量、优化代码和跨模块 fixture 的精确值 oracle |
FAIL-1 | 编译错误、OptimizedOut、ExprError、读取失败和 backtrace 状态测试 |
LOSS-1 | eBPF 输出失败计数与 CLI/TUI 报告链路;修改这条路径时必须补充压力覆盖 |
COST-1 | 编译器边界检查、经过 verifier 的加载、配置深度和深栈 backtrace 测试 |
修改目标选择、进程身份、模块/PC 映射、DWARF lowering、生成的 helper、事件协议、传输层或展示逻辑时,验证说明应指出受影响的不变量,并提供一个正向 oracle 和一个相关失败路径 oracle。