feat(scheduler): constrained-deadline EDF via processor-demand criterion (v0.3.0)

AxonOS-BCI · AxonOS-BCI · commit df9dee9e2f39 · 2026-05-29T16:51:19.000+08:00
Implements the first roadmap item of axonos-scheduler: constrained-deadline
task systems (D_i &lt;= T_i), previously implicit-deadline only.

- Task::periodic_with_deadline: explicit relative deadline (D_i &lt;= T_i)
- demand_bound: the demand-bound function dbf(t)
- processor_demand_feasible -&gt; Feasibility {Feasible|Infeasible{at,demand}|Uncertain}:
  exact feasibility by the processor-demand criterion (Baruah/Rosier/Howell 1990),
  integer-only, bounded, conservative (never reports Feasible unless every
  relevant deadline point was checked). Catches constrained-infeasible sets the
  utilisation bound admits.
- Kani harnesses S6 (dbf monotone) and S7 (dbf zero below first deadline)
- Workspace lockstep version bump to 0.3.0; KERNEL_ABI_VERSION unchanged (1)
- Additive only; implicit-deadline API unchanged; no unsafe introduced
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -10,6 +10,56 @@ The workspace versions all 8 crates lock-step (`axonos-capability`,
 
 ---
 
+## [v0.3.0] — 2026-05-29
+
+### Added — constrained-deadline scheduling (`axonos-scheduler`)
+
+The headline of this release: the scheduler now supports **constrained-deadline**
+task systems (`D_i <= T_i`), the first item on its roadmap. Previously only
+implicit-deadline systems (`D_i = T_i`) were supported.
+
+- **`Task::periodic_with_deadline(id, wcet, period, deadline)`** constructs a
+  task whose relative deadline is shorter than its period. The existing
+  `Task::periodic` (implicit deadline) is unchanged.
+- **`demand_bound(set, t)`** computes the demand-bound function `dbf(t)` — the
+  maximum cumulative execution demand of jobs whose release and deadline both
+  fall within an interval of length `t`.
+- **`processor_demand_feasible(set) -> Feasibility`** decides EDF feasibility
+  by the **processor-demand criterion** (Baruah, Rosier, and Howell, 1990).
+  Under constrained deadlines the Liu–Layland utilisation bound is necessary
+  but not sufficient; this test evaluates `dbf(t) <= t` at every deadline in
+  the La–Sha feasibility interval. It is **integer-only** (no floating point on
+  the analysis path) and **bounded**: it returns `Feasibility::Uncertain`
+  rather than risk an unsound pass, and never returns `Feasible` unless every
+  relevant deadline point was checked. The verdict is `Feasible`,
+  `Infeasible { at, demand }` (a definite counterexample), or `Uncertain`.
+- This catches a class of error the utilisation test cannot: a task set well
+  under `U = 1` can still miss a constrained deadline, and
+  `processor_demand_feasible` reports it as `Infeasible` with the violating
+  deadline and demand.
+- Two new Kani harnesses in `axonos-scheduler/kani-proofs`: `sched_dbf_monotone`
+  (dbf is monotone non-decreasing in `t`) and `sched_dbf_zero_below_first_deadline`
+  (dbf is zero below the first deadline).
+
+### Changed
+
+- All workspace crates and the workspace package version move to **0.3.0** in
+  lockstep; inter-crate path-dependency requirements updated accordingly. Only
+  `axonos-scheduler` carries functional changes in this release; the other
+  crates are versioned together as a coherent kernel release.
+- `axonos-scheduler` is the only crate with API changes, all **additive**: the
+  implicit-deadline API (`Task::periodic`, `TaskSet::admit`, `select_next`,
+  `response_time_bound`) is unchanged and backward-compatible.
+
+### Notes
+
+- `KERNEL_ABI_VERSION` remains **1**: the kernel ABI surface is unchanged. The
+  `Task` struct is unchanged (its `deadline` field already existed), so the
+  addition is source- and ABI-compatible.
+- No `unsafe` introduced; `axonos-scheduler` remains `#![forbid(unsafe_code)]`.
+
+---
+
 ## [v0.2.3] — 2026-05-27
 
 AxonOS-style refresh. No source-code or API changes — the v0.2.1
diff --git a/CITATION.cff b/CITATION.cff
@@ -20,5 +20,5 @@ keywords:
   - neurotechnology
   - rust
 license: [Apache-2.0, MIT]
-version: "0.2.3"
-date-released: "2026-05-27"
+version: "0.3.0"
+date-released: "2026-05-29"
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -18,7 +18,7 @@ exclude = [
 ]
 
 [workspace.package]
-version = "0.2.3"
+version = "0.3.0"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"
diff --git a/README.md b/README.md
@@ -4,7 +4,7 @@
 
 ### The verifiable substrate underneath a brain–computer interface.
 
-<sub>seven crates · 3 603 lines · 28 formal proofs · 66 tests · zero unsafe outside two operations</sub>
+<sub>seven crates · 30 formal proofs · 72 tests · zero unsafe outside two operations</sub>
 
 <br/>
 
@@ -130,7 +130,7 @@ and its specific dependencies.
 git clone https://github.com/AxonOS-org/axonos-kernel
 cd axonos-kernel
 cargo test --workspace
-# → 66 tests passed.
+# → 72 tests passed.
 ```
 
 ### One-minute integration
@@ -229,7 +229,7 @@ cd axonos-intent/kani-proofs     && cargo kani
 | T1–T6 | `axonos-time` | Monotonic arithmetic; saturation; clock observability |
 | I1–I5 | `axonos-intent` | Round-trip identity; strict decoder rejection of malformed input |
 
-**Total: 28 BMC harnesses.** Runnable against the published source.
+**Total: 30 BMC harnesses.** Runnable against the published source.
 
 ---
 
@@ -313,7 +313,7 @@ repository.
 
 | Phase | Window | Deliverable |
 |:---|:---|:---|
-| **Now** | May 2026 | Seven crates published. 66 tests, 28 Kani harnesses, CI green. |
+| **Now** | May 2026 | Seven crates published. Constrained-deadline scheduling (processor-demand criterion). 72 tests, 30 Kani harnesses, CI green. |
 | **Phase 1** | Q2 2026 | GPIO-instrumented WCRT measurement on STM32H573 reference fixture. Falsification protocol P1–P5 executed and published regardless of outcome. |
 | **Phase 2** | Q3–Q4 2026 | First 8-channel clinical kit deployment with the partner ALS rehabilitation centre. |
 | **Phase 3** | 2027 | FDA Pre-Submission. Ferrocene-qualified toolchain integration. ISO 14971 risk management file. |
diff --git a/axonos-capability/Cargo.toml b/axonos-capability/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "axonos-capability"
-version = "0.2.1"
+version = "0.3.0"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"
diff --git a/axonos-firmware-stm32f407/Cargo.toml b/axonos-firmware-stm32f407/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "axonos-firmware-stm32f407"
-version = "0.2.1"
+version = "0.3.0"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"
@@ -23,12 +23,12 @@ cortex-m-rt = "0.7"
 panic-halt = "0.2"
 
 # AxonOS workspace dependencies
-axonos-kernel-core = { version = "0.2.0", path = "../axonos-kernel-core" }
-axonos-time = { version = "0.2.0", path = "../axonos-time" }
-axonos-scheduler = { version = "0.2.0", path = "../axonos-scheduler" }
-axonos-capability = { version = "0.2.0", path = "../axonos-capability" }
-axonos-intent = { version = "0.2.0", path = "../axonos-intent" }
-axonos-spsc = { version = "0.2.0", path = "../axonos-spsc" }
+axonos-kernel-core = { version = "0.3.0", path = "../axonos-kernel-core" }
+axonos-time = { version = "0.3.0", path = "../axonos-time" }
+axonos-scheduler = { version = "0.3.0", path = "../axonos-scheduler" }
+axonos-capability = { version = "0.3.0", path = "../axonos-capability" }
+axonos-intent = { version = "0.3.0", path = "../axonos-intent" }
+axonos-spsc = { version = "0.3.0", path = "../axonos-spsc" }
 
 [[bin]]
 name = "axonos-firmware-stm32f407"
diff --git a/axonos-intent/Cargo.toml b/axonos-intent/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "axonos-intent"
-version = "0.2.1"
+version = "0.3.0"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"
@@ -15,8 +15,8 @@ default = []
 std = ["axonos-time/std"]
 
 [dependencies]
-axonos-time = { version = "0.2.0", path = "../axonos-time" }
-axonos-capability = { version = "0.2.0", path = "../axonos-capability" }
+axonos-time = { version = "0.3.0", path = "../axonos-time" }
+axonos-capability = { version = "0.3.0", path = "../axonos-capability" }
 
 [lib]
 name = "axonos_intent"
diff --git a/axonos-kernel-core/Cargo.toml b/axonos-kernel-core/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "axonos-kernel-core"
-version = "0.2.1"
+version = "0.3.0"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"
@@ -15,11 +15,11 @@ default = []
 std = ["axonos-time/std", "axonos-intent/std"]
 
 [dependencies]
-axonos-spsc = { version = "0.2.0", path = "../axonos-spsc" }
-axonos-scheduler = { version = "0.2.0", path = "../axonos-scheduler" }
-axonos-capability = { version = "0.2.0", path = "../axonos-capability" }
-axonos-time = { version = "0.2.0", path = "../axonos-time" }
-axonos-intent = { version = "0.2.0", path = "../axonos-intent" }
+axonos-spsc = { version = "0.3.0", path = "../axonos-spsc" }
+axonos-scheduler = { version = "0.3.0", path = "../axonos-scheduler" }
+axonos-capability = { version = "0.3.0", path = "../axonos-capability" }
+axonos-time = { version = "0.3.0", path = "../axonos-time" }
+axonos-intent = { version = "0.3.0", path = "../axonos-intent" }
 
 [lib]
 name = "axonos_kernel_core"
diff --git a/axonos-scheduler/Cargo.toml b/axonos-scheduler/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "axonos-scheduler"
-version = "0.2.1"
+version = "0.3.0"
 edition = "2021"
 rust-version = "1.75"
 license = "Apache-2.0 OR MIT"
diff --git a/axonos-scheduler/README.md b/axonos-scheduler/README.md
@@ -19,6 +19,8 @@ This crate contains:
 - Liu–Layland admission test (`TaskSet::admit`)
 - Synchronous busy-period response-time analysis (`response_time_bound`)
 - Earliest-deadline-first selection function (`select_next`)
+- Constrained-deadline feasibility by the processor-demand criterion
+  (`demand_bound`, `processor_demand_feasible`)
 
 This crate does NOT contain:
 
@@ -123,6 +125,8 @@ The crate ships with five Kani harnesses in `kani-proofs/`:
 | S3 | Tie-breaking is deterministic: lower `TaskId` wins |
 | S4 | Single-task RTA equals the task's WCET |
 | S5 | Empty task set is trivially schedulable with `R = 0` |
+| S6 | The demand-bound function `dbf(t)` is monotone non-decreasing in `t` |
+| S7 | Below the first deadline, `dbf(t) = 0` (no job's deadline has elapsed) |
 
 To reproduce:
 
@@ -141,18 +145,26 @@ rustup target add thumbv8m.main-none-eabihf # Cortex-M33 (STM32H573)
 cargo build --release --target thumbv7em-none-eabihf
 ```
 
-## Limitations and future work
-
-- **Implicit deadlines only.** Constrained-deadline (`D_i < T_i`) is not
-  yet supported. Required for some sensor-fusion workloads beyond BCI.
+## Capabilities and future work
+
+- **Constrained deadlines (`D_i <= T_i`) — supported since 0.3.0.** Tasks may
+  declare a relative deadline shorter than their period via
+  `Task::periodic_with_deadline`. Because the Liu–Layland utilisation bound is
+  necessary but not sufficient under constrained deadlines, feasibility is
+  decided exactly by the **processor-demand criterion** (Baruah, Rosier, and
+  Howell, 1990): `processor_demand_feasible` evaluates the demand-bound
+  function `dbf(t)` at every deadline in the La–Sha feasibility interval. The
+  test is integer-only and bounded; it returns `Uncertain` rather than risk an
+  unsound pass, and never reports `Feasible` unless every relevant deadline
+  point was checked.
 - **No mixed-criticality.** Mixed-criticality EDF-VD (Vestal 2007) is a
   natural extension for the safety-critical regulatory pathway.
 - **No blocking.** Tasks with shared resources (mutexes, semaphores) are
   not yet modelled. The current contract is that all tasks are
   independent. Blocking will require the priority-inheritance or
   priority-ceiling protocol, which is a separate body of work.
 
-These limitations are explicit. They will be addressed in subsequent
+The remaining limitations are explicit. They will be addressed in subsequent
 versions of this crate or in a successor crate (e.g.,
 `axonos-scheduler-mcs`).
 
diff --git a/axonos-scheduler/kani-proofs/src/main.rs b/axonos-scheduler/kani-proofs/src/main.rs
diff --git a/axonos-scheduler/src/lib.rs b/axonos-scheduler/src/lib.rs
diff --git a/axonos-spsc/Cargo.toml b/axonos-spsc/Cargo.toml
diff --git a/axonos-time/Cargo.toml b/axonos-time/Cargo.toml

Original file line number	Diff line number	Diff line change
`@@ -18,7 +18,7 @@ exclude = [`
`18`	`18`	`]`
`19`	`19`
`20`	`20`	`[workspace.package]`
`21`		`-version = "0.2.3"`
	`21`	`+version = "0.3.0"`
`22`	`22`	`edition = "2021"`
`23`	`23`	`rust-version = "1.75"`
`24`	`24`	`license = "Apache-2.0 OR MIT"`