Phase 3: Sharding (The Distribution Axis)

This directory contains the formal specification and implementation plan for Phase 3 of the Kina research program.

Overview

Phase 3 elevates device meshes and distributed tensor sharding into the core type system. Rather than treating distributed execution as a runtime optimization or a bolted-on library, Kina models it as a formal type refinement. A tensor's type mathematically enforces its layout across a mesh of accelerators.

This phase is based on the theoretical foundation that sharding is a structural refinement, and re-sharding (e.g., all-reduce, all-gather) is a type-changing coercion.

Documents

• 01: Scope, Milestones, and Exit Criteria - The project plan and abandonment triggers.
• 02: Mesh and Sharding Types - The core calculus extensions for device meshes and sharding rules.
• 03: GSPMD Propagation - The type inference engine for deducing sharding constraints.
• 04: Collective Coercions - Lowering sharding mismatches to NCCL/Gloo collective operations.
• 05: StoryLM-0 Workload - First numeric instance: 2-way column-parallel lm_head as slice / matmul / concat. Mesh types stay unimplemented.
• 06: StoryLM-0 Head-Parallel - 2-way head-parallel attention as slice / rank-4 matmul / concat. Mesh types stay unimplemented.
• 07: StoryLM-0 Projection Shards - 2-way column-parallel Wq/Wk/Wv as slice / rank-3 matmul / per-head attention / concat. Mesh types stay unimplemented.