From 077cd0b8029b662cedc94a01f803007974132c2b Mon Sep 17 00:00:00 2001 From: DslsDZC Date: Tue, 11 Aug 2026 18:25:24 +0800 Subject: [PATCH 1/2] =?UTF-8?q?docs:=20=E5=9B=BE=E9=94=9A=E5=AE=9A?= =?UTF-8?q?=E5=8C=BA=E5=9F=9F=E5=86=85=E5=AD=98=E6=A8=A1=E5=9E=8B=E8=AE=BE?= =?UTF-8?q?=E8=AE=A1=EF=BC=88graph-anchored=20regions=EF=BC=89=E2=80=94?= =?UTF-8?q?=E2=80=94=E4=BF=9D=E7=95=99=E7=AB=9E=E6=8A=80=E5=9C=BA=E5=8F=8C?= =?UTF-8?q?=E4=BB=B7=E5=80=BC=EF=BC=88=E9=9B=B6=E7=A2=8E=E7=89=87/?= =?UTF-8?q?=E6=9C=89=E7=95=8C=E7=A2=8E=E7=89=87=EF=BC=89=EF=BC=8C=E5=8C=BA?= =?UTF-8?q?=E5=9F=9F=E9=94=9A=E5=AE=9A=E6=95=B0=E6=8D=AE=E6=B5=81=E5=9B=BE?= =?UTF-8?q?=EF=BC=8C=E4=BA=94=E6=9C=BA=E5=88=B6=EF=BC=88=E7=94=9F=E5=91=BD?= =?UTF-8?q?=E5=91=A8=E6=9C=9F/=E5=B8=83=E5=B1=80/=E6=94=BE=E7=BD=AE/?= =?UTF-8?q?=E7=A2=8E=E7=89=87/=E8=B7=A8=E5=8C=BA=E5=9F=9F=EF=BC=89?= =?UTF-8?q?=E5=85=A8=E9=83=A8=E5=9B=BE=E5=86=85=E5=8C=96=EF=BC=8C=E7=94=A8?= =?UTF-8?q?=E6=88=B7=E9=9D=A2=E9=9B=B6=E7=AE=A1=E7=90=86=E8=B4=9F=E6=8B=85?= =?UTF-8?q?=EF=BC=9B=E6=9C=AC=E9=98=B6=E6=AE=B5=E5=8F=AA=E6=94=B9=E6=96=87?= =?UTF-8?q?=E6=A1=A3=E4=B8=8D=E5=AE=9E=E7=8E=B0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...026-08-13-graph-anchored-regions-design.md | 165 ++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 docs/superpowers/specs/2026-08-13-graph-anchored-regions-design.md diff --git a/docs/superpowers/specs/2026-08-13-graph-anchored-regions-design.md b/docs/superpowers/specs/2026-08-13-graph-anchored-regions-design.md new file mode 100644 index 0000000..0594ac1 --- /dev/null +++ b/docs/superpowers/specs/2026-08-13-graph-anchored-regions-design.md @@ -0,0 +1,165 @@ +# 图锚定区域内存模型设计（Graph-Anchored Regions） + +## 概述 + +在现有 Arena 内存模型（`docs/memory-model.md` + `docs/superpowers/specs/2026-07-28-arena-model-design.md`）**基础上修改**，不发明新模型。 + +核心命题：**区域（Region）锚定在数据流图上**——区域是子图节点的字节域，不是词法作用域的影子。传统区域内存管理（Tofte-Talpin 区域栈、Cyclone、Verona）全部锚定词法作用域（LIFO 嵌套）；Core 的执行模型是数据流图，区域应该与图同构。 + +保留 Arena 的两个核心价值（放弃它们的代价，不可接受）： +1. **无碎片**——静态已知大小的分配路径保持纯 bump +2. **动态模式下工程可控的极低碎片**——动态大小分配路径走分档子区域，浪费上界由 size class 表决定 + +用户面**零内存管理负担**：区域划分、生命周期、回收时机、碎片策略、跨区域合法性全部由图自动推导/验证。用户只表达两件只有用户自己知道的事实：布局（逃生门）与放置（地址声明）。 + +## 设计动机 + +### 论文依据 + +| 论文 | 结论 | 对 Core 的意义 | +|------|------|---------------| +| Tofte & Talpin, *Region-Based Memory Management* (POPL'94 / I&C 1997) | 存储 = 区域的栈；区域分配/回收点由类型-效果分析自动推断；形式化可靠性证明。已知弱点：区域活得太久导致内存泄漏 | 自动推断可行且可证；泄漏弱点 → 需要显式提前释放（见 Cyclone） | +| Gay & Aiken, *Memory Management with Explicit Regions* (PLDI'98)；*Language Support for Regions* (PLDI'01) | 显式区域与 malloc/free 性能相当；区域子类型（outlives）；多级区域层次；**提前释放是工程可用的关键** | "指定回收"作为编译器内部机制（IR 层生成回收点），不暴露语法 | +| *Reference Capabilities for Flexible Memory Management* (OOPSLA'24, Verona 线) | 区域 = dominator scope，内部对象同生共死；内存按区域局部管理；底层 snmalloc = 分档 bump 分配（size class） | size class 是动态碎片控制的工程标准答案 | +| Leroy et al., *The CompCert Memory Model, Version 2* (2012) | 块 + (块 ID, 字节偏移) 指针；**每字节权限**（Freeable > Writable > Readable > Nonempty > Empty）；`loadbytes`/`storebytes`；块按构造分离；Coq 机器验证 | 每字节权限层 = 语义面（验证器）的范式 | + +### 与传统模型的差异 + +传统模型锚定词法作用域：区域随函数/块进入而创建，退出而回收（LIFO）。Core 的区域锚定图结构： + +``` +传统（词法锚定）： Core（图锚定）： +fn f() { ┌─ SG_IF ─┐ + let x = ...; ← 区域 = 词法块 │ ┌─────┴─────┐ + ... │ branch1 branch2 +} ← LIFO 弹出 │ └─────┬─────┘ + │ join + └────────┘ + 区域 = 子图节点，生命周期 = 图活性 +``` + +## 核心概念：图锚定区域 + +区域 = 子图节点（DFNode）的字节域。现有设计的「每个 DFNode 可关联一个 Arena」「子图绑定」「Arena 嵌套」原样继承，概念升级为区域。 + +### 推论 A：生命周期 = 图活性，不是 LIFO + +RegionCheck 的 `cur_seq < exit_seq` 判定（pointer-model.md Pass 2）就是图版本的生命周期定义。这天然支持 flow/go 的独立区域（区域栈做不到非 LIFO 生命周期），也天然给出跨区域引用的合法性判据（outlives 的图形式）。 + +### 推论 B：区域操作沿图边 + +区域不仅嵌套（树），还能沿数据流边操作： + +- **split**：一块字节沿边划给子消费者（= 字节块独立回收；子区域 = 图边的子块，自己的游标 + 自己的重置点） +- **merge**：汇合点两个子区域的数据汇入（拷贝或区域合并） +- **share**：分叉点一个区域被多个消费者只读共享（共享者必须 outlive 引用） + +### 推论 C：每字节归属 = 图的 provenance 边 + +pointer-model.md 已定义记忆模型为「字节序列 + 宽度 + 边界」，provenance（归属）、offset（字节偏移）、alloc_size（字节大小）全部与类型无关。"控制每一个字节"不是新语法，是图上本来就有的信息。 + +### 与传统的关系 + +区域树是图区域的特例（无汇合/分叉的图 = 树 = 词法嵌套）；Tofte-Talpin 的区域栈是更窄的特例（树 + LIFO）。本设计是推广，不是发明。 + +### 术语注意 + +dataflow 模块已有「region」一词指控制流嵌套（SG_IF/LOOP/FOR/FLOW/UNSAFE）。本文的「区域」指**内存字节域**。文档中按上下文区分；若需精确，内存区域全称「内存区域」。 + +## 机制总图 + +| # | 需求 | 图上的机制 | 验证/推导者 | +|---|------|-----------|-----------| +| 1 | 字节块独立回收 | 区域 = 子图节点；子区域 = 沿图边 split；显式提前释放（回收点）由 IR 层生成；merge/share 处理汇合/分叉 | 图活性（RegionCheck） | +| 2 | 逐字节布局 | **布局元数据进图**：字段字节偏移/packed/对齐，后端与验证器同一来源（语义保鲜） | 编译期计算，图节点存储 | +| 3 | 固定地址放置 | **ALLOC_AT 节点**（地址+大小+对齐）进图，与 ALLOC 同路径获得 provenance | ProvenanceVerify（边界+宽度） | +| 4 | 碎片有界 | **策略推导**：子图全静态大小 → 纯 bump（零碎片）；混动态 → 分档子区域（size class 表由图上分配大小分布推导） | 图分析（大小预计算扩展） | +| 5 | 跨区域 | **outlives 顺序判定**：引用者存活区间 ⊆ 被引用区域存活区间（RegionCheck 现有机制，从"禁止"放宽为"顺序判定"） | RegionCheck | + +不变的三条铁律： + +1. 静态已知大小路径 = 纯 bump，**零碎片** +2. 动态路径 = 分档子区域，**浪费上界由 size class 表决定**（工程可控：档位越细上界越低，如 pow2 档 ≈50%、细分档 ≈12.5%） +3. Arena Pool / 嵌套 / 子图绑定 = 原样继承，概念升级为"区域" + +## 用户面（零管理负担） + +用户零参与、全部由图推导的事项： + +| 事项 | 谁做 | +|------|------| +| 区域划分/生命周期 | 图活性推导（子图边界即区域） | +| 回收时机（含"指定回收"需求） | 图分析生成回收点——推断在编译器内部完成，用户看不到 | +| 碎片策略 / size class | 图分析推导分配策略 | +| 跨区域合法性 | RegionCheck 自动判定 | +| 所有验证 | 三点 pass 自动 | + +用户只表达两件只有用户自己知道的事实： + +```core +// 1. 布局声明（逃生门）——默认布局全自动：编译器按类型推导自然布局 +// （字段顺序 + 自然对齐），用户不写任何东西。 +// layout(...) 仅当默认布局不合用时才需要：packed（FFI）、强制对齐、硬件结构。 +struct PackedHeader layout(packed, align(4)) { + a: u8, // 偏移 0 + b: u32, // 偏移 4 + c: u16, // 偏移 8 +} + +// 2. 放置声明——地址是物理事实，只有用户知道。 +// 声明式进图（地址+大小+对齐），之后全图追踪，ProvenanceVerify 照常验证。 +mmio := alloc_at(0x7fff0000, 4096, align(4096)); +``` + +- v1 **不提供**显式区域/回收语法（YAGNI）。「指定回收」是编译器内部机制（IR 层生成回收点 = Cyclone early deallocation 的自动版）。 +- 与 pointer-model.md 2026-08-10 定论的关系：0x 字面量仍是 unsafe 外部入口；`alloc_at` 是**声明式进图**（获得 provenance 的节点），不冲突——声明是唯一信任点，之后全图追踪。 + +## 语义面（验证器） + +内存模型 = 图 + 字节权限层（CompCert v2 范式）： + +- 每字节内容 = 字节序列（已有） +- 每字节权限 = **Freeable > Writable > Readable > Nonempty > Empty**（新加） +- 区域树 = 图的子图结构；布局元数据、ALLOC_AT 边界、outlives 结论全部从图导出——**验证器消费图即消费全部内存语义** +- 前置缺口：宽度检查（`off + width <= alloc_size`）待补（对应 TODO 预存 bug 7） + +## 分配器面（实现） + +现有 2026-07-28 arena 实现设计（arena pool、bump 双路径、链式扩容、子图绑定、大小预计算）**原样继承**，作为区域的实现层： + +| 机制 | 实现 | +|------|------| +| 纯 bump 路径（零碎片） | 现有 arena_new/arena_reset + 大小预计算 | +| 分档子区域（有界碎片） | 池内 size-classed 子分配器（档位表由图分析推导，链式扩容沿用） | +| ALLOC_AT（固定放置） | 固定映射区（mmap/段），不进池 | +| 策略推导 | 图分析输出（大小预计算扩展：全静态 → bump；混动态 → 分档） | + +## 与现有文档的关系 + +| 文档 | 改动 | +|------|------| +| `docs/memory-model.md` | 重写：Arena → 图锚定区域（本设计的语义核心） | +| `docs/pointer-model.md` | 修订：ALLOC_AT 节点、跨区域从"禁止"放宽为 outlives 顺序判定、补字节权限层 | +| `docs/ir-schema/coreir-schema.md` | 补：布局元数据、ALLOC_AT 节点定义 | +| `docs/spec-design.md` | 检查涉内存条目（#no_alloc 等）是否需要同步 | +| `docs/superpowers/specs/2026-07-28-arena-model-design.md` | 保留不动（分配器面实现设计），新设计在其上叠加语义层 | + +## 本阶段范围 + +**只改文档，不实现**（用户明确指示）。交付物 = 上述文档改动。 + +## 后续实施方向（不在本阶段） + +| 里程碑 | 内容 | 前置 | +|--------|------|------| +| M1 生命周期+碎片 | memory-model.md 重写落地；子区域 split；IR 层回收点生成；size class 策略推导 | 现有 arena 基础；TODO 预存 bug 5（arena 运行时死循环）为阻塞项 | +| M2 布局+放置 | 布局元数据进图（IR schema）；ALLOC_AT 节点；ProvenanceVerify 宽度检查 | M1；接 TODO 预存 bug 7 | +| M3 跨区域 | RegionCheck 从"禁止"放宽为 outlives 顺序判定；pointer-model.md 逃逸规则修订 | M1/M2 | + +## 参考 + +- Tofte & Talpin, *Region-Based Memory Management*, POPL'94 / Information and Computation 132(2), 1997 — [ACM](https://dl.acm.org/doi/10.1006/inco.1996.2613) +- Gay & Aiken, *Memory Management with Explicit Regions*, PLDI'98 — [ACM](https://dl.acm.org/doi/10.1145/277652.277748) +- Gay & Aiken, *Language Support for Regions*, PLDI'01 — [ACM](https://dl.acm.org/doi/abs/10.1145/378795.378815) +- *Reference Capabilities for Flexible Memory Management*, OOPSLA'24（Verona 线）— [arXiv:2309.02983](https://arxiv.org/pdf/2309.02983) +- *The CompCert Memory Model, Version 2* — [Semantic Scholar](https://www.semanticscholar.org/paper/The-CompCert-Memory-Model%2C-Version-2-Leroy-Appel/a90495f9f586298a7424df15fb1308b42a373b5a) From 22b8c3520dbb25e4453492671e2d41596b1b3360 Mon Sep 17 00:00:00 2001 From: DslsDZC Date: Thu, 13 Aug 2026 19:54:57 +0800 Subject: [PATCH 2/2] =?UTF-8?q?docs:=20=E5=9B=BE=E9=94=9A=E5=AE=9A?= =?UTF-8?q?=E5=8C=BA=E5=9F=9F=E8=AE=BE=E8=AE=A1=E8=90=BD=E5=9C=B0=E2=80=94?= =?UTF-8?q?=E2=80=94memory-model.md=20=E9=87=8D=E5=86=99=EF=BC=88=E5=8C=BA?= =?UTF-8?q?=E5=9F=9F=3D=E5=AD=90=E5=9B=BE=E5=AD=97=E8=8A=82=E5=9F=9F/?= =?UTF-8?q?=E5=9B=BE=E6=B4=BB=E6=80=A7=E7=94=9F=E5=91=BD=E5=91=A8=E6=9C=9F?= =?UTF-8?q?/split-merge-share/=E4=BA=94=E6=9C=BA=E5=88=B6/=E5=AD=97?= =?UTF-8?q?=E8=8A=82=E6=9D=83=E9=99=90=E5=B1=82/=E7=94=A8=E6=88=B7?= =?UTF-8?q?=E9=9D=A2=E9=9B=B6=E7=AE=A1=E7=90=86=EF=BC=89=EF=BC=9Bpointer-m?= =?UTF-8?q?odel.md=20=E4=BF=AE=E8=AE=A2=EF=BC=88ALLOC=5FAT=20=E5=A3=B0?= =?UTF-8?q?=E6=98=8E=E5=BC=8F=E6=94=BE=E7=BD=AE=E3=80=81=E8=B7=A8=E5=8C=BA?= =?UTF-8?q?=E5=9F=9F=E6=94=BE=E5=AE=BD=E4=B8=BA=20outlives=E3=80=81?= =?UTF-8?q?=E5=AD=97=E8=8A=82=E6=9D=83=E9=99=90=EF=BC=89=EF=BC=9Bcoreir-sc?= =?UTF-8?q?hema=20+=20spec-design=20=E5=90=8C=E6=AD=A5=EF=BC=88ALLOC=5FAT?= =?UTF-8?q?=20=E8=8A=82=E7=82=B9/=E5=B8=83=E5=B1=80=E5=85=83=E6=95=B0?= =?UTF-8?q?=E6=8D=AE/#no=5Falloc=EF=BC=89?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- docs/ir-schema/coreir-schema.md | 31 +++- docs/memory-model.md | 289 ++++++++++++++++++++------------ docs/pointer-model.md | 38 ++++- docs/spec-design.md | 4 +- 4 files changed, 255 insertions(+), 107 deletions(-) diff --git a/docs/ir-schema/coreir-schema.md b/docs/ir-schema/coreir-schema.md index c81e7eb..5521ef9 100644 --- a/docs/ir-schema/coreir-schema.md +++ b/docs/ir-schema/coreir-schema.md @@ -151,6 +151,34 @@ DFNode 覆盖两种节点：普通指令节点（opcode ≤ IR_AWAIT）和规约 | 4 | 4 | kind | 符号类型：0=func, 1=var, 2=type, 3=field | | 8 | 4 | scope | 作用域（函数索引或 -1 表示全局） | +### ALLOC_AT 节点（声明式放置，2026-08-13） + +固定地址放置的声明式进图节点（图锚定区域内存模型，见 `docs/memory-model.md` 机制 #3）： + +| 字段 | 含义 | +|------|------| +| opcode | ALLOC_AT（编号待实现时分配，不与 SPEC_* 冲突为前提） | +| dest_var | 结果指针变量 | +| src1 | 固定地址（编译期常量或部署配置值） | +| src2 | 大小（字节） | +| src3 | 对齐（字节） | +| type_kind | 指向的元素类型 | + +与 ALLOC 同路径获得 provenance；ProvenanceVerify 验证边界+宽度（`offset ∈ [0, size)` 且 `off + width <= size`）。声明是唯一信任点，之后全图追踪。 + +### 布局元数据（Layout Descriptor，2026-08-13） + +struct 类型关联布局描述符。**默认由编译器推导自然布局**（字段顺序 + 自然对齐），用户 `layout(...)` 声明时显式给出（packed/强制对齐/硬件结构逃生门）： + +| 字段 | 含义 | +|------|------| +| packed | 是否紧凑（无填充） | +| align | 整体对齐要求（字节） | +| field_count | 字段数 | +| fields | 每字段：(name_idx, offset, width, align)——name_idx 索引字符串表 | + +布局元数据是**图数据**：后端与验证器消费同一来源（语义保鲜），DEREF 的偏移+宽度检查对着布局走。 + --- ## 三、规约操作码（新增 DFNode opcode） @@ -179,7 +207,7 @@ DFNode 覆盖两种节点：普通指令节点（opcode ≤ IR_AWAIT）和规约 | `#pure` | 函数的所有 DFNode 中：无 CALL 到非纯函数、无 STORE 到外部全局变量 | 无副作用 | | `#deterministic` | #pure + 无依赖于外部状态（IO、env、随机源）的路径 | 确定性 | | `#terminating` | 所有循环（DFNode 中的回边）有可识别的单调递减度量 | 终止性 | -| `#no_alloc` | 无 ALLOC / ALLOC_ARRAY / ALLOC_STRUCT 节点 | 不分配 | +| `#no_alloc` | 无 ALLOC / ALLOC_ARRAY / ALLOC_STRUCT / ALLOC_AT 节点 | 不分配 | | `#no_throw` | 无可达的异常路径（无分支导向 panic/error 节点） | 不抛异常 | | `#safe_index` | 所有 LOAD_INDEX/STORE_INDEX 节点的索引输入 ≤ 数组长度变量 | 安全索引 | | `#len_preserved` | 输入集合变量和输出集合变量之间的 DFNode 无插入/删除操作（STORE_INDEX 不超出边界，无 ALLOC 替换） | 长度守恒 | @@ -269,6 +297,7 @@ store_index_var, make_enum, ref, // 15-17 branch, jump, label, phi, load_enum_tag, // 18-23 slice, deref, store_ptr, // 24-26 spawn, yield, await, // 27-29 +alloc_at, // 编号待实现时分配（声明式放置，2026-08-13） spec_constraint, spec_forall, spec_exists, // 30-32 spec_imply, spec_old, spec_assume // 33-35 ``` diff --git a/docs/memory-model.md b/docs/memory-model.md index 36d58f9..7879998 100644 --- a/docs/memory-model.md +++ b/docs/memory-model.md @@ -1,8 +1,15 @@ -# Arena 内存模型 +# 内存模型：图锚定区域（Graph-Anchored Regions） ## 概述 -Core 采用基于 Arena 的统一内存管理方案，将堆内存划分为与数据流子图绑定的独立 Arena。每个 Arena 内部使用线性指针碰撞分配（bump allocation），回收直接将整个 Arena 游标重置回起始地址（格式化清空）。所有权系统静态保证区域内无活跃引用逃逸。 +Core 采用**图锚定区域**的统一内存管理方案：区域（Region）锚定在数据流图上——**区域是子图节点的字节域**，不是词法作用域的影子。堆内存划分为与数据流子图绑定的独立区域，每个区域内部使用线性指针碰撞分配（bump allocation），回收直接将整个区域游标重置回起始地址（格式化清空）。 + +本设计是 2026-07-28 多 Arena 模型（`docs/superpowers/specs/2026-07-28-arena-model-design.md`）的**概念升级**：Arena 保留为分配器面实现，语义面升级为图锚定区域。传统区域内存管理（Tofte-Talpin 区域栈、Cyclone、Verona）全部锚定词法作用域（LIFO 嵌套）；Core 的执行模型是数据流图，区域与图同构。 + +**不可放弃的两个核心价值**（放弃它们的代价）： + +1. **无碎片**——静态已知大小的分配路径保持纯 bump，零碎片 +2. **动态模式下工程可控的极低碎片**——动态大小分配路径走分档子区域，浪费上界由 size class 表决定 长期运行服务的内存占用上限由并发区域数量决定，天然无 GC 停顿。 @@ -19,25 +26,34 @@ Core 采用基于 Arena 的统一内存管理方案，将堆内存划分为与 | 跟踪式 GC (Mark-Sweep/Compact) | 停顿不可预测、内存开销不确定、不适合硬实时 | | RAII + 所有权 (Rust) | 静态正确，但复杂数据结构需精细设计借用关系，且 Drop 顺序在运行时产生开销 | -### Arena 方案的优势 +### 区域方案的优势 - **分配 O(1)**：仅指针碰撞，无空闲链表遍历 - **回收 O(1)**：整体重置游标，不逐元素析构 -- **无碎片**：Arena 内线性分配，无释放操作，不会产生内部碎片 -- **可预测**：分配只检查 Arena 剩余容量，无 GC 停顿 -- **Cache 友好**：同一子图的数据集中在同一 Arena，空间局部性好 +- **无碎片**：区域内线性分配，无释放操作，不会产生内部碎片 +- **可预测**：分配只检查区域剩余容量，无 GC 停顿 +- **Cache 友好**：同一子图的数据集中在同一区域，空间局部性好 + +### 论文依据 + +| 论文 | 结论 | 对 Core 的意义 | +|------|------|---------------| +| Tofte & Talpin, *Region-Based Memory Management* (POPL'94 / I&C 1997) | 存储 = 区域的栈；区域分配/回收点由类型-效果分析自动推断；形式化可靠性证明。已知弱点：区域活得太久导致内存泄漏 | 自动推断可行且可证；泄漏弱点 → 需要显式提前释放（见 Cyclone） | +| Gay & Aiken, *Memory Management with Explicit Regions* (PLDI'98)；*Language Support for Regions* (PLDI'01) | 显式区域与 malloc/free 性能相当；区域子类型（outlives）；多级区域层次；**提前释放是工程可用的关键** | "指定回收"作为编译器内部机制（IR 层生成回收点），不暴露语法 | +| *Reference Capabilities for Flexible Memory Management* (OOPSLA'24, Verona 线) | 区域 = dominator scope，内部对象同生共死；内存按区域局部管理；底层 snmalloc = 分档 bump 分配（size class） | size class 是动态碎片控制的工程标准答案 | +| Leroy et al., *The CompCert Memory Model, Version 2* (2012) | 块 + (块 ID, 字节偏移) 指针；**每字节权限**（Freeable > Writable > Readable > Nonempty > Empty）；块按构造分离；Coq 机器验证 | 每字节权限层 = 语义面（验证器）的范式 | --- ## 核心概念 -### Arena +### 区域（Region） -Arena 是一段连续虚拟内存区域，维护一个单调递增的分配游标（bump pointer）： +区域是一段连续虚拟内存区域，维护一个单调递增的分配游标（bump pointer）： ``` ┌─────────────────────────────────────────────┐ -│ Arena │ +│ 区域 │ │ ┌──────┬──────┬──────┬──────┬─────────────┐│ │ │ Alloc │ Alloc │ Alloc │ │ 剩余空间 ││ │ │ #1 │ #2 │ #3 │ │ ││ @@ -60,126 +76,186 @@ fn alloc(size: usize) -> *mut u8 { } ``` -### 子图绑定 +### 图锚定：区域 = 子图节点的字节域 -每个数据流图节点（DFNode）可关联一个 Arena。执行器在激活节点时将其 Arena 设为当前 Arena，节点内所有分配均来自该 Arena。 +每个数据流图节点（DFNode）可关联一个区域。执行器在激活节点时将其区域设为当前区域，节点内所有分配均来自该区域。 ``` -DFGraph Arena Pool +DFGraph Arena Pool（区域的实现） ┌──────────┐ ┌──────────────┐ -│ node A │────────────▶│ Arena A │ +│ node A │────────────▶│ 区域 A │ │ node B │────────┐ │ │ -│ node C │──┐ └───▶│ Arena B │ -│ node D │──│─────────▶│ Arena C │ -└──────────┘ │ │ Arena D │ +│ node C │──┐ └───▶│ 区域 B │ +│ node D │──│─────────▶│ 区域 C │ +└──────────┘ │ │ 区域 D │ │ └──────────────┘ │ ↑ - │ Arena Pool —— 所有 Arena - │ 由运行时统一管理 + │ 区域池 —— 所有区域 + │ 由运行时统一管理 ``` -### 生命周期 +三个推论（与传统词法锚定模型的分野）： + +**推论 A：生命周期 = 图活性，不是 LIFO。** RegionCheck 的 `cur_seq < exit_seq` 判定（见 `docs/pointer-model.md`）就是图版本的生命周期定义。这天然支持 flow/go 的独立区域（区域栈做不到非 LIFO 生命周期），也天然给出跨区域引用的合法性判据（outlives 的图形式）。 + +**推论 B：区域操作沿图边。** 区域不仅嵌套（树），还能沿数据流边操作： + +- **split**：一块字节沿边划给子消费者（= 字节块独立回收；子区域 = 图边的子块，自己的游标 + 自己的重置点） +- **merge**：汇合点两个子区域的数据汇入（拷贝或区域合并） +- **share**：分叉点一个区域被多个消费者只读共享（共享者必须 outlive 引用） -Arena 生命周期绑定到子图执行周期： +**推论 C：每字节归属 = 图的 provenance 边。** 记忆模型是"字节序列 + 宽度 + 边界"——provenance（归属）、offset（字节偏移）、alloc_size（字节大小）全部与类型无关。"控制每一个字节"不是新语法，是图上本来就有的信息。 -| 构造 | 子图开始执行时创建。容量由编译器静态推断或配置指定 | -|------|------------------------------------------------------| -| 分配 | 子图内所有分配均从绑定 Arena 的 bump pointer 分配 | -| 回收 | 子图执行完毕后，Arena 游标重置到起始地址。不调用析构函数 | -| 复用 | Arena 返回 Arena Pool，供后续同类子图重复使用 | +### 与传统区域模型的关系 + +区域树是图区域的特例（无汇合/分叉的图 = 树 = 词法嵌套）；Tofte-Talpin 的区域栈是更窄的特例（树 + LIFO）。本设计是推广，不是发明。 + +> 术语注意：dataflow 模块已有「region」一词指控制流嵌套（SG_IF/LOOP/FOR/FLOW/UNSAFE）。本文的「区域」指**内存字节域**，按上下文区分。 + +### Arena = 区域的实现 + +2026-07-28 的 Arena 设计（arena pool、bump 双路径、链式扩容、子图绑定、大小预计算，见 `docs/superpowers/specs/2026-07-28-arena-model-design.md`）原样继承，作为分配器面实现。概念关系： + +| 语义面（本设计） | 分配器面（07-28 设计） | +|------------------|----------------------| +| 区域（Region） | Arena slot | +| 子区域 split | 子图嵌套 arena / 分档子分配器 | +| 图活性生命周期 | arena_new / arena_reset 插桩 | +| 策略推导 | 大小预计算（IR 层） | --- -## 所有权与逃逸分析 +## 机制总图 + +| # | 需求 | 图上的机制 | 验证/推导者 | +|---|------|-----------|-----------| +| 1 | 字节块独立回收 | 区域 = 子图节点；子区域 = 沿图边 split；显式提前释放（回收点）由 IR 层生成（Cyclone early deallocation 的自动版）；merge/share 处理汇合/分叉 | 图活性（RegionCheck） | +| 2 | 逐字节布局 | **布局元数据进图**：字段字节偏移/packed/对齐，后端与验证器同一来源（语义保鲜）。默认布局全自动（自然对齐），`layout(...)` 仅逃生门 | 编译期计算，图节点存储 | +| 3 | 固定地址放置 | **ALLOC_AT 节点**（地址+大小+对齐）进图，与 ALLOC 同路径获得 provenance | ProvenanceVerify（边界+宽度） | +| 4 | 碎片有界 | **策略推导**：子图全静态大小 → 纯 bump（零碎片）；混动态 → 分档子区域（size class 表由图上分配大小分布推导） | 图分析（大小预计算扩展） | +| 5 | 跨区域 | **outlives 顺序判定**：引用者存活区间 ⊆ 被引用区域存活区间（RegionCheck 现有机制，从"禁止"放宽为"顺序判定"） | RegionCheck | + +不变的三条铁律： + +1. 静态已知大小路径 = 纯 bump，**零碎片** +2. 动态路径 = 分档子区域，**浪费上界由 size class 表决定**（工程可控：档位越细上界越低，如 pow2 档 ≈50%、细分档 ≈12.5%） +3. 区域池 / 嵌套 / 子图绑定 = 原样继承，概念升级为"区域" -Arena 方案的核心前提：**子图内分配的引用不会逃逸到子图之外**。编译器通过静态分析保证： +--- -### 逃逸规则 +## 用户面：零管理负担 -1. **向下逃逸禁止**：Arena A 内分配的对象不能作为参数传递给生命周期比 A 长的子图 -2. **向上逃逸禁止**：Arena A 内分配的对象不能作为返回值给生命周期比 A 长的调用者 -3. **全局逃逸禁止**：Arena A 内分配的对象不能赋值给全局变量 -4. **跨 Arena 引用禁止**：Arena A 内的指针不能指向 Arena B 内的对象 +用户零参与、全部由图推导的事项： -### 例外：跨 Arena 引用 +| 事项 | 谁做 | +|------|------| +| 区域划分/生命周期 | 图活性推导（子图边界即区域） | +| 回收时机（含"指定回收"需求） | 图分析生成回收点——推断在编译器内部完成，用户看不到 | +| 碎片策略 / size class | 图分析推导分配策略 | +| 跨区域合法性 | RegionCheck 自动判定 | +| 所有验证 | 三点 pass 自动 | -跨 Arena 引用（Arena A 的指针指向 Arena B 的数据）需要 `unsafe`，和所有数据流图无法追踪 provenance 的情况一样。详见 `docs/pointer-model.md`。 +用户只表达两件只有用户自己知道的事实： ```core -unsafe { - ref := &arena_b.data; // 跨 Arena 引用，编译器无法自动验证 +// 1. 布局声明（逃生门）——默认布局全自动：编译器按类型推导自然布局 +// （字段顺序 + 自然对齐），用户不写任何东西。 +// layout(...) 仅当默认布局不合用时才需要：packed（FFI）、强制对齐、硬件结构。 +struct PackedHeader layout(packed, align(4)) { + a: u8, // 偏移 0 + b: u32, // 偏移 4 + c: u16, // 偏移 8 } + +// 2. 放置声明——地址是物理事实，只有用户知道。 +// 声明式进图（地址+大小+对齐），之后全图追踪，ProvenanceVerify 照常验证。 +mmio := alloc_at(0x7fff0000, 4096, align(4096)); ``` -`unsafe` 块在此处的作用不是"关掉检查"，而是"我知道这违反规则，但我保证安全"。 +- **不提供**显式区域/回收语法（YAGNI）。「指定回收」是编译器内部机制（IR 层生成回收点）。 +- 与 `docs/pointer-model.md` 2026-08-10 定论的关系：0x 字面量仍是 unsafe 外部入口；`alloc_at` 是**声明式进图**（获得 provenance 的节点），不冲突——声明是唯一信任点，之后全图追踪。 + +--- -### 实现方式 +## 语义面：字节权限层 -逃逸分析在 IR 层面以数据流分析实现： +内存模型 = 图 + 字节权限层（CompCert v2 范式）： -- 每个 IR 变量标注 Arena 来源（`ArenaTag`） -- 赋值/传参时检查 ArenaTag 兼容性 -- 违反规则产生编译错误，除非在 `unsafe` 块中 +- 每字节内容 = 字节序列（已有，见 `docs/pointer-model.md`） +- 每字节权限：**Freeable > Writable > Readable > Nonempty > Empty**（新加） + - Freeable：可比较、可读、可写、可释放 + - Writable：可比较、可读、可写、不可释放 + - Readable：可比较、可读、不可写 + - Nonempty：仅可比较（指针有效性） + - Empty：无任何权限（未分配/已释放） +- 区域树 = 图的子图结构；布局元数据、ALLOC_AT 边界、outlives 结论全部从图导出——**验证器消费图即消费全部内存语义** -``` -// 伪代码：ArenaTag 传播 -let a = Arena::new(); // a.tag = ArenaA -let x = alloc_in(a, 32); // x.tag = ArenaA -let y = x; // y.tag = ArenaA (传播) -let z = some_func(x); // z.tag = ArenaA (返回tag传播) -store_global(g, x); // 错误：ArenaA → Global 逃逸 -unsafe { store_global(g, x) } // 允许：unsafe 豁免 -``` +--- + +## 所有权与逃逸 + +区域方案的核心前提：**子图内分配的引用不会逃逸到子图之外**。编译器通过静态分析保证。逃逸分析在 IR 层面以数据流分析实现：每个 IR 变量标注区域来源（`ArenaTag`），赋值/传参时检查兼容性，违反规则产生编译错误。 + +### 逃逸规则（2026-08-13 修订） + +1. **向下逃逸禁止**：区域 A 内分配的对象不能作为参数传递给生命周期比 A 长的子图 +2. **向上逃逸禁止**：区域 A 内分配的对象不能作为返回值给生命周期比 A 长的调用者 +3. **全局逃逸禁止**：区域 A 内分配的对象不能赋值给全局变量 +4. **跨区域引用：outlives 顺序判定**（修订）——区域 A 的指针可以指向区域 B 的对象，**当且仅当** B 的存活区间 ⊇ 引用的使用区间（RegionCheck 的 `cur_seq < exit_seq` 判定）。不再一刀切禁止。 + +### 例外：图边界 + +编译器无法追踪 provenance 的入口点（外部地址、FFI 返回值、inline asm）仍需要 `unsafe`，和所有数据流图无法追踪 provenance 的情况一样。详见 `docs/pointer-model.md`。`unsafe` 块在此处的作用不是"关掉检查"，而是"标注图边界入口"。 --- ## 与数据流图的集成 -### 子图类型与 Arena 策略 +### 子图类型与区域策略 -| 子图类型 | Arena 策略 | 说明 | +| 子图类型 | 区域策略 | 说明 | |----------|-----------|------| -| DAG (函数/分支/for) | 栈式 Arena | 函数入口创建，出口回收。与调用栈深度同步 | -| 静态循环 (loop) | 固定 Arena | 循环开始前分配，结束后回收。容量根据循环不变量预计算 | -| Flow | 独立 Arena | 每次 flow 激活创建独立 Arena。并发 flow 各自独立 | -| Go | 独立 Arena | 每个 goroutine 拥有独立 Arena。退出时整体回收 | -| Yield/Recv | 消息 Arena | 跨 flow 传递的数据在接收端 Arena 中重新分配 | +| DAG (函数/分支/for) | 栈式区域 | 函数入口创建，出口回收。与调用栈深度同步 | +| 静态循环 (loop) | 固定区域 | 循环开始前分配，结束后回收。容量根据循环不变量预计算 | +| Flow | 独立区域 | 每次 flow 激活创建独立区域。并发 flow 各自独立 | +| Go | 独立区域 | 每个 goroutine 拥有独立区域。退出时整体回收 | +| Yield/Recv | 消息区域 | 跨 flow 传递的数据在接收端区域中重新分配 | -### Arena 嵌套 +### 区域嵌套 -Arena 可嵌套：子图在父图的 Arena 内创建子 Arena。子 Arena 回收后，父 Arena 不受影响。 +区域可嵌套：子图在父图的区域内创建子区域。子区域回收后，父区域不受影响。 ``` -Arena A (函数 main) -├── Arena B (loop 主体) -├── Arena C (flow 1) -└── Arena D (flow 2) - └── Arena E (flow 2 内的子 loop) +区域 A (函数 main) +├── 区域 B (loop 主体) +├── 区域 C (flow 1) +└── 区域 D (flow 2) + └── 区域 E (flow 2 内的子 loop) ``` --- ## 运行时布局 -### Arena 内存池 +### 区域内存池 -运行时维护一个 Arena Pool，包含固定数量的预分配 Arena： +运行时维护一个区域池（Arena Pool），包含固定数量的预分配区域： ``` -Arena Pool +区域池 ┌────┬────┬────┬────┬────┬────┬────┬────┐ │ P0 │ P1 │ P2 │ P3 │ P4 │ P5 │ P6 │ P7 │ └────┴────┴────┴────┴────┴────┴────┴────┘ │ ↑ - │ 分配中的 Arena + │ 分配中的区域 │ - └─── 空闲 Arena + └─── 空闲区域 ``` -- 活跃 Arena 数量 = 当前并发子图数量 -- 任一时刻，最多 `MAX_CONCURRENCY` 个 Arena 同时活跃 -- 未使用的 Arena 留在池中，不需归还操作系统 -- 必要时可向操作系统扩展 Arena 容量 +- 活跃区域数量 = 当前并发子图数量 +- 任一时刻，最多 `MAX_CONCURRENCY` 个区域同时活跃 +- 未使用的区域留在池中，不需归还操作系统 +- 必要时可向操作系统扩展区域容量 ### 大小预计算 @@ -190,74 +266,81 @@ Arena Pool 3. 对动态分配（如运行时决定的缓冲区大小）标注最大容量上限 4. 若无法推断上限，使用部署配置中的默认容量 +**策略推导**（2026-08-13 扩展）：预计算结果同时决定子图的分配策略——全静态已知 → 纯 bump（零碎片）；混有动态大小 → 分档子区域（size class 表由图上分配大小分布推导）。 + --- ## 与并发模型的协作 ### 无锁分配 -每个 Arena 只被一个执行线程访问。Arena 内 bump pointer 可以是线程局部变量，无需原子操作。 +每个区域只被一个执行线程访问。区域内 bump pointer 可以是线程局部变量，无需原子操作。 ``` -// 线程安全：每线程 Arena +// 线程安全：每线程区域 thread_local! { - static CURRENT_ARENA: RefCell; + static CURRENT_REGION: RefCell; } ``` -### Go/Flow 的 Arena 隔离 +### Go/Flow 的区域隔离 ``` -go f() → 新 Arena G → 函数 f 内所有分配在 G +go f() → 新区域 G → 函数 f 内所有分配在 G ↓ - f 结束 → Arena G 整体回收 + f 结束 → 区域 G 整体回收 ↓ - go 表达式的结果 → 拷贝到父 Arena + go 表达式的结果 → 拷贝到父区域 ``` -- `go f()` 创建独立 Arena，f 的返回值在 f 结束后拷贝到父 Arena -- `flow` 的每个分支拥有独立 Arena，分支退出时回收 -- `yield` 的数据通过消息 Arena 传递，接收方在自己的 Arena 中重新分配 +- `go f()` 创建独立区域，f 的返回值在 f 结束后拷贝到父区域 +- `flow` 的每个分支拥有独立区域，分支退出时回收 +- `yield` 的数据通过消息区域传递，接收方在自己的区域中重新分配 ### 停止机制 -长期运行的服务，内存占用上限为 `MAX_CONCURRENCY × MAX_ARENA_SIZE`。当 Arena Pool 耗尽空闲 Arena 时，新的 go/flow 被阻塞直到有 Arena 可用。不需要 GC。 +长期运行的服务，内存占用上限为 `MAX_CONCURRENCY × MAX_REGION_SIZE`。当区域池耗尽空闲区域时，新的 go/flow 被阻塞直到有区域可用。不需要 GC。 --- ## Rust 风格的对比 -| | Rust (RAII + 所有权) | Core (Arena) | +| | Rust (RAII + 所有权) | Core (图锚定区域) | |--|---------------------|--------------| | 分配开销 | 栈分配 O(1)，堆分配需寻找空闲块 | Bump O(1) | | 释放开销 | Drop 链递归 O(深度) | 游标重置 O(1) | -| 借用检查 | 生命周期标注复杂，NLL 推断有局限 | ArenaTag 传播，按子图边界检查 | -| 并发 | Arc/RwLock 运行时开销 | Arena 隔离，无共享 | -| 循环引用 | 需 Weak 打破 | 同 Arena 内允许循环（回收时整体释放） | -| GC | 无 GC | 无 GC（Arena 回收等价于批量释放） | +| 借用检查 | 生命周期标注复杂，NLL 推断有局限 | 区域标签传播 + 图活性，按子图边界检查 | +| 并发 | Arc/RwLock 运行时开销 | 区域隔离，无共享 | +| 循环引用 | 需 Weak 打破 | 同区域内允许循环（回收时整体释放） | +| GC | 无 GC | 无 GC（区域回收等价于批量释放） | | 适用场景 | 通用系统编程 | 数据流驱动、并发密集、实时系统 | --- -## 当前实现状态 +## 设计状态 -**更新（2026-07-28）**：Arena 内存模型已完整实现（`src/stdlib/arena.cr`）——完整生命周期 +**2026-07-28**：多 Arena 模型已完整实现（`src/stdlib/arena.cr`）——完整生命周期 （init/new/reset）、动态元数据、free list、嵌套；IR 子图绑定（函数/loop/for/unsafe 自动 arena lifecycle + 大小预计算）；ELF 后端双路径 alloc（arena 感知 + 全局 bump 回退）； -mmap 堆扩展（BSS 打满自动 mmap 1GB）；emit_alloc_body 零初始化 + 链式扩容。 +mmap 堆扩展（BSS 打满自动 mmap 1GB）；emit_alloc_body 零初始化 + 链式扩容。实现细节见 +`docs/superpowers/specs/2026-07-28-arena-model-design.md`。 + +**2026-08-09**：发现 arena bump 分配运行时死循环（`arena_init` + `arena_new` 后调用 `alloc` 运行时挂起、无输出、CPU 占用）。ELF 后端 arena 相关编码已全部 objdump 验证正确（`mov [r8],r10d` 的 44 89 00 错误已修复回 45 89 10），定位方向为 `emit_alloc_body` 生成的运行时逻辑（g_current_arena 检查 / bump 推进 / .Lretry 循环 / OOM 链式扩展）。详见 TODO.md 预存 bug 5。 -**更新（2026-08-09）**：发现 arena bump 分配运行时死循环（`arena_init` + `arena_new` 后调用 `alloc` 运行时挂起、无输出、CPU 占用）。ELF 后端 arena 相关编码已全部 objdump 验证正确（`mov [r8],r10d` 的 44 89 00 错误已修复回 45 89 10），定位方向为 `emit_alloc_body` 生成的运行时逻辑（g_current_arena 检查 / bump 推进 / .Lretry 循环 / OOM 链式扩展）。详见 TODO.md 预存 bug 5。 -以下"待解决问题"为后续改进方向。 +**2026-08-13**：设计升级为图锚定区域（本文档）。本阶段**只改文档，不实现**；实现按 +M1（生命周期+碎片）→ M2（布局+放置）→ M3（跨区域）推进，见 +`docs/superpowers/specs/2026-08-13-graph-anchored-regions-design.md`。 ## 待解决问题 -### Arena 碎片化 +### 区域级空间浪费 -虽然 Arena 内无碎片，但 Arena 整体大小预分配可能导致： -- 小分配占用大 Arena → 空间浪费 -- 动态 Arena 大小调整策略待设计 +虽然区域内无碎片，但区域整体大小预分配可能导致： +- 小分配占用大区域 → 空间浪费 +- 动态区域大小调整策略 -候选方案：分档 Arena（size class）、链式 Arena（用满后追加新块） +**设计已定（2026-08-13）**：动态路径走分档子区域（size class 表由图分析推导）， +静态路径保持纯 bump。实现待 M1。 ### 逃逸分析精度 @@ -266,9 +349,9 @@ mmap 堆扩展（BSS 打满自动 mmap 1GB）；emit_alloc_body 零初始化 + - 条件性逃逸（某些分支逃逸某些分支不逃逸） - RawRef 与 unsafe 的交互边界 -### Arena 复用策略 +### 区域复用策略 -Arena 返回 Pool 后，重置游标但不清除内存。敏感场景可能需要清零： +区域返回池后，重置游标但不清除内存。敏感场景可能需要清零： - 跨安全边界的进程隔离 -- 包含密钥或隐私数据的 Arena +- 包含密钥或隐私数据的区域 - 由部署配置控制，非默认行为 diff --git a/docs/pointer-model.md b/docs/pointer-model.md index e15818a..33dc3e0 100644 --- a/docs/pointer-model.md +++ b/docs/pointer-model.md @@ -97,6 +97,8 @@ O(N × P)，其中 N 为指针变量数，P 为 points-to 集平均大小。Core 跨子图引用：子图 A 分配的内存被子图 B 引用。当子图 A 退出后，B 中的指针变成悬垂指针。 +**2026-08-13 修订**：跨区域引用不再一刀切禁止——安全当且仅当**被引用区域的存活区间 ⊇ 引用的使用区间**（outlives 顺序判定，Cyclone 区域子类型的图形式）。RegionCheck 的 `cur_seq < exit_seq` 判定就是这个顺序判定。见 `docs/memory-model.md` 机制 #5。 + ### 算法 RegionCheck 为每个子图分配递增的序号（由控制流决定，不是运行时值）。每个 ALLOC 节点标记它所属的子图 ID。每个 DEREF 节点检查目标子图是否存活。 @@ -176,13 +178,26 @@ fail → panic 后端将其编译为 `cmp` + `jae` + `ud2` 序列，约 10 字节，无其他运行时开销。 +### ALLOC_AT：声明式放置（2026-08-13） + +`alloc_at(addr, size, align)` 是**声明式进图节点**：固定地址区域以（地址+大小+对齐）声明，与 ALLOC 同路径获得 provenance。声明之后全图追踪，ProvenanceVerify 照常验证边界+宽度： + +```core +mmio := alloc_at(0x7fff0000, 4096, align(4096)); // MMIO 页，声明式进图 +*mmio = 42; // 安全代码即可，边界内照常验证 +p := mmio + 4096; // 越界 → 编译错误或运行时 check +``` + +- **声明是唯一信任点**（等价于一次受控的图边界入口），之后编译器重新获得追踪权——与 `unsafe` 的"标注图边界入口"语义一致，但进图后是普通 ALLOC 的验证路径 +- 与 2026-08-10 定论（不扩展 0x 字面量直接指内部对象）**不冲突**：0x 字面量仍是 unsafe 外部入口；`alloc_at` 是声明式进图，用户必须给出地址+大小+对齐三个事实 + ## unsafe 边界 `unsafe` 是编译器无法追踪 provenance 时的唯一退路。发生在图边界： | 场景 | 原因 | |------|------| -| 外部硬件地址 | `0x7fff0000 as *int` 没有 ALLOC 节点 | +| 外部硬件地址 | 裸 `0x7fff0000 as *int` 没有 ALLOC 节点；声明式放置用 `alloc_at`（见上节，进图后不需要 unsafe） | | FFI 返回值 | 外部函数返回的指针没有 Core 的 provenance | | inline assembly | 汇编的输出指针没有来源 | @@ -198,6 +213,19 @@ DEREF 处的"视图"。cast 在图里无节点（ir_gen 透传），provenance - 编译器内部 `asp`（外部地址空间）标志在 checker 写入 TYP_PTR 但全仓库无消费点—— `0x... as *int` 在 safe 代码同样放行，归属待定，见 TODO 预存 bug 7 +### 字节权限层（2026-08-13） + +记忆模型在"字节序列 + 宽度 + 边界"之上补充**每字节权限**（CompCert v2 范式）： + +``` +Freeable > Writable > Readable > Nonempty > Empty +``` + +- Freeable：可比较、可读、可写、可释放；Writable：可比较、可读、可写、不可释放； + Readable：可比较、可读、不可写；Nonempty：仅可比较（指针有效性）；Empty：无权限 +- 分配后默认 Freeable；`drop_perm` 可收窄（如 const 数据降为 Readable） +- 权限与 provenance/offset/size 一样是**图数据**——验证器消费图即获得每字节控制 + `unsafe` 块内部的指针操作仍然被三点 pass 追踪。`unsafe` 不是"关掉验证"——是"标注图边界入口"。一旦进入 safe 代码，编译器重新获得追踪权。 ```core @@ -235,6 +263,14 @@ Core 编译器已有数据流图（`src/compiler/dataflow.cr`）和线性扫描 更优（无漂移、类型全、验证无条件）；外部契约地址 unsafe 已够用。0x 字面量仅保留 unsafe 外部入口角色（上表前三行），详见 TODO 预存 bug 7 +**更新（2026-08-13）**：设计修订（图锚定区域内存模型，只改文档不实现）—— +1. **ALLOC_AT 声明式放置节点**进图（见上节）：固定地址区域声明式获得 provenance， + 与 2026-08-10 定论不冲突（0x 字面量仍是 unsafe 入口） +2. **跨区域引用放宽**：从"禁止"改为 outlives 顺序判定（RegionCheck 图活性判定即该检查） +3. **字节权限层**：每字节 Freeable/Writable/Readable/Nonempty/Empty（见上节） + +设计依据：`docs/superpowers/specs/2026-08-13-graph-anchored-regions-design.md` + `docs/memory-model.md`。 + ## 参考 - **SVF** (SVF-tools): LLVM 上的值流图框架，自动检测 use-after-free、double-free、buffer overflow。Core 的数据流图是更统一的形式——同一张图同时做 regalloc、调度、验证。 diff --git a/docs/spec-design.md b/docs/spec-design.md index ef5ae2f..df5c654 100644 --- a/docs/spec-design.md +++ b/docs/spec-design.md @@ -143,7 +143,7 @@ spec fn vec_invariant[T](v: Vec[T]) -> bool { | `#pure` | 无 STORE 到外部变量、无 CALL 到非纯函数 | | | `#deterministic` | 纯 + 无随机/外部依赖 | | | `#terminating` | 所有循环有可识别变体 | | -| `#no_alloc` | 无 ALLOC/ALLOC_ARRAY 节点 | | +| `#no_alloc` | 无 ALLOC/ALLOC_ARRAY/ALLOC_STRUCT/ALLOC_AT 节点 | | | `#no_throw` | 无异常路径 | | | `#safe_index` | 所有索引访问在边界内 | | | `#len_preserved` | 集合长度不变（无插入/删除） | `sort` | @@ -422,7 +422,7 @@ SMT 解不出时返回**反例模型**（哪个输入违反性质）——开发 | `#check(b != 0)` 已证 | 除法免零检查 | | `#safe_index` 已证 | DEREF 运行时边界检查（cmp+jae+ud2）直接消除——编译期证明免检的规约版，覆盖运行时数组 | | `#pure` 已证 | CSE / 死代码删除 / 重排（纯调用可删可移） | -| `#no_alloc` 已证 | 栈分配替代堆分配 | +| `#no_alloc` 已证 | 栈分配替代堆分配（区域路径：静态大小预计算 → 纯 bump 零碎片） | | `loop invariant` + `#terminating` 已证 | 循环变换（向量化/强度削减/展开）前提满足 | | 指针分离/别名规约已证 | 内存访问重排（否则保守不重排） | | `#deterministic` 已证 | 更激进的缓存/重算策略 |