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.