🥮 mooncakes.io

    moon-arena-plan

    Static multi-bank buffer planning and independent layout verification

    memory-planning
    tensor
    arena
    embedded
    Download zip
    Author
    Version
    0.2.0
    License
    MIT
    Repository
    Last updated
    yesterday
    Downloads
    13

    #MoonArenaPlan

    静态多内存区缓冲区规划库与 CLI。给定缓冲区的大小、存活区间、允许内存区和固定位置，生成可复用的偏移布局，并用独立检查器核验结果。核心实现为 MoonBit，MIT 许可证。

    适用于已知串行执行顺序的张量流水线、采集与处理缓冲区，以及内存预算的 CI 回归检查。使用者需提供准确的字节数、scratch、持久状态、保留输出和设备访问限制。

    #安装与构建

    使用 moonc 0.10.16 或更高；当前验证和 CI 固定 0.10.16+b1a0e846e 及匹配 core。Windows 已有 SDK 可在当前终端执行：

    . ./scripts/use-sdk.ps1 -SdkHome '你的 MoonBit SDK 绝对路径'
moon update
moon check --deny-warn
moon build --release --deny-warn
moon test --deny-warn

    库安装：moon add SongYZZZ/moon-arena-plan。在 moon.pkg 导入 "SongYZZZ/moon-arena-plan" @arena，调用 plan、verify、summarize、lifetimes、trace_lifetimes、solve_exact、explain、compare_layouts、c_header。API 见 pkg.generated.mbti，输入契约见 SPEC.md。

    #可复现案例

    moon run cmd/arenaplan -- plan examples/reuse.json
moon run cmd/arenaplan -- plan examples/dma_banks.json
moon run cmd/arenaplan -- plan examples/budget_failure.json

    第三条预期退出 1，报告超预算；不是构建失败。三个 64 字节、生命周期不重叠的缓冲区在第一个例子复用到 64 字节，而逐个独立预留需要 192 字节。第二例把固定采集缓冲区保留在 dma 内存区，把同一时刻存活的特征区放入 fast。第三例在交接步同时保留输入和输出，128 字节需求超出 96 字节预算。

    这些是可执行的工程场景样本，尚无真实设备部署或用户采用记录。项目目标及成熟工具关系见 docs/NECESSITY.md。

    # layout 命令只输出布局，可把 stdout 保存为 layout.json
moon run cmd/arenaplan -- layout examples/reuse.json
moon run cmd/arenaplan -- verify examples/reuse.json layout.json
moon run cmd/arenaplan -- header examples/reuse.json layout.json
moon run cmd/arenaplan -- lifetimes examples/graph.json

    文件读取仅接受最多 4 MiB 的 UTF-8 常规文件；CLI 只写 stdout/stderr，不覆盖输入。退出码 0 表示输入约束满足，1 表示布局/预算问题，2 表示输入、用法或导出失败。

    #验证

    python scripts/verify.py --exe _build/native/release/build/cmd/arenaplan/arenaplan.exe
moon run examples/c_replay
moon test --target js -p SongYZZZ/moon-arena-plan --deny-warn
moon test --target wasm-gc -p SongYZZZ/moon-arena-plan --deny-warn

    Python 黑盒检查器用另一种实现核对随机问题、峰值和输入重排；C 示例使用 CLI 实际生成的头文件读写数组，检查交接步的数据保持。它们验证静态布局合同，不构成神经网络推理或硬件验证。

    #边界

    schema 1 的完整字段及拒绝行为是本版本兼容终点。字节数、容量、对齐和偏移使用十进制字符串，时间步和 schema 使用 JSON 整数；禁止未知字段、重复 JSON 键和小数/指数形式的数值。空固定字段可省略或使用 null。

    规划采用固定位置优先、可选 bank 数量较少的缓冲区优先、大小降序的贪心规则；ID 按 ASCII 排序，bank 列表顺序用于平局选择。结果不保证全局最优；超预算不证明其他布局都不可行。允许 bank 集合来自调用者，不从芯片型号自动推导。硬件地址、缓存一致性、异步 DMA 实际完成时间、栈和运行时开销需另行验证。

    当前不读取 ONNX/TFLite 文件，不执行张量算子，不把外部框架的分配器作为产品实现。标准内存规划技术的公开参考与许可证见 docs/REFERENCES.md。

    终审自查与修复记录包含实际结果和保留风险。

    #0.2.0 新增的完整工作流

    # 区分贪心失败、有界穷举无解和搜索预算耗尽
moon run cmd/arenaplan -- exact examples/exact_alignment_kib.json
moon run cmd/arenaplan -- explain examples/exact_alignment_kib.json
# explain 在上述贪心布局下预期退出 1；exact 找到 9 KiB 的可行见证

# CI 回归：16 KiB 升级为 32 KiB，显式允许每 bank 增长 16 KiB
moon run cmd/arenaplan -- compare examples/regression_before.json examples/regression_after.json 16384

# C 例程输出调用点轨迹，保存其 stdout 后导入
moon run examples/trace_capture
moon run cmd/arenaplan -- trace trace.json

    精确求解限 12 个缓冲区、4 个 bank，默认 100000 次候选检查，上限 1000000。只有完整枚举结束才返回 infeasible；预算耗尽返回 limit，退出 3。它判断可行性，不保证最小占用。

    峰值解释列出峰值时存活的缓冲区，区分布局超预算与当前 bank 分配下的活跃需求。版本比较按 bank 检查高水位与活跃峰值增长、容量缩减和 bank 增删。声明的增长阈值不会豁免容量违规。

    轨迹导入从完整、非递减的 begin/read/write/end 事件推导闭合生命周期，检查已记录路径中的越界使用；它依赖调用点准确记录，不拦截任意指针访问。CI 运行 C 生产者、导入轨迹、生成布局与头文件，再用 C replay 检查数据保持。

    python scripts/verify_extensions.py --exe _build/native/release/build/cmd/arenaplan/arenaplan.exe --trace-exe _build/native/release/build/examples/trace_capture/trace_capture.exe

    该检查用独立笛卡尔积枚举器核对小问题的可行／不可行结果，并核对搜索限额、版本门禁和实际 C 轨迹流程。

    PlanError

    source
    pub suberror PlanError {
      PlanError(String, String)
    } derive(
    Debug    )

    Bank

    source
    pub(all) struct Bank {
      id : String
      capacity : Int64
    } derive(Eq, ToJson, 
    Debug    , 
    FromJson    )

    Bank::equal

    source
    fn Bank::equal(Bank, Bank) -> Bool

    Bank::from_json

    source

    Bank::not_equal

    source
    fn Bank::not_equal(x : Bank, y : Bank) -> Bool

    Bank::to_json

    source
    fn Bank::to_json(Bank) -> Json

    Bank::to_repr

    source

    BankDelta

    source
    pub(all) struct BankDelta {
      bank : String
      change : String
      before_capacity : Int64?
      after_capacity : Int64?
      before_highwater : Int64
      after_highwater : Int64
      highwater_delta : Int64
      before_peak_live_bytes : Int64
      after_peak_live_bytes : Int64
      peak_live_delta : Int64
      growth_exceeded : Bool
      candidate_over_budget : Bool
    } derive(Eq, ToJson, 
    Debug    )

    BankDelta::equal

    source
    fn BankDelta::equal(BankDelta, BankDelta) -> Bool

    BankDelta::not_equal

    source
    fn BankDelta::not_equal(x : BankDelta, y : BankDelta) -> Bool

    BankDelta::to_json

    source
    fn BankDelta::to_json(BankDelta) -> Json

    BankDelta::to_repr

    source

    BankUsage

    source
    pub(all) struct BankUsage {
      bank : String
      capacity : Int64
      highwater : Int64
      peak_live_bytes : Int64
      peak_step : Int
      fits : Bool
    } derive(Eq, ToJson, 
    Debug    )

    BankUsage::equal

    source
    fn BankUsage::equal(BankUsage, BankUsage) -> Bool

    BankUsage::not_equal

    source
    fn BankUsage::not_equal(x : BankUsage, y : BankUsage) -> Bool

    BankUsage::to_json

    source
    fn BankUsage::to_json(BankUsage) -> Json

    BankUsage::to_repr

    source

    Buffer

    source
    pub(all) struct Buffer {
      id : String
      bytes : Int64
      first : Int
      last : Int
      alignment : Int64
      banks : Array[String]
      fixed_bank : String?
      fixed_offset : Int64?
    } derive(Eq, ToJson, 
    Debug    , 
    FromJson    )

    Inclusive lifetimes. Access restrictions and byte sizes must be supplied.

    Buffer::equal

    source
    fn Buffer::equal(Buffer, Buffer) -> Bool

    Buffer::from_json

    source

    Buffer::not_equal

    source
    fn Buffer::not_equal(x : Buffer, y : Buffer) -> Bool

    Buffer::to_json

    source
    fn Buffer::to_json(Buffer) -> Json

    Buffer::to_repr

    source

    Comparison

    source
    pub(all) struct Comparison {
      allowed_growth_bytes : Int64
      baseline_valid : Bool
      candidate_valid : Bool
      gate_passed : Bool
      banks : Array[BankDelta]
    } derive(Eq, ToJson, 
    Debug    )

    Comparison::equal

    source
    fn Comparison::equal(Comparison, Comparison) -> Bool

    Comparison::not_equal

    source
    fn Comparison::not_equal(x : Comparison, y : Comparison) -> Bool

    Comparison::to_json

    source
    fn Comparison::to_json(Comparison) -> Json

    Comparison::to_repr

    source

    ExactResult

    source
    pub(all) struct ExactResult {
      status : String
      layout : Layout?
      nodes : Int
      budget : Int
    } derive(Eq, ToJson, 
    Debug    )

    A bounded feasibility search, not a minimum-footprint optimizer.

    ExactResult::equal

    source
    fn ExactResult::equal(ExactResult, ExactResult) -> Bool

    ExactResult::not_equal

    source
    fn ExactResult::not_equal(x : ExactResult, y : ExactResult) -> Bool

    ExactResult::to_json

    source
    fn ExactResult::to_json(ExactResult) -> Json

    ExactResult::to_repr

    source

    ExecutionTrace

    source
    pub(all) struct ExecutionTrace {
      schema : Int
      banks : Array[Bank]
      buffers : Array[TrackedBuffer]
      events : Array[TraceEvent]
    } derive(Eq, ToJson, 
    Debug    , 
    FromJson    )

    ExecutionTrace::equal

    source

    ExecutionTrace::from_json

    source

    ExecutionTrace::not_equal

    source
    fn ExecutionTrace::not_equal(x : ExecutionTrace, y : ExecutionTrace) -> Bool

    ExecutionTrace::to_json

    source

    ExecutionTrace::to_repr

    source

    Finding

    source
    pub(all) struct Finding {
      code : String
      buffer : String
      other : String
      message : String
    } derive(Eq, ToJson, 
    Debug    )

    Finding::equal

    source
    fn Finding::equal(Finding, Finding) -> Bool

    Finding::not_equal

    source
    fn Finding::not_equal(x : Finding, y : Finding) -> Bool

    Finding::to_json

    source
    fn Finding::to_json(Finding) -> Json

    Finding::to_repr

    source

    Graph

    source
    pub(all) struct Graph {
      schema : Int
      banks : Array[Bank]
      tensors : Array[Tensor]
      steps : Array[Step]
    } derive(Eq, ToJson, 
    Debug    , 
    FromJson    )

    Graph::equal

    source
    fn Graph::equal(Graph, Graph) -> Bool

    Graph::from_json

    source

    Graph::not_equal

    source
    fn Graph::not_equal(x : Graph, y : Graph) -> Bool

    Graph::to_json

    source
    fn Graph::to_json(Graph) -> Json

    Graph::to_repr

    source

    Layout

    source
    pub(all) struct Layout {
      schema : Int
      placements : Array[Placement]
    } derive(Eq, ToJson, 
    Debug    , 
    FromJson    )

    Layout::equal

    source
    fn Layout::equal(Layout, Layout) -> Bool

    Layout::from_json

    source

    Layout::not_equal

    source
    fn Layout::not_equal(x : Layout, y : Layout) -> Bool

    Layout::to_json

    source
    fn Layout::to_json(Layout) -> Json

    Layout::to_repr

    source

    PeakBuffer

    source
    pub(all) struct PeakBuffer {
      id : String
      bytes : Int64
      offset : Int64
    } derive(Eq, ToJson, 
    Debug    )

    PeakBuffer::equal

    source
    fn PeakBuffer::equal(PeakBuffer, PeakBuffer) -> Bool

    PeakBuffer::not_equal

    source
    fn PeakBuffer::not_equal(x : PeakBuffer, y : PeakBuffer) -> Bool

    PeakBuffer::to_json

    source
    fn PeakBuffer::to_json(PeakBuffer) -> Json

    PeakBuffer::to_repr

    source

    PeakExplanation

    source
    pub(all) struct PeakExplanation {
      bank : String
      capacity : Int64
      highwater : Int64
      peak_live_bytes : Int64
      peak_step : Int
      layout_over_budget_by : Int64
      live_over_budget_by : Int64
      highwater_minus_peak : Int64
      live_buffers : Array[PeakBuffer]
    } derive(Eq, ToJson, 
    Debug    )

    PeakExplanation::equal

    source

    PeakExplanation::not_equal

    source
    fn PeakExplanation::not_equal(x : PeakExplanation, y : PeakExplanation) -> Bool

    PeakExplanation::to_json

    source

    PeakExplanation::to_repr

    source

    Placement

    source
    pub(all) struct Placement {
      id : String
      bank : String
      offset : Int64
    } derive(Eq, ToJson, 
    Debug    , 
    FromJson    )

    Placement::equal

    source
    fn Placement::equal(Placement, Placement) -> Bool

    Placement::from_json

    source

    Placement::not_equal

    source
    fn Placement::not_equal(x : Placement, y : Placement) -> Bool

    Placement::to_json

    source
    fn Placement::to_json(Placement) -> Json

    Placement::to_repr

    source

    Problem

    source
    pub(all) struct Problem {
      schema : Int
      banks : Array[Bank]
      buffers : Array[Buffer]
    } derive(Eq, ToJson, 
    Debug    , 
    FromJson    )

    Problem::equal

    source
    fn Problem::equal(Problem, Problem) -> Bool

    Problem::from_json

    source

    Problem::not_equal

    source
    fn Problem::not_equal(x : Problem, y : Problem) -> Bool

    Problem::to_json

    source
    fn Problem::to_json(Problem) -> Json

    Problem::to_repr

    source

    Step

    source
    pub(all) struct Step {
      id : String
      inputs : Array[String]
      outputs : Array[String]
      scratch : Array[String]
    } derive(Eq, ToJson, 
    Debug    , 
    FromJson    )

    Step::equal

    source
    fn Step::equal(Step, Step) -> Bool

    Step::from_json

    source

    Step::not_equal

    source
    fn Step::not_equal(x : Step, y : Step) -> Bool

    Step::to_json

    source
    fn Step::to_json(Step) -> Json

    Step::to_repr

    source

    Tensor

    source
    pub(all) struct Tensor {
      id : String
      bytes : Int64
      alignment : Int64
      banks : Array[String]
      fixed_bank : String?
      fixed_offset : Int64?
      source : Bool
      retain : Bool
    } derive(Eq, ToJson, 
    Debug    , 
    FromJson    )

    Tensor::equal

    source
    fn Tensor::equal(Tensor, Tensor) -> Bool

    Tensor::from_json

    source

    Tensor::not_equal

    source
    fn Tensor::not_equal(x : Tensor, y : Tensor) -> Bool

    Tensor::to_json

    source
    fn Tensor::to_json(Tensor) -> Json

    Tensor::to_repr

    source

    TraceEvent

    source
    pub(all) struct TraceEvent {
      step : Int
      op : String
      buffer : String
    } derive(Eq, ToJson, 
    Debug    , 
    FromJson    )

    TraceEvent::equal

    source
    fn TraceEvent::equal(TraceEvent, TraceEvent) -> Bool

    TraceEvent::from_json

    source

    TraceEvent::not_equal

    source
    fn TraceEvent::not_equal(x : TraceEvent, y : TraceEvent) -> Bool

    TraceEvent::to_json

    source
    fn TraceEvent::to_json(TraceEvent) -> Json

    TraceEvent::to_repr

    source

    TrackedBuffer

    source
    pub(all) struct TrackedBuffer {
      id : String
      bytes : Int64
      alignment : Int64
      banks : Array[String]
      fixed_bank : String?
      fixed_offset : Int64?
    } derive(Eq, ToJson, 
    Debug    , 
    FromJson    )

    TrackedBuffer::equal

    source

    TrackedBuffer::from_json

    source

    TrackedBuffer::not_equal

    source
    fn TrackedBuffer::not_equal(x : TrackedBuffer, y : TrackedBuffer) -> Bool

    TrackedBuffer::to_json

    source

    TrackedBuffer::to_repr

    source

    c_header

    source
    fn c_header(problem : Problem, layout : Layout) -> String raise PlanError

    C11 offset macros only. The caller owns correctly aligned bank storage.

    compare_layouts

    source
    fn compare_layouts(before : Problem, before_layout : Layout, after : Problem, after_layout : Layout, max_growth_bytes? : Int64) -> Comparison raise PlanError

    Compare verified source/layout pairs. Growth is evaluated per bank for both highwater and live-byte peak; a candidate capacity violation always fails.

    decode_graph

    source
    fn decode_graph(text : String) -> Graph raise PlanError

    decode_layout

    source
    fn decode_layout(text : String) -> Layout raise PlanError

    decode_problem

    source
    fn decode_problem(text : String) -> Problem raise PlanError

    decode_trace

    source
    fn decode_trace(text : String) -> ExecutionTrace raise PlanError

    explain

    source
    fn explain(problem : Problem, layout : Layout) -> Array[PeakExplanation] raise PlanError

    Explain the earliest live-byte peak for each assigned bank. Excess live bytes apply to this bank assignment, not every possible assignment.

    lifetimes

    source
    fn lifetimes(graph : Graph) -> Problem raise PlanError

    Translate an explicit serial schedule; no shape or operator semantics inferred.

    plan

    source
    fn plan(problem : Problem) -> Layout raise PlanError

    Deterministic greedy planning. An over-budget result is not an infeasibility proof.

    solve_exact

    source
    fn solve_exact(problem : Problem, max_nodes? : Int) -> ExactResult raise PlanError

    Enumerates every aligned offset for <=12 buffers and <=4 banks. "infeasible" is returned only after exhaustive search; budget exhaustion is "limit".

    summarize

    source
    fn summarize(problem : Problem, layout : Layout) -> Array[BankUsage] raise PlanError

    Summary is defined for structurally valid layouts, including over-budget plans.

    trace_lifetimes

    source
    fn trace_lifetimes(trace : ExecutionTrace) -> Problem raise PlanError

    Import a complete logical last-use trace. Only recorded accesses are checked. Every ID describes one begin/end lifetime; steps are nondecreasing and inclusive.

    validate

    source
    fn validate(problem : Problem) -> Unit raise PlanError

    verify

    source
    fn verify(problem : Problem, layout : Layout) -> Array[Finding] raise PlanError

    Does not invoke the planner or trust a layout's size/lifetime metadata.

    Source Files

    Powered by MoonBit

    Site sourceReport issueModulesSkillsBuild queueStatistics

    © 2026 mooncakes.io