ywkang
168b0c89f0
Follow-up to the bilingual-structure commit: docs/adr-ko/ now holds only Korean versions (24 files translated from English placeholders), ADR-0013 slug uses kebab-case in both folders, and the verify tool allows translated parenthetical commentary in the Status block. - Translate 24 English files in docs/adr-ko/ to Korean. The previous bilingual-structure commit had left these as English copies because their source content was already English; this commit fulfills the policy that docs/adr-ko/ contains only Korean. - Rename ADR-0013 in both adr/ and adr-ko/ from ver-verification_strategy.md to ver-verification-strategy.md (kebab-case consistency with other ADRs). - CLAUDE.md (ADR Translation Discipline): clarify that only the Status lifecycle keyword (Accepted / Proposed / Stub / Draft / Superseded by ADR-NNNN / Merged into ADR-NNNN) must match across EN and KO; parenthetical commentary and trailing list items may be translated. - tools/verify_adr_lang_pairs.py: replace byte-equal Status check with normalize_status_keyword() which strips parenthetical commentary and takes only the first non-empty line. - tests/test_verify_adr_lang_pairs.py: update existing test names, add coverage for translated parenthetical, translated trailing list, and Superseded-by-NNNN keyword equality. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
140 lines
3.7 KiB
Markdown
140 lines
3.7 KiB
Markdown
# ADR-0013: Verification Strategy and Phase 1 Test Plan
|
|
|
|
## Status
|
|
|
|
Accepted
|
|
|
|
## Context
|
|
|
|
KernBench is a system-level simulator whose correctness is defined by:
|
|
|
|
- adherence to SPEC-defined invariants,
|
|
- determinism and debuggability,
|
|
- explicit modeling of routing and latency.
|
|
|
|
Given the evolving implementation, we need a stable verification strategy
|
|
that prevents architectural drift while allowing incremental development.
|
|
|
|
This ADR defines the Phase 1 verification plan and what constitutes
|
|
"correct behavior" for early implementations.
|
|
|
|
---
|
|
|
|
## Decision
|
|
|
|
### D1. Verification is contract-based
|
|
|
|
Verification MUST be derived from:
|
|
|
|
- SPEC requirements,
|
|
- accepted ADRs.
|
|
|
|
Tests MUST validate architectural contracts, not incidental implementation details.
|
|
|
|
---
|
|
|
|
### D2. Phase 1 verification scope
|
|
|
|
Phase 1 verification focuses on:
|
|
|
|
- message contract validity (ADR-0012),
|
|
- routing and fan-out semantics at the IO_CPU boundary (ADR-0009),
|
|
- PA-first memory addressing and shard tagging (ADR-0011),
|
|
- core latency and trace invariants (SPEC 0.1, R2).
|
|
|
|
Microarchitectural accuracy, bandwidth contention, and cycle-level behavior
|
|
are explicitly out of scope in Phase 1.
|
|
|
|
---
|
|
|
|
### D3. Required Phase 1 verification cases
|
|
|
|
The following verification cases MUST be supported by the implementation:
|
|
|
|
#### V1. Message schema validation
|
|
|
|
- KernelLaunch requests missing `(sip, cube, pe)` in any tensor shard MUST be rejected.
|
|
- MemoryWrite/MemoryRead requests missing destination/source placement tags MUST be rejected.
|
|
- Completion results MUST follow the `ok / error_code / error_message` contract.
|
|
|
|
#### V2. IO_CPU fan-out and aggregation
|
|
|
|
Given:
|
|
|
|
- a topology with one SIP, one CUBE, and two PEs,
|
|
- a KernelLaunch request containing two tensor shards targeting different PEs,
|
|
|
|
The system MUST:
|
|
|
|
- submit a single KernelLaunch to IO_CPU,
|
|
- fan-out work internally to both PEs,
|
|
- aggregate completion and return a single deterministic completion to the host.
|
|
|
|
#### V3. Latency and trace invariants
|
|
|
|
For any valid request:
|
|
|
|
- the hop-by-hop trace MUST be non-empty,
|
|
- total latency MUST be greater than zero,
|
|
- repeated runs with identical inputs MUST produce identical traces.
|
|
|
|
#### V4. Topology independence and cross-domain coverage
|
|
|
|
Verification cases MUST pass for multiple topology shapes, including:
|
|
|
|
- minimal: (1 SIP, 1 CUBE, 1 PE)
|
|
- multi-PE: (1 SIP, 1 CUBE, N PEs)
|
|
- multi-CUBE within a SIP: (1 SIP, M CUBEs, ≥1 PE per CUBE)
|
|
- multi-SIP tray: (K SIPs, ≥1 CUBE per SIP, ≥1 PE per CUBE)
|
|
|
|
For multi-CUBE and multi-SIP topologies, Phase 1 verification focuses on:
|
|
|
|
- explicit connectivity (required links exist),
|
|
- deterministic routing and control-path traversal,
|
|
- non-empty traces and latency > 0 for representative cross-domain requests
|
|
(inter-CUBE and inter-SIP paths).
|
|
|
|
Tests MUST NOT hardcode topology sizes, node ids, or link counts.
|
|
Instead, tests MUST derive expectations from the compiled topology metadata
|
|
---
|
|
|
|
### D4. Phase 1 artifacts
|
|
|
|
Phase 1 MAY include:
|
|
|
|
- verification-only test code,
|
|
- topology fixtures,
|
|
- trace inspection utilities.
|
|
|
|
Phase 1 MUST NOT require:
|
|
|
|
- production code changes solely to satisfy tests,
|
|
- weakening or removing tests to allow progress.
|
|
|
|
---
|
|
|
|
### D5. Phase 2 enforcement
|
|
|
|
Phase 2 (Apply) MUST:
|
|
|
|
- run the Phase 1 verification cases,
|
|
- rollback all changes if any verification fails,
|
|
- preserve tests as authoritative contracts.
|
|
|
|
---
|
|
|
|
## Consequences
|
|
|
|
- Architectural correctness is enforced early.
|
|
- Tests serve as executable documentation of system behavior.
|
|
- Implementation remains flexible without losing rigor.
|
|
|
|
---
|
|
|
|
## Links
|
|
|
|
- SPEC 0.1, R2, R6
|
|
- ADR-0011 (Memory Addressing — PA / VA / LA)
|
|
- ADR-0012 (Host ↔ IO_CPU message schema)
|
|
- ADR-0009 (Kernel execution semantics)
|