From f0edc5f6c9dcde4e39aeeace3675448195da9f84 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Tue, 16 Jun 2026 17:43:40 +0900 Subject: [PATCH 01/22] feat(async): add task::kill() for force-terminating async tasks Adds `task::kill(task_id)` to `awkernel_async_lib`, which marks a task as `Terminated` and removes it from the global TASKS registry. Also fixes a race in `run_main()` where `Poll::Pending` could overwrite a `Terminated` state set by a concurrent `kill()` call. Phase 0 of the PCIe detach roadmap. Co-Authored-By: Claude Sonnet 4.6 --- awkernel_async_lib/src/task.rs | 63 ++++++++++++++++++++++++++++++---- 1 file changed, 56 insertions(+), 7 deletions(-) diff --git a/awkernel_async_lib/src/task.rs b/awkernel_async_lib/src/task.rs index 8f0235260..4bad6934c 100644 --- a/awkernel_async_lib/src/task.rs +++ b/awkernel_async_lib/src/task.rs @@ -882,13 +882,16 @@ pub fn run_main() { match result { Ok(Poll::Pending) => { - // The task has not been terminated yet. - info.state = State::Waiting; - - if info.need_sched { - info.need_sched = false; - drop(info); - task.clone().wake(); + // A concurrent kill() may have set state = Terminated while we were polling. + // Do not overwrite it back to Waiting, and do not re-enqueue. + if !matches!(info.state, State::Terminated | State::Panicked) { + info.state = State::Waiting; + + if info.need_sched { + info.need_sched = false; + drop(info); + task.clone().wake(); + } } } Ok(Poll::Ready(result)) => { @@ -947,6 +950,52 @@ pub fn wake(task_id: u32) { gurad.wake(task_id); } +/// Force-terminate a task by its ID. +/// +/// Sets the task state to `Terminated` and removes it from the global task registry. +/// Any subsequent `wake()` call for this task will be a no-op. If the task was in +/// `Waiting` state, wakers may still hold `Arc` references; the `Task` is freed +/// only after those wakers are dropped — the caller is responsible for deregistering them. +/// +/// Returns `true` if the task was found and killed, `false` if it was not found or was +/// already in a terminal state. +pub fn kill(task_id: u32) -> bool { + // Step 1: Clone the Arc out of TASKS without holding TASKS while acquiring + // the per-task info lock (preserves the established lock ordering: TASKS is + // never held while info is locked by the executor or wake()). + let task = { + let mut node = MCSNode::new(); + let tasks = TASKS.lock(&mut node); + match tasks.id_to_task.get(&task_id) { + Some(t) => t.clone(), + None => return false, + } + }; + + // Step 2: Under the info lock, transition state to Terminated. + // This prevents any concurrent wake() from re-enqueuing the task via the + // existing `Terminated | Panicked => return` guard in Task::wake(). + { + let mut node = MCSNode::new(); + let mut info = task.info.lock(&mut node); + match info.state { + State::Terminated | State::Panicked => return false, + _ => info.state = State::Terminated, + } + } + + // Step 3: Remove the task from the global registry, decrementing the Arc refcount. + // Tasks::remove() is a BTreeMap::remove, so calling it on a missing key (e.g., if the + // future completed naturally at the same time) is a no-op. + { + let mut node = MCSNode::new(); + let mut tasks = TASKS.lock(&mut node); + tasks.remove(task_id); + } + + true +} + pub fn get_tasks() -> Vec> { let mut result = Vec::new(); From a96d470aae651c21cb7d07f5926cfb7db42ba4c7 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Tue, 16 Jun 2026 18:00:55 +0900 Subject: [PATCH 02/22] test(async): add test_task_kill application for task::kill() Adds a kernel test application that verifies task::kill() semantics at runtime: killing a sleeping task removes it from the registry, killing an unknown ID returns false, and a second kill on a dead task returns false. Co-Authored-By: Claude Sonnet 4.6 --- applications/tests/test_task_kill/Cargo.toml | 15 ++++ applications/tests/test_task_kill/src/lib.rs | 74 ++++++++++++++++++++ kernel/Cargo.toml | 1 + userland/Cargo.toml | 5 ++ userland/src/lib.rs | 3 + 5 files changed, 98 insertions(+) create mode 100644 applications/tests/test_task_kill/Cargo.toml create mode 100644 applications/tests/test_task_kill/src/lib.rs diff --git a/applications/tests/test_task_kill/Cargo.toml b/applications/tests/test_task_kill/Cargo.toml new file mode 100644 index 000000000..2152dea3b --- /dev/null +++ b/applications/tests/test_task_kill/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "test_task_kill" +version = "0.1.0" +edition = "2021" + +[dependencies] +log = "0.4" + +[dependencies.awkernel_async_lib] +path = "../../../awkernel_async_lib" +default-features = false + +[dependencies.awkernel_lib] +path = "../../../awkernel_lib" +default-features = false diff --git a/applications/tests/test_task_kill/src/lib.rs b/applications/tests/test_task_kill/src/lib.rs new file mode 100644 index 000000000..37a025f3e --- /dev/null +++ b/applications/tests/test_task_kill/src/lib.rs @@ -0,0 +1,74 @@ +#![no_std] + +extern crate alloc; + +use awkernel_async_lib::{scheduler::SchedulerType, sleep, task}; +use core::time::Duration; + +pub async fn run() { + sleep(Duration::from_secs(1)).await; + log::info!("TASK_KILL_TEST start"); + + kill_sleeping_task().await; + kill_unknown_id(); + kill_idempotent().await; + + log::info!("TASK_KILL_TEST done"); +} + +async fn kill_sleeping_task() { + let id = task::spawn( + "kill-target".into(), + async { + loop { + sleep(Duration::from_secs(3600)).await; + } + }, + SchedulerType::PrioritizedFIFO(0), + ); + + sleep(Duration::from_millis(50)).await; + + if task::kill(id) { + log::info!("TASK_KILL_TEST kill_sleeping_task: PASS (kill returned true)"); + } else { + log::error!("TASK_KILL_TEST kill_sleeping_task: FAIL (kill returned false)"); + } + + sleep(Duration::from_millis(50)).await; + + if task::get_task(id).is_none() { + log::info!("TASK_KILL_TEST task_removed_from_registry: PASS"); + } else { + log::error!("TASK_KILL_TEST task_removed_from_registry: FAIL (still in registry)"); + } +} + +fn kill_unknown_id() { + if !task::kill(u32::MAX) { + log::info!("TASK_KILL_TEST kill_unknown_id: PASS"); + } else { + log::error!("TASK_KILL_TEST kill_unknown_id: FAIL (returned true for unknown id)"); + } +} + +async fn kill_idempotent() { + let id = task::spawn( + "kill-twice".into(), + async { + loop { + sleep(Duration::from_secs(3600)).await; + } + }, + SchedulerType::PrioritizedFIFO(0), + ); + + sleep(Duration::from_millis(50)).await; + task::kill(id); + + if !task::kill(id) { + log::info!("TASK_KILL_TEST kill_idempotent: PASS (second kill returned false)"); + } else { + log::error!("TASK_KILL_TEST kill_idempotent: FAIL (second kill returned true)"); + } +} diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml index c08007c6e..6141bde0a 100644 --- a/kernel/Cargo.toml +++ b/kernel/Cargo.toml @@ -136,3 +136,4 @@ aarch64_virt = [ spinlock = ["awkernel_lib/spinlock"] linux = [] test_partitioned_edf = ["userland/test_partitioned_edf"] +test_task_kill = ["userland/test_task_kill"] diff --git a/userland/Cargo.toml b/userland/Cargo.toml index 6e5b64012..85fb3c681 100644 --- a/userland/Cargo.toml +++ b/userland/Cargo.toml @@ -82,6 +82,10 @@ optional = true path = "../applications/tests/test_partitioned_edf" optional = true +[dependencies.test_task_kill] +path = "../applications/tests/test_task_kill" +optional = true + [features] default = [] perf = ["awkernel_services/perf"] @@ -104,3 +108,4 @@ test_measure_channel_heavy = ["dep:test_measure_channel_heavy"] test_dag = ["dep:test_dag"] test_voluntary_preemption = ["dep:test_voluntary_preemption"] test_partitioned_edf = ["dep:test_partitioned_edf"] +test_task_kill = ["dep:test_task_kill"] diff --git a/userland/src/lib.rs b/userland/src/lib.rs index 1b64e34b4..9ad886db1 100644 --- a/userland/src/lib.rs +++ b/userland/src/lib.rs @@ -58,5 +58,8 @@ pub async fn main() -> Result<(), Cow<'static, str>> { #[cfg(feature = "test_partitioned_edf")] test_partitioned_edf::run().await; // test for Partitioned EDF scheduler + #[cfg(feature = "test_task_kill")] + test_task_kill::run().await; // test for task::kill() + Ok(()) } From c0558622d16b1eece9c9ac7b0b8f90ec566ef79d Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Tue, 16 Jun 2026 18:44:36 +0900 Subject: [PATCH 03/22] test(task): verify resource cleanup after kill() Adds resources_freed_after_kill() to the test_task_kill application. A DropTracker struct increments a global counter on drop; the test kills the owner task while it is sleeping and confirms the counter reaches 1 after the sleep timer fires and releases the last Arc. Co-Authored-By: Claude Sonnet 4.6 --- applications/tests/test_task_kill/src/lib.rs | 52 +++++++++++++++++++- 1 file changed, 51 insertions(+), 1 deletion(-) diff --git a/applications/tests/test_task_kill/src/lib.rs b/applications/tests/test_task_kill/src/lib.rs index 37a025f3e..525e997c1 100644 --- a/applications/tests/test_task_kill/src/lib.rs +++ b/applications/tests/test_task_kill/src/lib.rs @@ -3,7 +3,20 @@ extern crate alloc; use awkernel_async_lib::{scheduler::SchedulerType, sleep, task}; -use core::time::Duration; +use core::{ + sync::atomic::{AtomicUsize, Ordering}, + time::Duration, +}; + +static DROP_COUNT: AtomicUsize = AtomicUsize::new(0); + +struct DropTracker; + +impl Drop for DropTracker { + fn drop(&mut self) { + DROP_COUNT.fetch_add(1, Ordering::Release); + } +} pub async fn run() { sleep(Duration::from_secs(1)).await; @@ -12,6 +25,7 @@ pub async fn run() { kill_sleeping_task().await; kill_unknown_id(); kill_idempotent().await; + resources_freed_after_kill().await; log::info!("TASK_KILL_TEST done"); } @@ -72,3 +86,39 @@ async fn kill_idempotent() { log::error!("TASK_KILL_TEST kill_idempotent: FAIL (second kill returned true)"); } } + +async fn resources_freed_after_kill() { + DROP_COUNT.store(0, Ordering::Release); + + // The task owns a DropTracker and sleeps 200 ms per iteration. + // sleep() stores the Waker in a timer closure, which holds the last Arc + // reference after kill() removes the task from TASKS. When the timer fires + // the closure drops the Waker → Arc → 0 → Future → DropTracker::drop(). + let id = task::spawn( + "drop-tracker-task".into(), + async { + let _tracker = DropTracker; + loop { + sleep(Duration::from_millis(200)).await; + } + }, + SchedulerType::PrioritizedFIFO(0), + ); + + // Let the task enter its first 200 ms sleep (Waiting state). + sleep(Duration::from_millis(50)).await; + + task::kill(id); + + // Wait for the timer to fire (~150 ms remaining) plus a safety margin. + sleep(Duration::from_millis(300)).await; + + if DROP_COUNT.load(Ordering::Acquire) == 1 { + log::info!("TASK_KILL_TEST resources_freed_after_kill: PASS"); + } else { + log::error!( + "TASK_KILL_TEST resources_freed_after_kill: FAIL (drop_count={})", + DROP_COUNT.load(Ordering::Acquire) + ); + } +} From 47697206dc4292f9cf80f73f2e8bf6149d5e5567 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Tue, 16 Jun 2026 18:44:45 +0900 Subject: [PATCH 04/22] fix(display): exit early when no framebuffer is available MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit In nographic mode QEMU provides no GOP framebuffer, so draw() returns Err(NoFrameBuffer) immediately. Instead of ignoring the error and looping every 5 seconds forever, probe on startup and return if there is nothing to draw — eliminating needless scheduler churn and making the service self-cleaning in headless environments. Co-Authored-By: Claude Sonnet 4.6 --- applications/awkernel_display/src/lib.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/applications/awkernel_display/src/lib.rs b/applications/awkernel_display/src/lib.rs index 15a41b2a9..0f0a81c5a 100644 --- a/applications/awkernel_display/src/lib.rs +++ b/applications/awkernel_display/src/lib.rs @@ -14,7 +14,11 @@ use embedded_graphics::{ }; pub async fn run() { - let mut x = false; + if draw(false).is_err() { + return; + } + + let mut x = true; loop { let _ = draw(x); awkernel_async_lib::sleep(Duration::from_secs(5)).await; From adb164785863dae88dc5cb0d1013ec2dd8a62fd2 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Tue, 16 Jun 2026 19:05:22 +0900 Subject: [PATCH 05/22] fix(sleep): release state lock before waker.wake() to prevent deadlock MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit When task::kill() removes a task from TASKS, the timer closure for that task's ongoing sleep() becomes the sole Arc holder. If the timer fires before the Arc refcount reaches zero, the closure calls waker.wake() while still holding the Sleep state mutex. For a Terminated task, wake() returns immediately and drops the Arc inline; that triggers Task::drop() → Future::drop() → Sleep::drop(), which tries to re-acquire the same state mutex — instant spinlock deadlock, hanging the timer thread and blocking all subsequent sleeps. Fix: capture the wake decision under the state lock, release the lock, then call waker.wake() only if the state was Wait. Sleep::drop() now sees State::Finished and exits without trying to lock. Reproducer: test_task_kill::resources_freed_after_kill() kills a task mid-sleep(200ms); the 200ms timer then fires and previously deadlocked the scheduler, leaving the test task's own sleep(300ms) never waking up. Co-Authored-By: Claude Sonnet 4.6 --- awkernel_async_lib/src/sleep_task.rs | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/awkernel_async_lib/src/sleep_task.rs b/awkernel_async_lib/src/sleep_task.rs index eb36c9cb3..b361cb5dd 100644 --- a/awkernel_async_lib/src/sleep_task.rs +++ b/awkernel_async_lib/src/sleep_task.rs @@ -47,10 +47,21 @@ impl Future for Sleep { // Invoke `sleep_handler` after `self.dur` time. scheduler::sleep_task( Box::new(move || { - let mut node = MCSNode::new(); - let mut guard = state.lock(&mut node); - if let State::Wait = &*guard { - *guard = State::Finished; + // Release the state lock before calling waker.wake(). + // If kill() removed the task from TASKS, wake() drops the last + // Arc inline, which chains into Sleep::drop(), which tries + // to re-acquire the same state lock — deadlock if still held. + let should_wake = { + let mut node = MCSNode::new(); + let mut guard = state.lock(&mut node); + if let State::Wait = &*guard { + *guard = State::Finished; + true + } else { + false + } + }; + if should_wake { waker.wake(); } }), From 330623dcc2d433643591eecf4b5245796a1f2188 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Tue, 16 Jun 2026 19:09:16 +0900 Subject: [PATCH 06/22] Revert "fix(display): exit early when no framebuffer is available" This reverts commit 47697206dc4292f9cf80f73f2e8bf6149d5e5567. --- applications/awkernel_display/src/lib.rs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/applications/awkernel_display/src/lib.rs b/applications/awkernel_display/src/lib.rs index 0f0a81c5a..15a41b2a9 100644 --- a/applications/awkernel_display/src/lib.rs +++ b/applications/awkernel_display/src/lib.rs @@ -14,11 +14,7 @@ use embedded_graphics::{ }; pub async fn run() { - if draw(false).is_err() { - return; - } - - let mut x = true; + let mut x = false; loop { let _ = draw(x); awkernel_async_lib::sleep(Duration::from_secs(5)).await; From 6130429ba9fe60bc884866990102d369befdcae7 Mon Sep 17 00:00:00 2001 From: ytakano Date: Tue, 16 Jun 2026 19:59:38 +0900 Subject: [PATCH 07/22] Potential fix for pull request finding Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> --- awkernel_async_lib/src/task.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/awkernel_async_lib/src/task.rs b/awkernel_async_lib/src/task.rs index 4bad6934c..6f583b166 100644 --- a/awkernel_async_lib/src/task.rs +++ b/awkernel_async_lib/src/task.rs @@ -960,9 +960,9 @@ pub fn wake(task_id: u32) { /// Returns `true` if the task was found and killed, `false` if it was not found or was /// already in a terminal state. pub fn kill(task_id: u32) -> bool { - // Step 1: Clone the Arc out of TASKS without holding TASKS while acquiring - // the per-task info lock (preserves the established lock ordering: TASKS is - // never held while info is locked by the executor or wake()). + // Step 1: Clone the Arc out of TASKS, then drop TASKS before acquiring the per-task info lock. + // This keeps the TASKS critical section short and avoids lock-order inversions with code paths + // that may lock TASKS and then lock task.info (e.g., task::wake()). let task = { let mut node = MCSNode::new(); let tasks = TASKS.lock(&mut node); From e0b3363e4494f93a27609024d6df9dbd6f8cf59a Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 07:43:38 +0900 Subject: [PATCH 08/22] fix(task): safely kill Preempted tasks via kill_pending deferred termination MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Introduce kill_pending flag in TaskInfo (cfg not no_preempt): when kill() is called on a State::Preempted task, set the flag instead of overwriting state. yield_preempted_and_wake_task() unconditionally writes State::Preempted which would clobber a direct State::Terminated write, so deferral is required. - Poll::Pending handler in run_main() checks take_kill_pending() and finalizes termination (state=Terminated + TASKS.remove) at the task's next await point. - Drop the Arc in run_main() before calling yield_and_pool(ctx) so the thread pool does not hold a stale reference. Without this drop, the pooled thread's task Arc would only be released on the next preemption, which may never happen after kill() — leaving the future (and its DropTracker) alive. - Fix do_preemption() TOCTOU: keep the Arc from the first get_task() lookup alive through the entire function, removing the second unwrap() lookup and handling the None case (task already removed by kill()) gracefully. - Add kill_preempted_task() test using PrioritizedRR to exercise the deferred kill path; verify kill() returns true, task leaves TASKS, and DropTracker fires. Co-Authored-By: Claude Sonnet 4.6 --- applications/tests/test_task_kill/src/lib.rs | 61 ++++++++++++++++++++ awkernel_async_lib/src/task.rs | 60 +++++++++++++++++-- awkernel_async_lib/src/task/preempt.rs | 25 ++++---- 3 files changed, 129 insertions(+), 17 deletions(-) diff --git a/applications/tests/test_task_kill/src/lib.rs b/applications/tests/test_task_kill/src/lib.rs index 525e997c1..f1cb54daa 100644 --- a/applications/tests/test_task_kill/src/lib.rs +++ b/applications/tests/test_task_kill/src/lib.rs @@ -26,6 +26,7 @@ pub async fn run() { kill_unknown_id(); kill_idempotent().await; resources_freed_after_kill().await; + kill_preempted_task().await; log::info!("TASK_KILL_TEST done"); } @@ -87,6 +88,66 @@ async fn kill_idempotent() { } } +async fn kill_preempted_task() { + log::info!("TASK_KILL_TEST kill_preempted_task: step 1 start"); + DROP_COUNT.store(0, Ordering::Release); + + // Spin-loop followed by a short sleep: the spin phase is interrupted by the timer + // preemption interrupt, putting the task in State::Preempted. PrioritizedRR enables + // time-slicing preemption; PrioritizedFIFO does not. The sleep gives the deferred + // kill_pending machinery an await point to trigger on. + let id = task::spawn( + "preempt-target".into(), + async { + let _tracker = DropTracker; + loop { + for _ in 0..500_000u64 { + core::hint::spin_loop(); + } + sleep(Duration::from_millis(10)).await; + } + }, + SchedulerType::PrioritizedRR(0), + ); + + log::info!("TASK_KILL_TEST kill_preempted_task: step 2 spawned id={}", id); + + // Allow the task to run and be preempted at least once. + sleep(Duration::from_millis(50)).await; + + log::info!("TASK_KILL_TEST kill_preempted_task: step 3 after sleep 50ms"); + + // kill() may find the task in Preempted, Running, or Waiting state. + let killed = task::kill(id); + + log::info!("TASK_KILL_TEST kill_preempted_task: step 4 kill={}", killed); + + if !killed { + log::error!("TASK_KILL_TEST kill_preempted_task: FAIL (kill returned false)"); + return; + } + + // If the task was Preempted when killed, it resumes via yield_and_pool and terminates + // at the next await (sleep 10 ms). Allow enough margin for that path. + sleep(Duration::from_millis(300)).await; + + log::info!("TASK_KILL_TEST kill_preempted_task: step 5 after sleep 300ms"); + + if task::get_task(id).is_some() { + log::error!("TASK_KILL_TEST kill_preempted_task: FAIL (task still in registry)"); + return; + } + + if DROP_COUNT.load(Ordering::Acquire) == 1 { + log::info!("TASK_KILL_TEST kill_preempted_task: PASS"); + } else { + log::error!( + "TASK_KILL_TEST kill_preempted_task: FAIL (drop_count={})", + DROP_COUNT.load(Ordering::Acquire) + ); + } +} + async fn resources_freed_after_kill() { DROP_COUNT.store(0, Ordering::Release); diff --git a/awkernel_async_lib/src/task.rs b/awkernel_async_lib/src/task.rs index 6f583b166..23953a64f 100644 --- a/awkernel_async_lib/src/task.rs +++ b/awkernel_async_lib/src/task.rs @@ -170,6 +170,14 @@ pub struct TaskInfo { #[cfg(not(feature = "no_preempt"))] thread: Option, + + // Set by kill() when the task is in State::Preempted. The worker thread is + // suspended mid-execution; this flag defers actual termination to the next + // Poll::Pending return (i.e., the task's next await point). + // Unlike setting State::Terminated directly, this flag survives re-preemptions + // because yield_preempted_and_wake_task() overwrites the state field unconditionally. + #[cfg(not(feature = "no_preempt"))] + kill_pending: bool, } impl TaskInfo { @@ -186,6 +194,14 @@ impl TaskInfo { self.thread = Some(ctx) } + #[inline(always)] + fn take_kill_pending(&mut self) -> bool { + #[cfg(not(feature = "no_preempt"))] + return core::mem::take(&mut self.kill_pending); + #[cfg(feature = "no_preempt")] + false + } + #[inline(always)] pub fn get_state(&self) -> State { self.state @@ -318,6 +334,9 @@ impl Tasks { #[cfg(not(feature = "no_preempt"))] thread: None, + + #[cfg(not(feature = "no_preempt"))] + kill_pending: false, }); // Set the task priority. @@ -780,6 +799,12 @@ pub fn run_main() { if let Some(ctx) = info.take_preempt_context() { info.update_last_executed(); drop(info); + // Drop our Arc before this thread is pooled inside yield_and_pool. + // The preempted task's original worker thread holds its own Arc, so the + // task is not freed here. Without this drop, the pooled thread would hold + // a stale Arc that is only released when the thread is taken from the pool + // for a future preemption — which may never happen after kill(). + drop(task); #[cfg(feature = "perf")] perf::start_context_switch(); @@ -885,12 +910,22 @@ pub fn run_main() { // A concurrent kill() may have set state = Terminated while we were polling. // Do not overwrite it back to Waiting, and do not re-enqueue. if !matches!(info.state, State::Terminated | State::Panicked) { - info.state = State::Waiting; - - if info.need_sched { - info.need_sched = false; + if info.take_kill_pending() { + // Deferred kill: task was Preempted when kill() was called. + // Now at an await boundary, complete the termination. + info.state = State::Terminated; drop(info); - task.clone().wake(); + let mut node = MCSNode::new(); + let mut tasks = TASKS.lock(&mut node); + tasks.remove(task.id); + } else { + info.state = State::Waiting; + + if info.need_sched { + info.need_sched = false; + drop(info); + task.clone().wake(); + } } } } @@ -980,6 +1015,20 @@ pub fn kill(task_id: u32) -> bool { let mut info = task.info.lock(&mut node); match info.state { State::Terminated | State::Panicked => return false, + #[cfg(not(feature = "no_preempt"))] + State::Preempted => { + if info.kill_pending { + return false; + } + // The worker thread is suspended inside poll_unpin mid-execution. + // Directly setting Terminated is unsafe: yield_preempted_and_wake_task() + // unconditionally overwrites the state field to Preempted on the next + // re-preemption, losing the Terminated signal. Instead, set kill_pending + // so run_main() completes the termination once the thread yields at its + // next await point. The task stays in TASKS until then. + info.kill_pending = true; + return true; + } _ => info.state = State::Terminated, } } @@ -987,6 +1036,7 @@ pub fn kill(task_id: u32) -> bool { // Step 3: Remove the task from the global registry, decrementing the Arc refcount. // Tasks::remove() is a BTreeMap::remove, so calling it on a missing key (e.g., if the // future completed naturally at the same time) is a no-op. + // Skipped for State::Preempted (handled above via kill_pending). { let mut node = MCSNode::new(); let mut tasks = TASKS.lock(&mut node); diff --git a/awkernel_async_lib/src/task/preempt.rs b/awkernel_async_lib/src/task/preempt.rs index b1129cec4..e3bf06b8f 100644 --- a/awkernel_async_lib/src/task/preempt.rs +++ b/awkernel_async_lib/src/task/preempt.rs @@ -135,14 +135,21 @@ unsafe fn do_preemption() { return; }; - { - let current_task = get_task(current_task_id).unwrap(); - - if current_task > next { + // Obtain the Arc for the currently-running task. + // If kill() has already removed it from TASKS, abort preemption and re-enqueue next. + let current_task = match get_task(current_task_id) { + Some(t) => t, + None => { remove_preemption_pending(cpu_id, next.id); next.scheduler.wake_task(next); return; } + }; + + if current_task > next { + remove_preemption_pending(cpu_id, next.id); + next.scheduler.wake_task(next); + return; } // If a new preemption-pending task with the highest priority is pushed from peek_preemption_pending() to here, the subsequent re-wake may cause a infinite loop. @@ -158,14 +165,8 @@ unsafe fn do_preemption() { p.scheduler.wake_task(p); } - // If there is a task to be invoked next, execute the task. - let current_task = { - let mut node = MCSNode::new(); - let tasks = super::TASKS.lock(&mut node); - let current_task = tasks.id_to_task.get(¤t_task_id).unwrap(); - current_task.clone() - }; - + // current_task Arc is kept alive from the lookup above — no second TASKS lock needed. + // This also closes the TOCTOU window where kill() could remove the task between two lookups. if let Some(next_thread) = { let mut node = MCSNode::new(); let mut task_info = next.info.lock(&mut node); From 17b04f09cc7cc228a26df0801dd6a07bf9327e9e Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 13:15:14 +0900 Subject: [PATCH 09/22] Update task kill semantics tests and add repository guidelines --- AGENTS.md | 54 ++++++++++++++++++++ applications/tests/test_task_kill/src/lib.rs | 29 +++++++++++ awkernel_async_lib/src/task.rs | 8 +++ 3 files changed, 91 insertions(+) create mode 100644 AGENTS.md diff --git a/AGENTS.md b/AGENTS.md new file mode 100644 index 000000000..08fb0fa6b --- /dev/null +++ b/AGENTS.md @@ -0,0 +1,54 @@ +# Repository Guidelines + +## Project Structure & Module Organization +This repository is a Rust workspace (`Cargo.toml`) with these primary areas: + +- `kernel/`: core OS kernel crate. +- `awkernel_lib/`, `awkernel_async_lib/`, `awkernel_drivers/`: shared kernel/runtime infrastructure. +- `awkernel_aarch64/`, `x86bootdisk/`: architecture/platform support helpers. +- `userland/`: user-space library and app support. +- `applications/`: runnable samples/tests (`applications/tests/*`) and app crates. +- `smoltcp/`: network stack crate used by kernel/user code. +- `mdbook/`: documentation source; `docs/` stores generated docs output. +- `specification/`: design and implementation notes. +- `docker/`, `scripts/`, `targets/`, `misc/`: tooling, build config, boot artifacts, and platform files. + +## Build, Test, and Development Commands +- `make x86_64 [RELEASE=1]`: build x86_64 kernel image. +- `make aarch64 BSP= [RELEASE=1]`: build AArch64 targets. +- `make riscv32` / `make riscv64`: build RISC-V targets. +- `make qemu-x86_64`, `make qemu-aarch64-virt`, `make qemu-raspi3`: boot in QEMU. +- `make check`: run check across kernel targets and std crates. +- `make clippy`: run lints for major targets. +- `make test`: run `test_awkernel_lib`, `test_awkernel_async_lib`, `test_awkernel_drivers`, `test_smoltcp`, `test_rd_gen_to_dags`. +- `make docs`: build mdBook docs. +- `make fmt`: run `cargo fmt`. +- Direct aliases are in `.cargo/config.toml` (examples: `cargo +nightly-2026-06-13 test_awkernel_lib`, `cargo +nightly-2026-06-13 x86`, `cargo +nightly-2026-06-13 doc_x86`). + +## Coding Style & Naming Conventions +- Rust 2021 edition, default rustfmt formatting (`cargo fmt`). +- Use 4-space indentation and standard Rust naming: + - crates, modules, functions: `snake_case`. + - types/traits: `CamelCase`. + - test functions: `test_*`. +- Prefer small, explicit feature-gated modules; avoid broad default features. +- Keep architecture-specific code separated by crate and feature flags (`x86`, `aarch64`, `rv32`, `rv64`, `std`). + +## Testing Guidelines +- Unit tests are in `mod tests` blocks under crate source and can be run per-package through cargo aliases (e.g., `cargo +nightly-2026-06-13 test_awkernel_lib`). +- Integration-style workload tests are under `applications/tests/*`, typically invoked through the general `make test` suite. +- For behavior validation requiring emulation, reproduce with matching QEMU target command and board (`qemu-...` targets). +- Use `cargo +nightly-2026-06-13 clippy_x86` / `clippy_rv64` style aliases for target-specific linting. + +## Commit & Pull Request Guidelines +- Use Conventional Commit style observed in history: `type(scope): short summary` (examples: `feat(async): ...`, `fix(task): ...`, `test(task): ...`). +- Keep each commit focused to one logical change. +- PRs should include: + - target architecture and commands run (`make`, `cargo`, QEMU target), + - rationale for API/behavior changes, + - test commands and results. +- Link related issues when applicable and call out platform impact (`x86_64`, `aarch64`, `riscv32`, `riscv64`). + +## Security & Environment Notes +- Repository uses nightly toolchain; ensure `rustup toolchain install nightly-2026-06-13` and target support are in place before builds. +- x86 UEFI QEMU flows require `OVMF_PATH` to point at valid `code.fd` and `vars.fd` locations. diff --git a/applications/tests/test_task_kill/src/lib.rs b/applications/tests/test_task_kill/src/lib.rs index f1cb54daa..11ecb8e05 100644 --- a/applications/tests/test_task_kill/src/lib.rs +++ b/applications/tests/test_task_kill/src/lib.rs @@ -27,6 +27,7 @@ pub async fn run() { kill_idempotent().await; resources_freed_after_kill().await; kill_preempted_task().await; + kill_panicked_task().await; log::info!("TASK_KILL_TEST done"); } @@ -148,6 +149,34 @@ async fn kill_preempted_task() { } } +async fn kill_panicked_task() { + log::info!("TASK_KILL_TEST kill_panicked_task: step 1 start"); + + let id = task::spawn( + "panicked-target".into(), + async { + panic!("intentional panic for kill semantics test"); + }, + SchedulerType::PrioritizedFIFO(0), + ); + + // Let the task start and transition to Panicked after panic handling. + sleep(Duration::from_millis(100)).await; + + if task::get_task(id).is_none() { + log::info!("TASK_KILL_TEST kill_panicked_task: PASS (panicked task removed from registry)"); + } else { + log::error!("TASK_KILL_TEST kill_panicked_task: FAIL (panicked task still in registry)"); + } + + // Panicked tasks are terminal; kill() should return false and not mutate state. + if !task::kill(id) { + log::info!("TASK_KILL_TEST kill_panicked_task: PASS (kill returned false)"); + } else { + log::error!("TASK_KILL_TEST kill_panicked_task: FAIL (kill returned true)"); + } +} + async fn resources_freed_after_kill() { DROP_COUNT.store(0, Ordering::Release); diff --git a/awkernel_async_lib/src/task.rs b/awkernel_async_lib/src/task.rs index 23953a64f..7f52a9016 100644 --- a/awkernel_async_lib/src/task.rs +++ b/awkernel_async_lib/src/task.rs @@ -992,6 +992,14 @@ pub fn wake(task_id: u32) { /// `Waiting` state, wakers may still hold `Arc` references; the `Task` is freed /// only after those wakers are dropped — the caller is responsible for deregistering them. /// +/// `Preempted` tasks are not marked `Terminated` immediately because preemption bookkeeping +/// (`yield_preempted_and_wake_task`) unconditionally rewrites the state to `Preempted`. +/// In that case, `kill_pending` is used to defer termination until the task reaches the +/// next poll boundary. +/// +/// `Panicked` tasks are also considered terminal here. `kill()` returns `false` for +/// already-terminal tasks and does not alter `Panicked`/`Terminated` state. +/// /// Returns `true` if the task was found and killed, `false` if it was not found or was /// already in a terminal state. pub fn kill(task_id: u32) -> bool { From 80d5ba833569304da428ee9b14bb058756a38af1 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 13:38:10 +0900 Subject: [PATCH 10/22] Improve task kill resource cleanup and scheduling safety --- applications/tests/test_task_kill/src/lib.rs | 38 ++++++++++++++------ awkernel_async_lib/src/scheduler.rs | 36 +++++++++++++------ awkernel_async_lib/src/task.rs | 28 ++++++++++++--- 3 files changed, 77 insertions(+), 25 deletions(-) diff --git a/applications/tests/test_task_kill/src/lib.rs b/applications/tests/test_task_kill/src/lib.rs index 11ecb8e05..af81bf7b1 100644 --- a/applications/tests/test_task_kill/src/lib.rs +++ b/applications/tests/test_task_kill/src/lib.rs @@ -33,17 +33,20 @@ pub async fn run() { } async fn kill_sleeping_task() { + DROP_COUNT.store(0, Ordering::Release); + let id = task::spawn( "kill-target".into(), async { + let _tracker = DropTracker; loop { - sleep(Duration::from_secs(3600)).await; + sleep(Duration::from_millis(40)).await; } }, SchedulerType::PrioritizedFIFO(0), ); - sleep(Duration::from_millis(50)).await; + sleep(Duration::from_millis(20)).await; if task::kill(id) { log::info!("TASK_KILL_TEST kill_sleeping_task: PASS (kill returned true)"); @@ -51,13 +54,20 @@ async fn kill_sleeping_task() { log::error!("TASK_KILL_TEST kill_sleeping_task: FAIL (kill returned false)"); } - sleep(Duration::from_millis(50)).await; - if task::get_task(id).is_none() { log::info!("TASK_KILL_TEST task_removed_from_registry: PASS"); } else { log::error!("TASK_KILL_TEST task_removed_from_registry: FAIL (still in registry)"); } + + if wait_for_drop_count(1, 10).await { + log::info!("TASK_KILL_TEST kill_sleeping_task: PASS (resources freed)"); + } else { + log::error!( + "TASK_KILL_TEST kill_sleeping_task: FAIL (drop_count={})", + DROP_COUNT.load(Ordering::Acquire) + ); + } } fn kill_unknown_id() { @@ -182,8 +192,8 @@ async fn resources_freed_after_kill() { // The task owns a DropTracker and sleeps 200 ms per iteration. // sleep() stores the Waker in a timer closure, which holds the last Arc - // reference after kill() removes the task from TASKS. When the timer fires - // the closure drops the Waker → Arc → 0 → Future → DropTracker::drop(). + // reference after kill() removes the task from TASKS. The dropped Waker should + // drop the future and trigger the DropTracker. let id = task::spawn( "drop-tracker-task".into(), async { @@ -200,10 +210,7 @@ async fn resources_freed_after_kill() { task::kill(id); - // Wait for the timer to fire (~150 ms remaining) plus a safety margin. - sleep(Duration::from_millis(300)).await; - - if DROP_COUNT.load(Ordering::Acquire) == 1 { + if wait_for_drop_count(1, 8).await { log::info!("TASK_KILL_TEST resources_freed_after_kill: PASS"); } else { log::error!( @@ -212,3 +219,14 @@ async fn resources_freed_after_kill() { ); } } + +async fn wait_for_drop_count(expected: usize, retries: usize) -> bool { + for _ in 0..retries { + if DROP_COUNT.load(Ordering::Acquire) >= expected { + return true; + } + sleep(Duration::from_millis(20)).await; + } + + DROP_COUNT.load(Ordering::Acquire) >= expected +} diff --git a/awkernel_async_lib/src/scheduler.rs b/awkernel_async_lib/src/scheduler.rs index b9c98d726..3a9f39910 100644 --- a/awkernel_async_lib/src/scheduler.rs +++ b/awkernel_async_lib/src/scheduler.rs @@ -316,18 +316,32 @@ impl SleepingTasks { /// Wake tasks up. fn wake_task(&mut self) { - while let Some((dur, _)) = self.delta_list.front() { - let dur = Duration::from_nanos(dur); - let elapsed = self.base_time.elapsed(); - - if dur <= elapsed { - // Timed out. - if let DeltaList::Cons(data) = self.delta_list.pop().unwrap() { - let (_, handler, _) = data.into_inner(); - handler(); // Invoke a handler. - - self.base_time += dur; + loop { + let mut handler = None; + + { + let mut node = MCSNode::new(); + let mut guard = SLEEPING.lock(&mut node); + if let Some((dur, _)) = guard.delta_list.front() { + let dur = Duration::from_nanos(dur); + let elapsed = guard.base_time.elapsed(); + + if dur <= elapsed { + if let DeltaList::Cons(data) = guard.delta_list.pop().unwrap() { + let (_, h, _) = data.into_inner(); + guard.base_time += dur; + handler = Some(h); + } + } else { + break; + } + } else { + break; } + } + + if let Some(task) = handler { + task(); } else { break; } diff --git a/awkernel_async_lib/src/task.rs b/awkernel_async_lib/src/task.rs index 7f52a9016..de3599005 100644 --- a/awkernel_async_lib/src/task.rs +++ b/awkernel_async_lib/src/task.rs @@ -155,6 +155,21 @@ impl ArcWake for Task { awkernel_lib::cpu::wake_cpu(0); } } + +#[inline(always)] +fn drop_task_future(task: &Arc) { + let mut node = MCSNode::new(); + let Some(mut future) = task.future.try_lock(&mut node) else { + return; + }; + + if future.is_terminated() { + return; + } + + *future = futures::future::ready(Ok::<(), Cow<'static, str>>(())).boxed().fuse(); +} + /// Information of task. pub struct TaskInfo { @@ -844,6 +859,8 @@ pub fn run_main() { if matches!(info.state, State::Terminated | State::Panicked) { RUNNING[cpu_id].store(0, Ordering::Relaxed); + drop(info); + drop_task_future(&task); continue; } @@ -927,6 +944,9 @@ pub fn run_main() { task.clone().wake(); } } + } else { + drop(info); + drop_task_future(&task); } } Ok(Poll::Ready(result)) => { @@ -990,7 +1010,7 @@ pub fn wake(task_id: u32) { /// Sets the task state to `Terminated` and removes it from the global task registry. /// Any subsequent `wake()` call for this task will be a no-op. If the task was in /// `Waiting` state, wakers may still hold `Arc` references; the `Task` is freed -/// only after those wakers are dropped — the caller is responsible for deregistering them. +/// after those references are dropped. /// /// `Preempted` tasks are not marked `Terminated` immediately because preemption bookkeeping /// (`yield_preempted_and_wake_task`) unconditionally rewrites the state to `Preempted`. @@ -1003,9 +1023,8 @@ pub fn wake(task_id: u32) { /// Returns `true` if the task was found and killed, `false` if it was not found or was /// already in a terminal state. pub fn kill(task_id: u32) -> bool { - // Step 1: Clone the Arc out of TASKS, then drop TASKS before acquiring the per-task info lock. - // This keeps the TASKS critical section short and avoids lock-order inversions with code paths - // that may lock TASKS and then lock task.info (e.g., task::wake()). + // Step 1: Clone the Arc out of TASKS, then drop TASKS before touching task.info. + // This keeps the TASKS critical section short and avoids nested lock contention. let task = { let mut node = MCSNode::new(); let tasks = TASKS.lock(&mut node); @@ -1045,6 +1064,7 @@ pub fn kill(task_id: u32) -> bool { // Tasks::remove() is a BTreeMap::remove, so calling it on a missing key (e.g., if the // future completed naturally at the same time) is a no-op. // Skipped for State::Preempted (handled above via kill_pending). + drop_task_future(&task); { let mut node = MCSNode::new(); let mut tasks = TASKS.lock(&mut node); From f9ba4288e7ce13712ccac9cb356033b1233f456e Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 16:54:14 +0900 Subject: [PATCH 11/22] Handle deferred kill cleanup for preempted tasks --- awkernel_async_lib/src/task.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/awkernel_async_lib/src/task.rs b/awkernel_async_lib/src/task.rs index de3599005..78ee738ca 100644 --- a/awkernel_async_lib/src/task.rs +++ b/awkernel_async_lib/src/task.rs @@ -932,6 +932,7 @@ pub fn run_main() { // Now at an await boundary, complete the termination. info.state = State::Terminated; drop(info); + drop_task_future(&task); let mut node = MCSNode::new(); let mut tasks = TASKS.lock(&mut node); tasks.remove(task.id); @@ -1021,7 +1022,8 @@ pub fn wake(task_id: u32) { /// already-terminal tasks and does not alter `Panicked`/`Terminated` state. /// /// Returns `true` if the task was found and killed, `false` if it was not found or was -/// already in a terminal state. +/// already in a terminal state. If the task is currently polling, `kill()` marks termination +/// and returns `true` immediately; the task is cleaned up when that poll returns. pub fn kill(task_id: u32) -> bool { // Step 1: Clone the Arc out of TASKS, then drop TASKS before touching task.info. // This keeps the TASKS critical section short and avoids nested lock contention. From 62c108a5d6310eac915080940631d1552c8977e5 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 17:27:49 +0900 Subject: [PATCH 12/22] fix: detach service tasks in awkernel_services --- applications/awkernel_services/src/lib.rs | 15 ++++----- .../awkernel_services/src/network_service.rs | 31 ++++++++----------- 2 files changed, 19 insertions(+), 27 deletions(-) diff --git a/applications/awkernel_services/src/lib.rs b/applications/awkernel_services/src/lib.rs index 900163ffb..6ae1cf017 100644 --- a/applications/awkernel_services/src/lib.rs +++ b/applications/awkernel_services/src/lib.rs @@ -12,26 +12,23 @@ const BUFFERED_LOGGER_NAME: &str = "[Awkernel] buffered logger service"; const DISPLAY_SERVICE_NAME: &str = "[Awkernel] display service"; pub async fn run() { - awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( BUFFERED_LOGGER_NAME.into(), buffered_logger::run(), awkernel_async_lib::scheduler::SchedulerType::PrioritizedFIFO(0), - ) - .await; + ); - awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( NETWORK_SERVICE_NAME.into(), network_service::run(), awkernel_async_lib::scheduler::SchedulerType::PrioritizedFIFO(0), - ) - .await; + ); - awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( DISPLAY_SERVICE_NAME.into(), awkernel_display::run(), awkernel_async_lib::scheduler::SchedulerType::PrioritizedFIFO(0), - ) - .await; + ); awkernel_async_lib::sleep(Duration::from_secs(1)).await; awkernel_shell::init(); diff --git a/applications/awkernel_services/src/network_service.rs b/applications/awkernel_services/src/network_service.rs index 261b579ec..bbfe22e78 100644 --- a/applications/awkernel_services/src/network_service.rs +++ b/applications/awkernel_services/src/network_service.rs @@ -16,19 +16,17 @@ type ChanProtoInterruptHandlerDual = Chan<(), pub async fn run() { log::info!("Starting {}.", crate::NETWORK_SERVICE_NAME); - awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( GARBAGE_COLLECTOR_NAME.into(), tcp_garbage_collector(), SchedulerType::PrioritizedFIFO(0), - ) - .await; + ); - awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( NETWORK_IF_POLLER_NAME.into(), network_interface_poller(), SchedulerType::PrioritizedFIFO(0), - ) - .await; + ); let mut ch_irq_handlers = BTreeMap::new(); let mut ch_poll_handlers = BTreeMap::new(); @@ -137,12 +135,11 @@ async fn spawn_handlers( if_status.device_name, ); - awkernel_async_lib::spawn( - name.into(), + let _ = awkernel_async_lib::spawn( + name.into(), interrupt_handler(if_status.interface_id, irq, server), SchedulerType::PrioritizedFIFO(0), - ) - .await; + ); } if if_status.poll_mode { @@ -155,12 +152,11 @@ async fn spawn_handlers( if_status.device_name, ); - awkernel_async_lib::spawn( - name.into(), + let _ = awkernel_async_lib::spawn( + name.into(), poll_handler(if_status.interface_id, server), SchedulerType::PrioritizedFIFO(0), - ) - .await; + ); } if let Some(tick_msec) = if_status.tick_msec { @@ -173,12 +169,11 @@ async fn spawn_handlers( if_status.device_name, ); - awkernel_async_lib::spawn( - name.into(), + let _ = awkernel_async_lib::spawn( + name.into(), tick_handler(if_status.interface_id, tick_msec, server), SchedulerType::PrioritizedFIFO(0), - ) - .await; + ); } } From d8d363c4add643bf611d745df5db2b1600bfdd47 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 18:50:30 +0900 Subject: [PATCH 13/22] Fix task kill races --- applications/tests/test_task_kill/src/lib.rs | 5 +- awkernel_async_lib/src/scheduler.rs | 40 ++--- .../src/scheduler/prioritized_fifo.rs | 7 +- awkernel_async_lib/src/task.rs | 7 +- .../task/preemptive_spin/data_structure.pml | 3 +- .../task/preemptive_spin/for_verification.pml | 22 ++- .../src/task/preemptive_spin/future_mock.pml | 12 +- .../src/task/preemptive_spin/ltl.pml | 16 ++ .../src/task/preemptive_spin/preemptive.pml | 168 +++++++++++++++--- 9 files changed, 209 insertions(+), 71 deletions(-) diff --git a/applications/tests/test_task_kill/src/lib.rs b/applications/tests/test_task_kill/src/lib.rs index af81bf7b1..889b41a97 100644 --- a/applications/tests/test_task_kill/src/lib.rs +++ b/applications/tests/test_task_kill/src/lib.rs @@ -121,7 +121,10 @@ async fn kill_preempted_task() { SchedulerType::PrioritizedRR(0), ); - log::info!("TASK_KILL_TEST kill_preempted_task: step 2 spawned id={}", id); + log::info!( + "TASK_KILL_TEST kill_preempted_task: step 2 spawned id={}", + id + ); // Allow the task to run and be preempted at least once. sleep(Duration::from_millis(50)).await; diff --git a/awkernel_async_lib/src/scheduler.rs b/awkernel_async_lib/src/scheduler.rs index 3a9f39910..de4b75625 100644 --- a/awkernel_async_lib/src/scheduler.rs +++ b/awkernel_async_lib/src/scheduler.rs @@ -317,34 +317,26 @@ impl SleepingTasks { /// Wake tasks up. fn wake_task(&mut self) { loop { - let mut handler = None; - - { - let mut node = MCSNode::new(); - let mut guard = SLEEPING.lock(&mut node); - if let Some((dur, _)) = guard.delta_list.front() { - let dur = Duration::from_nanos(dur); - let elapsed = guard.base_time.elapsed(); - - if dur <= elapsed { - if let DeltaList::Cons(data) = guard.delta_list.pop().unwrap() { - let (_, h, _) = data.into_inner(); - guard.base_time += dur; - handler = Some(h); - } - } else { - break; - } - } else { - break; - } + let Some((dur, _)) = self.delta_list.front() else { + break; + }; + + let dur = Duration::from_nanos(dur); + let elapsed = self.base_time.elapsed(); + + if dur > elapsed { + break; } - if let Some(task) = handler { - task(); + let handler = if let DeltaList::Cons(data) = self.delta_list.pop().unwrap() { + let (_, handler, _) = data.into_inner(); + self.base_time += dur; + handler } else { break; - } + }; + + handler(); } } diff --git a/awkernel_async_lib/src/scheduler/prioritized_fifo.rs b/awkernel_async_lib/src/scheduler/prioritized_fifo.rs index da125cf3b..dfc329d4b 100644 --- a/awkernel_async_lib/src/scheduler/prioritized_fifo.rs +++ b/awkernel_async_lib/src/scheduler/prioritized_fifo.rs @@ -125,10 +125,11 @@ impl PrioritizedFIFOScheduler { (max(t, highest_pending), rt.cpu_id) }) }) - .min() - .unwrap(); + .min(); - let (target_task, target_cpu) = preemption_target; + let Some((target_task, target_cpu)) = preemption_target else { + return false; + }; if task > target_task { push_preemption_pending(target_cpu, task); let preempt_irq = awkernel_lib::interrupt::get_preempt_irq(); diff --git a/awkernel_async_lib/src/task.rs b/awkernel_async_lib/src/task.rs index 78ee738ca..78aa68205 100644 --- a/awkernel_async_lib/src/task.rs +++ b/awkernel_async_lib/src/task.rs @@ -155,7 +155,7 @@ impl ArcWake for Task { awkernel_lib::cpu::wake_cpu(0); } } - + #[inline(always)] fn drop_task_future(task: &Arc) { let mut node = MCSNode::new(); @@ -167,10 +167,11 @@ fn drop_task_future(task: &Arc) { return; } - *future = futures::future::ready(Ok::<(), Cow<'static, str>>(())).boxed().fuse(); + *future = futures::future::ready(Ok::<(), Cow<'static, str>>(())) + .boxed() + .fuse(); } - /// Information of task. pub struct TaskInfo { pub(crate) state: State, diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml index ab7869074..3c9dad755 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml @@ -7,7 +7,7 @@ typedef Worker { Worker workers[WORKER_NUM] -mtype = { Initialized,Runnable,Running,Waiting,Terminated,Pending,Preempted }// Panic is not considered. +mtype = { Initialized,Runnable,Running,Waiting,Terminated,Pending,Preempted,Panicked,Ready } /* awkernel_async_lib::task::TaskInfo */ typedef TaskInfo { @@ -16,6 +16,7 @@ typedef TaskInfo { bool need_sched = false; byte id;// This also represents the priority of the task. The lower the value,the higher the priority. bool need_preemption = false; + bool kill_pending = false; short thread = - 1;// tid when this task is preempted, -1 otherwise. } diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/for_verification.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/for_verification.pml index dce3d2be4..535e02134 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/for_verification.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/for_verification.pml @@ -1,6 +1,9 @@ byte num_terminated = 0 byte waking[TASK_NUM] = 0 +bool killed[TASK_NUM] = false +bool kill_requested[TASK_NUM] = false +byte num_kill_requests = 0 bool handling_interrupt[IR_HANDLER_NUM] = false byte runnable_preempted_highest_priority = BYTE_MAX @@ -12,7 +15,7 @@ inline update_runnable_preempted_highest_priority() { byte j; for (j: 0 .. TASK_NUM - 1) { if - :: ((tasks[j].state == Runnable || tasks[j].state == Preempted) && tasks[j].id < runnable_preempted_highest_priority) -> + :: ((tasks[j].state == Runnable || tasks[j].state == Preempted) && tasks[j].id < runnable_preempted_highest_priority) -> runnable_preempted_highest_priority = tasks[j].id :: else fi @@ -26,7 +29,7 @@ inline update_running_lowest_priority() { byte j; for (j: 0 .. TASK_NUM - 1) { if - :: (tasks[j].state == Running && tasks[j].id > running_lowest_priority) -> + :: (tasks[j].state == Running && tasks[j].id > running_lowest_priority) -> running_lowest_priority = tasks[j].id :: else fi @@ -42,19 +45,20 @@ chan resume_requests = [WORKER_NUM] of { byte }// tid that requested to resume e active proctype timeout_handler() { xr resume_requests; byte tid; - + do - :: timeout -> + :: timeout -> if :: num_terminated == TASK_NUM -> break - :: atomic{else -> - assert(nempty(resume_requests)); + :: else -> + if + :: len(resume_requests) > 0 -> resume_requests?tid; - assert(wait_for_weak_fairness[tid]); wait_for_weak_fairness[tid] = false; - assert(consecutive_run_main_loop[tid] == MAX_CONSECUTIVE_RUN_MAIN_LOOP); consecutive_run_main_loop[tid] = 0; - } + :: else -> + skip + fi fi od } diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml index 5be31c5b8..f6a548079 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml @@ -9,24 +9,24 @@ inline future(tid,task,ret) { :: wake(tid,1); wake(tid,0); :: wake(tid,0); wake(tid,1); fi - future_blocked[2]; - ret = Ready + future_blocked[2] = true; + ret = Ready; :: task == 3 -> // 1st Low priority task wake(tid,2); - future_blocked[3]; - ret = Ready + future_blocked[3] = true; + ret = Ready; :: task == 0 -> // 1st High priority task if :: future_blocked[2] = true; future_blocked[3] = true; :: future_blocked[3] = true; future_blocked[2] = true; fi - ret = Ready + ret = Ready; :: task == 1 -> // 2nd High priority task if :: future_blocked[2] = true; future_blocked[3] = true; :: future_blocked[3] = true; future_blocked[2] = true; fi - ret = Ready + ret = Ready; :: else -> assert(false); fi } diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/ltl.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/ltl.pml index 92474bdb5..ea3524b16 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/ltl.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/ltl.pml @@ -17,3 +17,19 @@ ltl ensure_priority { !handling_interrupt[0] && !handling_interrupt[1] && !handling_interrupt[2] && !handling_interrupt[3]) -> (running_lowest_priority < runnable_preempted_highest_priority)) } + +ltl killed_task_eventually_terminated_and_not_running { + []( + (!killed[0] || (<>(tasks[0].state == Terminated && RUNNING[0] != 0 && RUNNING[1] != 0)) ) && + (!killed[1] || (<>(tasks[1].state == Terminated && RUNNING[0] != 1 && RUNNING[1] != 1)) ) && + (!killed[2] || (<>(tasks[2].state == Terminated && RUNNING[0] != 2 && RUNNING[1] != 2)) ) && + (!killed[3] || (<>(tasks[3].state == Terminated && RUNNING[0] != 3 && RUNNING[1] != 3)) ) + ) +} + +ltl kill_pending_eventually_terminated { + []((!tasks[0].kill_pending || <> (tasks[0].state == Terminated)) && + (!tasks[1].kill_pending || <> (tasks[1].state == Terminated)) && + (!tasks[2].kill_pending || <> (tasks[2].state == Terminated)) && + (!tasks[3].kill_pending || <> (tasks[3].state == Terminated))) +} diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml index 26a055ca4..544f17c8f 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml @@ -117,9 +117,9 @@ inline wake(tid,task) { waking[task]--; } unlock(tid,lock_info[task]) - :: tasks[task].state == Terminated -> + :: tasks[task].state == Terminated || tasks[task].state == Panicked -> d_step{ - printf("wake() already terminated: tid = %d,task = %d,state = %e\n",tid,task,tasks[task].state); + printf("wake() already terminal: tid = %d,task = %d,state = %e\n",tid,task,tasks[task].state); assert(waking[task] > 0); waking[task]--; } @@ -136,6 +136,52 @@ inline wake(tid,task) { fi } +inline kill_task(tid,task) { + bool was_killed; + was_killed = false; + + lock(tid,lock_info[task]); + if + :: tasks[task].state == Running || tasks[task].state == Runnable || tasks[task].state == Waiting || tasks[task].state == Initialized -> + d_step{ + printf("kill_task(): direct terminate, tid = %d,task = %d,state = %e\n",tid,task,tasks[task].state); + tasks[task].state = Terminated; + kill_requested[task] = true; + if + :: !killed[task] -> + killed[task] = true; + num_kill_requests++; + num_terminated++; + :: else + fi + was_killed = true; + } + unlock(tid,lock_info[task]) + :: tasks[task].state == Preempted -> + d_step{ + printf("kill_task(): deferred terminate for preempted, tid = %d,task = %d\n",tid,task); + tasks[task].kill_pending = true; + kill_requested[task] = true; + if + :: !killed[task] -> + killed[task] = true; + num_kill_requests++; + :: else + fi + was_killed = true; + } + unlock(tid,lock_info[task]) + :: tasks[task].state == Terminated || tasks[task].state == Panicked -> + d_step{ + printf("kill_task(): already terminal, tid = %d,task = %d,state = %e\n",tid,task,tasks[task].state); + was_killed = false; + } + unlock(tid,lock_info[task]) + :: else -> + assert(false) + fi +} + /* awkernel_async_lib::scheduler::fifo::PrioritizedFIFOScheduler::get_next()*/ inline get_next_each_scheduler(tid,ret,sched_type) { lock(tid,lock_queue[sched_type]); @@ -149,7 +195,7 @@ inline get_next_each_scheduler(tid,ret,sched_type) { lock(tid,lock_info[head]); if - :: tasks[head].state == Terminated -> + :: tasks[head].state == Terminated || tasks[head].state == Panicked -> unlock(tid,lock_info[head]); goto start_get_next :: tasks[head].state == Preempted -> @@ -300,7 +346,7 @@ inline take_preempt_context(task,ret) { * In this model,Worker and InterruptHandler has one-to-one relationship, so tid equals the interrupt handler's id. */ proctype interrupt_handler(byte tid) provided (workers[tid].executing_in != - 1) { - byte cpu_id_;short cur_task;short hp_task;short next_thread;byte pending_lp_task; + byte cpu_id_;short cur_task;short hp_task;short next_thread;byte pending_lp_task;bool found_hp_task; chan moved_preemption_pending = [TASK_NUM] of { byte }; do @@ -314,6 +360,14 @@ proctype interrupt_handler(byte tid) provided (workers[tid].executing_in != - 1) } cur_task = RUNNING[cpu_id_]; + + if + :: tasks[hp_task].state == Terminated || tasks[hp_task].state == Panicked -> + printf("preemption(): skip terminal pending task = %d,state = %e\n",hp_task,tasks[hp_task].state); + remove_from_channel(ipi_requests[cpu_id_],hp_task); + goto finish + :: else + fi if :: d_step{cur_task == - 1 -> @@ -342,6 +396,21 @@ proctype interrupt_handler(byte tid) provided (workers[tid].executing_in != - 1) // If there is a task to be invoked next, execute the task. move_channel(ipi_requests[cpu_id_],moved_preemption_pending); moved_preemption_pending?hp_task;// hp_task may be updated, so the latest hp_task is used. + found_hp_task = true; + do + :: tasks[hp_task].state == Terminated || tasks[hp_task].state == Panicked -> + if + :: moved_preemption_pending?[hp_task] -> moved_preemption_pending?hp_task + :: else -> + found_hp_task = false; + break + fi + :: else -> break + od + if + :: !found_hp_task -> goto finish + :: else + fi d_step { printf("RUNNING[%d] = %d\n",cpu_id_,hp_task); RUNNING[cpu_id_] = hp_task; @@ -350,29 +419,50 @@ proctype interrupt_handler(byte tid) provided (workers[tid].executing_in != - 1) // Re-wake the remaining all preemption-pending tasks with lower priorities than `next`. do :: d_step{moved_preemption_pending?[pending_lp_task] -> - moved_preemption_pending?pending_lp_task; - waking[pending_lp_task]++;} - wake_task(tid,pending_lp_task) + moved_preemption_pending?pending_lp_task;} + if + :: tasks[pending_lp_task].state == Terminated || tasks[pending_lp_task].state == Panicked -> skip + :: else -> + waking[pending_lp_task]++; + wake_task(tid,pending_lp_task) + fi :: else -> break od printf("Preemption Occurs: cpu_id = %d,cur_task = %d,hp_task = %d\n",cpu_id_,cur_task,hp_task); lock(tid,lock_info[hp_task]); if - :: d_step { tasks[hp_task].thread != - 1 -> take_preempt_context(hp_task,next_thread); } + :: tasks[hp_task].state == Terminated || tasks[hp_task].state == Panicked -> + unlock(tid,lock_info[hp_task]); + goto finish + :: tasks[hp_task].thread != - 1 -> + take_preempt_context(hp_task,next_thread); unlock(tid,lock_info[hp_task]); yield_preempted_and_wake_task(cur_task,tid,next_thread) :: else -> // Otherwise,get a thread from the thread pool or create a new thread. unlock(tid,lock_info[hp_task]); take_pooled_thread(next_thread); - d_step { - assert(NEXT_TASK[cpu_id_] == - 1); - NEXT_TASK[cpu_id_] = hp_task; - } - yield_preempted_and_wake_task(cur_task,tid,next_thread) + lock(tid,lock_info[hp_task]); + if + :: tasks[hp_task].state == Terminated || tasks[hp_task].state == Panicked -> + d_step { + RUNNING[cpu_id_] = cur_task; + workers[next_thread].pooled = true; + } + unlock(tid,lock_info[hp_task]); + goto finish + :: else -> + d_step { + assert(NEXT_TASK[cpu_id_] == - 1); + NEXT_TASK[cpu_id_] = hp_task; + } + unlock(tid,lock_info[hp_task]); + yield_preempted_and_wake_task(cur_task,tid,next_thread) + fi fi finish: + skip; atomic { interrupt_enabled[cpu_id(tid)] = true;// iretq workers[tid].interrupted = false @@ -467,25 +557,43 @@ proctype run_main(byte tid) provided (workers[tid].executing_in != - 1 && !worke if :: d_step{poll_result == Pending -> printf("result_future Pending: tid = %d,task = %d\n",tid,task);} - d_step { - tasks[task].state = Waiting; - update_running_lowest_priority(); - } - if - :: tasks[task].need_sched -> - tasks[task].need_sched = false; + :: tasks[task].state == Terminated || tasks[task].state == Panicked -> unlock(tid,lock_info[task]); - wake(tid,task); goto start - :: else + :: tasks[task].kill_pending -> + d_step { + printf("result_future Pending with kill_pending: tid = %d,task = %d\n",tid,task); + tasks[task].state = Terminated; + tasks[task].kill_pending = false; + update_running_lowest_priority(); + num_terminated++; + } + unlock(tid,lock_info[task]); + goto start + :: else -> + d_step { + printf("result_future Pending: tid = %d,task = %d\n",tid,task); + tasks[task].state = Waiting; + update_running_lowest_priority(); + } + + if + :: tasks[task].need_sched -> + tasks[task].need_sched = false; + unlock(tid,lock_info[task]); + wake(tid,task); + goto start + :: else + fi fi :: d_step{poll_result == Ready -> printf("result_future Ready: tid = %d,task = %d\n",tid,task);} if - :: tasks[task].state != Terminated -> + :: tasks[task].state == Terminated || tasks[task].state == Panicked -> + skip + :: else -> num_terminated++ - :: else -> assert(false) fi d_step { @@ -503,8 +611,20 @@ proctype run_main(byte tid) provided (workers[tid].executing_in != - 1 && !worke } +proctype killer(byte tid) { + byte target; + if + :: target = 0 + :: target = 1 + :: target = 2 + :: target = 3 + fi + kill_task(tid,target); +} + init { byte i; + run killer(0); for (i: 0 .. TASK_NUM - 1) { tasks[i].id = i; From ed4722abdd3137f6c9115eb5072799f8952076f8 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 19:16:42 +0900 Subject: [PATCH 14/22] Add SPIN kill test variant --- .../src/task/preemptive_spin/Makefile | 11 ++++++- .../src/task/preemptive_spin/README.md | 28 ++++++++++++++++ .../task/preemptive_spin/data_structure.pml | 2 ++ .../task/preemptive_spin/for_verification.pml | 2 ++ .../src/task/preemptive_spin/future_mock.pml | 19 +++++++++++ .../src/task/preemptive_spin/ltl.pml | 26 ++++++--------- .../src/task/preemptive_spin/preemptive.pml | 33 ++++++++++++++----- 7 files changed, 96 insertions(+), 25 deletions(-) diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/Makefile b/specification/awkernel_async_lib/src/task/preemptive_spin/Makefile index 2a77926f6..f0dcf6c1f 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/Makefile +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/Makefile @@ -8,9 +8,18 @@ run: pan rm -f *.trail ./pan -a -n -m30000 +kill-test: + rm -f pan pan.* *.trail *.tmp _spin_nvr.tmp kill-test-*.log + spin -a -DKILL_TEST preemptive.pml + gcc -O3 -DCOLLAPSE -DVECTORSZ=5000 -DNFAIR=3 -o pan pan.c + ./pan -a -n -m30000 -N killed_task_eventually_terminated_and_not_running | tee kill-test-killed.log + grep -q "errors: 0" kill-test-killed.log + ./pan -a -n -m30000 -N kill_pending_eventually_terminated | tee kill-test-pending.log + grep -q "errors: 0" kill-test-pending.log + trail: clear spin -t preemptive.pml clean: - rm -f pan.* *.trail pan *.tmp + rm -f pan.* *.trail pan *.tmp _spin_nvr.tmp kill-test-*.log diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/README.md b/specification/awkernel_async_lib/src/task/preemptive_spin/README.md index 974e4ea94..aac5a7b5c 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/README.md +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/README.md @@ -171,6 +171,34 @@ pan: elapsed time 1.26e+03 seconds pan: rate 215529.76 states/second ``` +## Kill test + +The kill-specific verification is separated from the normal priority LTL tests by the `KILL_TEST` build flag. +This keeps `make run` free from the killer process and kill-only state such as `kill_pending`, while `make kill-test` enables a smaller model for kill behavior. + +In the kill-test variant, the model uses `TASK_NUM=2`, `CPU_NUM=1`, `WORKER_NUM=2`, and `IR_HANDLER_NUM=1`. +Task 1 is the low-priority kill target, and task 0 is the high-priority task that preempts it. +The `killer` process waits until task 1 becomes `Preempted`, then calls `kill_task(1)`. + +Verified properties: + +1. A killed task eventually becomes `Terminated` and is not running (`ltl killed_task_eventually_terminated_and_not_running`). +2. A task with `kill_pending` eventually becomes `Terminated` (`ltl kill_pending_eventually_terminated`). + +Result: + +``` +$ make kill-test +... +State-vector 400 byte, depth reached 888, errors: 0 + 7825 states, stored (9442 visited) +... +State-vector 400 byte, depth reached 888, errors: 0 + 7590 states, stored (8972 visited) +``` + +No invalid array index was reported. + ## Inter-scheduler priority inversion As the above verification does not cover inter-scheduler priority inversion, we need to verify it separately. The model now supports multiple scheduler types through [this](https://github.com/tier4/awkernel/commit/4724e908cebeba5ab89ab21d310a309a6d892a00) changes: diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml index 3c9dad755..d31557bf0 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml @@ -16,7 +16,9 @@ typedef TaskInfo { bool need_sched = false; byte id;// This also represents the priority of the task. The lower the value,the higher the priority. bool need_preemption = false; +#ifdef KILL_TEST bool kill_pending = false; +#endif short thread = - 1;// tid when this task is preempted, -1 otherwise. } diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/for_verification.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/for_verification.pml index 535e02134..361852082 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/for_verification.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/for_verification.pml @@ -1,9 +1,11 @@ byte num_terminated = 0 byte waking[TASK_NUM] = 0 +#ifdef KILL_TEST bool killed[TASK_NUM] = false bool kill_requested[TASK_NUM] = false byte num_kill_requests = 0 +#endif bool handling_interrupt[IR_HANDLER_NUM] = false byte runnable_preempted_highest_priority = BYTE_MAX diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml index f6a548079..478dbb904 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml @@ -1,5 +1,23 @@ bool future_blocked[TASK_NUM] = false +#ifdef KILL_TEST +// Kill-test variant: task 1 is the low-priority target, task 0 preempts it. +inline future(tid,task,ret) { + printf("future(): tid = %d, task = %d\n", tid, task); + if + :: task == 1 -> + wake(tid,0); + future_blocked[1] = true; + ret = Pending; + :: task == 0 -> + future_blocked[0] = true; + ret = Ready; + :: else -> assert(false); + fi +} + +#define INIT_TASK 1 +#else // This assumes that there are 4 tasks, with task IDs 0, 1, 2, and 3. inline future(tid,task,ret) { printf("future(): tid = %d, task = %d\n", tid, task); @@ -32,3 +50,4 @@ inline future(tid,task,ret) { } #define INIT_TASK 3 +#endif diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/ltl.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/ltl.pml index ea3524b16..be46a2ae9 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/ltl.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/ltl.pml @@ -1,3 +1,12 @@ +#ifdef KILL_TEST +ltl killed_task_eventually_terminated_and_not_running { + [](!killed[1] || <> (tasks[1].state == Terminated && RUNNING[0] != 1)) +} + +ltl kill_pending_eventually_terminated { + [](!tasks[1].kill_pending || <> (tasks[1].state == Terminated)) +} +#else ltl eventually_terminate { <> (num_terminated == TASK_NUM) } @@ -17,19 +26,4 @@ ltl ensure_priority { !handling_interrupt[0] && !handling_interrupt[1] && !handling_interrupt[2] && !handling_interrupt[3]) -> (running_lowest_priority < runnable_preempted_highest_priority)) } - -ltl killed_task_eventually_terminated_and_not_running { - []( - (!killed[0] || (<>(tasks[0].state == Terminated && RUNNING[0] != 0 && RUNNING[1] != 0)) ) && - (!killed[1] || (<>(tasks[1].state == Terminated && RUNNING[0] != 1 && RUNNING[1] != 1)) ) && - (!killed[2] || (<>(tasks[2].state == Terminated && RUNNING[0] != 2 && RUNNING[1] != 2)) ) && - (!killed[3] || (<>(tasks[3].state == Terminated && RUNNING[0] != 3 && RUNNING[1] != 3)) ) - ) -} - -ltl kill_pending_eventually_terminated { - []((!tasks[0].kill_pending || <> (tasks[0].state == Terminated)) && - (!tasks[1].kill_pending || <> (tasks[1].state == Terminated)) && - (!tasks[2].kill_pending || <> (tasks[2].state == Terminated)) && - (!tasks[3].kill_pending || <> (tasks[3].state == Terminated))) -} +#endif diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml index 544f17c8f..a8b43da93 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml @@ -1,7 +1,14 @@ +#ifdef KILL_TEST +#define TASK_NUM 2 +#define WORKER_NUM 2// One running worker and one preemption context worker. +#define IR_HANDLER_NUM 1// One interrupt handler is enough with CPU_NUM == 1. +#define CPU_NUM 1 +#else #define TASK_NUM 4 #define WORKER_NUM TASK_NUM// Prepare same number of worker threads as tasks. #define IR_HANDLER_NUM TASK_NUM// Prepare same number of interrupt handlers as tasks. #define CPU_NUM 2 +#endif #define SCHEDULER_TYPE_NUM 2 #include "data_structure.pml" @@ -136,6 +143,7 @@ inline wake(tid,task) { fi } +#ifdef KILL_TEST inline kill_task(tid,task) { bool was_killed; was_killed = false; @@ -182,6 +190,8 @@ inline kill_task(tid,task) { fi } +#endif + /* awkernel_async_lib::scheduler::fifo::PrioritizedFIFOScheduler::get_next()*/ inline get_next_each_scheduler(tid,ret,sched_type) { lock(tid,lock_queue[sched_type]); @@ -561,6 +571,7 @@ proctype run_main(byte tid) provided (workers[tid].executing_in != - 1 && !worke :: tasks[task].state == Terminated || tasks[task].state == Panicked -> unlock(tid,lock_info[task]); goto start +#ifdef KILL_TEST :: tasks[task].kill_pending -> d_step { printf("result_future Pending with kill_pending: tid = %d,task = %d\n",tid,task); @@ -571,6 +582,7 @@ proctype run_main(byte tid) provided (workers[tid].executing_in != - 1 && !worke } unlock(tid,lock_info[task]); goto start +#endif :: else -> d_step { printf("result_future Pending: tid = %d,task = %d\n",tid,task); @@ -611,25 +623,29 @@ proctype run_main(byte tid) provided (workers[tid].executing_in != - 1 && !worke } +#ifdef KILL_TEST proctype killer(byte tid) { - byte target; - if - :: target = 0 - :: target = 1 - :: target = 2 - :: target = 3 - fi - kill_task(tid,target); + do + :: tasks[1].state == Preempted -> break + :: else -> skip + od; + kill_task(tid,1); } +#endif init { byte i; +#ifdef KILL_TEST run killer(0); +#endif for (i: 0 .. TASK_NUM - 1) { tasks[i].id = i; } tasks[0].scheduler_type = 0; +#ifdef KILL_TEST + tasks[1].scheduler_type = 0; +#else #if SCHED_TYPE_PATTERN==0 tasks[1].scheduler_type = 0;tasks[2].scheduler_type = 0;tasks[3].scheduler_type = 0; #elif SCHED_TYPE_PATTERN==1 @@ -638,6 +654,7 @@ init { tasks[1].scheduler_type = 0;tasks[2].scheduler_type = 1;tasks[3].scheduler_type = 1; #elif SCHED_TYPE_PATTERN==3 tasks[1].scheduler_type = 1;tasks[2].scheduler_type = 1;tasks[3].scheduler_type = 1; +#endif #endif wake(0,INIT_TASK); From dc7dc664f8f3d1491a6de00ed141705a73854088 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 19:22:38 +0900 Subject: [PATCH 15/22] Add async scheduler testing skill --- .../awkernel-async-scheduler-testing/SKILL.md | 81 +++++++++++++++++++ .../skills/awkernel-async-scheduler-testing | 1 + .../skills/awkernel-async-scheduler-testing | 1 + 3 files changed, 83 insertions(+) create mode 100644 .agents/skills/awkernel-async-scheduler-testing/SKILL.md create mode 120000 .claude/skills/awkernel-async-scheduler-testing create mode 120000 .codex/skills/awkernel-async-scheduler-testing diff --git a/.agents/skills/awkernel-async-scheduler-testing/SKILL.md b/.agents/skills/awkernel-async-scheduler-testing/SKILL.md new file mode 100644 index 000000000..a0ed684e9 --- /dev/null +++ b/.agents/skills/awkernel-async-scheduler-testing/SKILL.md @@ -0,0 +1,81 @@ +--- +name: awkernel-async-scheduler-testing +description: Use when testing or debugging Awkernel async/await task scheduler behavior, including task kill, preemption, sleep/wake, timer interactions, QEMU reproduction, and SPIN model checking under specification/awkernel_async_lib/src/task/preemptive_spin. +--- + +# Awkernel Async Scheduler Testing + +Use this skill when changing or reviewing `awkernel_async_lib` task scheduling behavior: `kill()`, preemption, sleep/wake, timer wakeups, task registry removal, or scheduler queues. + +## Core workflow + +1. Identify whether the issue is in runtime code, model code, or a test app. +2. Prefer `make` for kernel builds; do not replace kernel validation with direct `cargo` commands. +3. Reproduce on the smallest layer first, then escalate: + - Rust/library check for compile-level regressions. + - SPIN for scheduler state-machine properties. + - RELEASE QEMU for real kernel behavior and shell responsiveness. +4. Treat shell stuck as a scheduler/timer symptom, not necessarily a shell bug. + +## Build and QEMU commands + +Use RELEASE builds for QEMU experiments: + +```sh +make x86_64 RELEASE=1 +make qemu-x86_64_nographic RELEASE=1 +``` + +For kill-specific QEMU testing: + +```sh +make x86_64 RELEASE=1 OPT='--release --features test_task_kill' +make qemu-x86_64_nographic RELEASE=1 +``` + +After feature tests complete, verify the shell still responds with a small expression such as `(+ 7 8)`. Intentional panic logs from panic-specific tests are not automatically failures; check the PASS/FAIL lines after the panic. + +## SPIN model checking + +The preemptive scheduler model lives in: + +```text +specification/awkernel_async_lib/src/task/preemptive_spin +``` + +Use the normal LTL tests for non-kill scheduler behavior: + +```sh +make -C specification/awkernel_async_lib/src/task/preemptive_spin clean run +``` + +Use the kill-specific reduced model for kill behavior: + +```sh +make -C specification/awkernel_async_lib/src/task/preemptive_spin clean kill-test +``` + +`kill-test` enables `KILL_TEST`, uses a smaller task set, and should keep killer/kill-only state out of normal `make run`. Do not run `clean run` and `clean kill-test` concurrently in the same directory; both targets delete and regenerate `pan.*` files. + +## Scheduler failure patterns to check + +- Stale task IDs: a running snapshot may reference a task removed from the registry by `kill()`. +- Terminal tasks: `Terminated` and `Panicked` tasks must not be requeued or selected for preemption. +- Deferred kill: `Preempted` tasks should set `kill_pending` and terminate at a safe await/resume point. +- Lock nesting: watch for self-deadlock around sleep/timer wake paths and global scheduler locks. +- Pending preemption: queues may contain tasks that become terminal before the interrupt handler consumes them. + +## Generated files and commits + +Do not commit SPIN or QEMU generated artifacts unless explicitly requested: + +```text +pan +pan.* +*.trail +*_spin_nvr.tmp +kill-test-*.log +qemu-*.log +``` + +When committing scheduler work, include only source/model/test files relevant to the change. Leave unrelated dirty files untouched. diff --git a/.claude/skills/awkernel-async-scheduler-testing b/.claude/skills/awkernel-async-scheduler-testing new file mode 120000 index 000000000..710b2a443 --- /dev/null +++ b/.claude/skills/awkernel-async-scheduler-testing @@ -0,0 +1 @@ +../../.agents/skills/awkernel-async-scheduler-testing \ No newline at end of file diff --git a/.codex/skills/awkernel-async-scheduler-testing b/.codex/skills/awkernel-async-scheduler-testing new file mode 120000 index 000000000..710b2a443 --- /dev/null +++ b/.codex/skills/awkernel-async-scheduler-testing @@ -0,0 +1 @@ +../../.agents/skills/awkernel-async-scheduler-testing \ No newline at end of file From 0699b6997036bae6bd2c874bbd53b6da948b1707 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 19:26:10 +0900 Subject: [PATCH 16/22] add CLAUDE.md Signed-off-by: Yuuki Takano --- CLAUDE.md | 3 +++ .../awkernel_services/src/network_service.rs | 12 ++++++------ 2 files changed, 9 insertions(+), 6 deletions(-) create mode 100644 CLAUDE.md diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 000000000..f6aa6c026 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,3 @@ +# CLAUDE.md + +@AGENTS.md diff --git a/applications/awkernel_services/src/network_service.rs b/applications/awkernel_services/src/network_service.rs index bbfe22e78..0d77dbd75 100644 --- a/applications/awkernel_services/src/network_service.rs +++ b/applications/awkernel_services/src/network_service.rs @@ -136,10 +136,10 @@ async fn spawn_handlers( ); let _ = awkernel_async_lib::spawn( - name.into(), + name.into(), interrupt_handler(if_status.interface_id, irq, server), SchedulerType::PrioritizedFIFO(0), - ); + ); } if if_status.poll_mode { @@ -153,10 +153,10 @@ async fn spawn_handlers( ); let _ = awkernel_async_lib::spawn( - name.into(), + name.into(), poll_handler(if_status.interface_id, server), SchedulerType::PrioritizedFIFO(0), - ); + ); } if let Some(tick_msec) = if_status.tick_msec { @@ -170,10 +170,10 @@ async fn spawn_handlers( ); let _ = awkernel_async_lib::spawn( - name.into(), + name.into(), tick_handler(if_status.interface_id, tick_msec, server), SchedulerType::PrioritizedFIFO(0), - ); + ); } } From fa5cb14366fcc13566368eeec7581a450fc823db Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 19:55:01 +0900 Subject: [PATCH 17/22] Fix clippy warnings without logic changes --- applications/awkernel_services/src/lib.rs | 12 +++++------ .../awkernel_services/src/network_service.rs | 20 +++++++++---------- awkernel_async_lib/src/scheduler.rs | 5 +---- 3 files changed, 17 insertions(+), 20 deletions(-) diff --git a/applications/awkernel_services/src/lib.rs b/applications/awkernel_services/src/lib.rs index 6ae1cf017..45614ca0a 100644 --- a/applications/awkernel_services/src/lib.rs +++ b/applications/awkernel_services/src/lib.rs @@ -12,23 +12,23 @@ const BUFFERED_LOGGER_NAME: &str = "[Awkernel] buffered logger service"; const DISPLAY_SERVICE_NAME: &str = "[Awkernel] display service"; pub async fn run() { - let _ = awkernel_async_lib::spawn( + core::mem::drop(awkernel_async_lib::spawn( BUFFERED_LOGGER_NAME.into(), buffered_logger::run(), awkernel_async_lib::scheduler::SchedulerType::PrioritizedFIFO(0), - ); + )); - let _ = awkernel_async_lib::spawn( + core::mem::drop(awkernel_async_lib::spawn( NETWORK_SERVICE_NAME.into(), network_service::run(), awkernel_async_lib::scheduler::SchedulerType::PrioritizedFIFO(0), - ); + )); - let _ = awkernel_async_lib::spawn( + core::mem::drop(awkernel_async_lib::spawn( DISPLAY_SERVICE_NAME.into(), awkernel_display::run(), awkernel_async_lib::scheduler::SchedulerType::PrioritizedFIFO(0), - ); + )); awkernel_async_lib::sleep(Duration::from_secs(1)).await; awkernel_shell::init(); diff --git a/applications/awkernel_services/src/network_service.rs b/applications/awkernel_services/src/network_service.rs index 0d77dbd75..6e2ce6025 100644 --- a/applications/awkernel_services/src/network_service.rs +++ b/applications/awkernel_services/src/network_service.rs @@ -16,17 +16,17 @@ type ChanProtoInterruptHandlerDual = Chan<(), pub async fn run() { log::info!("Starting {}.", crate::NETWORK_SERVICE_NAME); - let _ = awkernel_async_lib::spawn( + core::mem::drop(awkernel_async_lib::spawn( GARBAGE_COLLECTOR_NAME.into(), tcp_garbage_collector(), SchedulerType::PrioritizedFIFO(0), - ); + )); - let _ = awkernel_async_lib::spawn( + core::mem::drop(awkernel_async_lib::spawn( NETWORK_IF_POLLER_NAME.into(), network_interface_poller(), SchedulerType::PrioritizedFIFO(0), - ); + )); let mut ch_irq_handlers = BTreeMap::new(); let mut ch_poll_handlers = BTreeMap::new(); @@ -135,11 +135,11 @@ async fn spawn_handlers( if_status.device_name, ); - let _ = awkernel_async_lib::spawn( + core::mem::drop(awkernel_async_lib::spawn( name.into(), interrupt_handler(if_status.interface_id, irq, server), SchedulerType::PrioritizedFIFO(0), - ); + )); } if if_status.poll_mode { @@ -152,11 +152,11 @@ async fn spawn_handlers( if_status.device_name, ); - let _ = awkernel_async_lib::spawn( + core::mem::drop(awkernel_async_lib::spawn( name.into(), poll_handler(if_status.interface_id, server), SchedulerType::PrioritizedFIFO(0), - ); + )); } if let Some(tick_msec) = if_status.tick_msec { @@ -169,11 +169,11 @@ async fn spawn_handlers( if_status.device_name, ); - let _ = awkernel_async_lib::spawn( + core::mem::drop(awkernel_async_lib::spawn( name.into(), tick_handler(if_status.interface_id, tick_msec, server), SchedulerType::PrioritizedFIFO(0), - ); + )); } } diff --git a/awkernel_async_lib/src/scheduler.rs b/awkernel_async_lib/src/scheduler.rs index de4b75625..f2d5c21ad 100644 --- a/awkernel_async_lib/src/scheduler.rs +++ b/awkernel_async_lib/src/scheduler.rs @@ -316,10 +316,7 @@ impl SleepingTasks { /// Wake tasks up. fn wake_task(&mut self) { - loop { - let Some((dur, _)) = self.delta_list.front() else { - break; - }; + while let Some((dur, _)) = self.delta_list.front() { let dur = Duration::from_nanos(dur); let elapsed = self.base_time.elapsed(); From 06bfe7949db2590b2ac90c79f81e9d3e71c69677 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 20:03:04 +0900 Subject: [PATCH 18/22] Await service task spawns before dropping handles --- applications/awkernel_services/src/lib.rs | 15 ++++++----- .../awkernel_services/src/network_service.rs | 25 +++++++++++-------- 2 files changed, 24 insertions(+), 16 deletions(-) diff --git a/applications/awkernel_services/src/lib.rs b/applications/awkernel_services/src/lib.rs index 45614ca0a..29544a811 100644 --- a/applications/awkernel_services/src/lib.rs +++ b/applications/awkernel_services/src/lib.rs @@ -12,23 +12,26 @@ const BUFFERED_LOGGER_NAME: &str = "[Awkernel] buffered logger service"; const DISPLAY_SERVICE_NAME: &str = "[Awkernel] display service"; pub async fn run() { - core::mem::drop(awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( BUFFERED_LOGGER_NAME.into(), buffered_logger::run(), awkernel_async_lib::scheduler::SchedulerType::PrioritizedFIFO(0), - )); + ) + .await; - core::mem::drop(awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( NETWORK_SERVICE_NAME.into(), network_service::run(), awkernel_async_lib::scheduler::SchedulerType::PrioritizedFIFO(0), - )); + ) + .await; - core::mem::drop(awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( DISPLAY_SERVICE_NAME.into(), awkernel_display::run(), awkernel_async_lib::scheduler::SchedulerType::PrioritizedFIFO(0), - )); + ) + .await; awkernel_async_lib::sleep(Duration::from_secs(1)).await; awkernel_shell::init(); diff --git a/applications/awkernel_services/src/network_service.rs b/applications/awkernel_services/src/network_service.rs index 6e2ce6025..4a7e30bf7 100644 --- a/applications/awkernel_services/src/network_service.rs +++ b/applications/awkernel_services/src/network_service.rs @@ -16,17 +16,19 @@ type ChanProtoInterruptHandlerDual = Chan<(), pub async fn run() { log::info!("Starting {}.", crate::NETWORK_SERVICE_NAME); - core::mem::drop(awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( GARBAGE_COLLECTOR_NAME.into(), tcp_garbage_collector(), SchedulerType::PrioritizedFIFO(0), - )); + ) + .await; - core::mem::drop(awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( NETWORK_IF_POLLER_NAME.into(), network_interface_poller(), SchedulerType::PrioritizedFIFO(0), - )); + ) + .await; let mut ch_irq_handlers = BTreeMap::new(); let mut ch_poll_handlers = BTreeMap::new(); @@ -135,11 +137,12 @@ async fn spawn_handlers( if_status.device_name, ); - core::mem::drop(awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( name.into(), interrupt_handler(if_status.interface_id, irq, server), SchedulerType::PrioritizedFIFO(0), - )); + ) + .await; } if if_status.poll_mode { @@ -152,11 +155,12 @@ async fn spawn_handlers( if_status.device_name, ); - core::mem::drop(awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( name.into(), poll_handler(if_status.interface_id, server), SchedulerType::PrioritizedFIFO(0), - )); + ) + .await; } if let Some(tick_msec) = if_status.tick_msec { @@ -169,11 +173,12 @@ async fn spawn_handlers( if_status.device_name, ); - core::mem::drop(awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( name.into(), tick_handler(if_status.interface_id, tick_msec, server), SchedulerType::PrioritizedFIFO(0), - )); + ) + .await; } } From 9894193f6e13a948aedb1d6327ad203a3fc18203 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 20:08:47 +0900 Subject: [PATCH 19/22] Handle missing preemption targets in schedulers --- awkernel_async_lib/src/scheduler/gedf.rs | 7 ++++--- awkernel_async_lib/src/scheduler/prioritized_rr.rs | 7 ++++--- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/awkernel_async_lib/src/scheduler/gedf.rs b/awkernel_async_lib/src/scheduler/gedf.rs index 09ec0d4f3..f72b9c2eb 100644 --- a/awkernel_async_lib/src/scheduler/gedf.rs +++ b/awkernel_async_lib/src/scheduler/gedf.rs @@ -172,10 +172,11 @@ impl GEDFScheduler { (max(t, highest_pending), rt.cpu_id) }) }) - .min() - .unwrap(); + .min(); - let (target_task, target_cpu) = preemption_target; + let Some((target_task, target_cpu)) = preemption_target else { + return false; + }; if task > target_task { push_preemption_pending(target_cpu, task); let preempt_irq = awkernel_lib::interrupt::get_preempt_irq(); diff --git a/awkernel_async_lib/src/scheduler/prioritized_rr.rs b/awkernel_async_lib/src/scheduler/prioritized_rr.rs index d06b3fe63..24af1d123 100644 --- a/awkernel_async_lib/src/scheduler/prioritized_rr.rs +++ b/awkernel_async_lib/src/scheduler/prioritized_rr.rs @@ -153,10 +153,11 @@ impl PrioritizedRRScheduler { (max(t, highest_pending), rt.cpu_id) }) }) - .min() - .unwrap(); + .min(); - let (target_task, target_cpu) = preemption_target; + let Some((target_task, target_cpu)) = preemption_target else { + return false; + }; if task > target_task { push_preemption_pending(target_cpu, task); let preempt_irq = awkernel_lib::interrupt::get_preempt_irq(); From 8550c73f1b912cda4386f2d80050958cc7c60512 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 20:16:47 +0900 Subject: [PATCH 20/22] fmt Signed-off-by: Yuuki Takano --- awkernel_async_lib/src/scheduler.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/awkernel_async_lib/src/scheduler.rs b/awkernel_async_lib/src/scheduler.rs index f2d5c21ad..25813ee73 100644 --- a/awkernel_async_lib/src/scheduler.rs +++ b/awkernel_async_lib/src/scheduler.rs @@ -317,7 +317,6 @@ impl SleepingTasks { /// Wake tasks up. fn wake_task(&mut self) { while let Some((dur, _)) = self.delta_list.front() { - let dur = Duration::from_nanos(dur); let elapsed = self.base_time.elapsed(); From 799dad676a47fe1928c96db02bb23b708302d273 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 20:39:57 +0900 Subject: [PATCH 21/22] Cover preempted kill race in SPIN --- awkernel_async_lib/src/scheduler.rs | 28 ++++++++++++++----- awkernel_async_lib/src/task/preempt.rs | 4 +++ .../src/task/preemptive_spin/Makefile | 4 +++ .../src/task/preemptive_spin/README.md | 6 ++++ .../task/preemptive_spin/data_structure.pml | 2 +- .../task/preemptive_spin/for_verification.pml | 2 +- .../src/task/preemptive_spin/future_mock.pml | 2 +- .../src/task/preemptive_spin/ltl.pml | 8 +++++- .../src/task/preemptive_spin/preemptive.pml | 27 +++++++++++++++--- 9 files changed, 68 insertions(+), 15 deletions(-) diff --git a/awkernel_async_lib/src/scheduler.rs b/awkernel_async_lib/src/scheduler.rs index 25813ee73..079177f42 100644 --- a/awkernel_async_lib/src/scheduler.rs +++ b/awkernel_async_lib/src/scheduler.rs @@ -7,6 +7,7 @@ use core::time::Duration; use crate::task::Task; use crate::task::{get_current_task, get_scheduler_type_by_task_id}; use alloc::collections::{binary_heap::BinaryHeap, btree_map::BTreeMap}; +use alloc::vec::Vec; use alloc::sync::Arc; use awkernel_async_lib_verified::delta_list::DeltaList; use awkernel_lib::{ @@ -314,8 +315,10 @@ impl SleepingTasks { self.delta_list.insert(dur.as_nanos() as u64, handler); } - /// Wake tasks up. - fn wake_task(&mut self) { + /// Take wake handlers for tasks whose sleep duration has elapsed. + fn take_wake_handlers(&mut self) -> Vec> { + let mut handlers = Vec::new(); + while let Some((dur, _)) = self.delta_list.front() { let dur = Duration::from_nanos(dur); let elapsed = self.base_time.elapsed(); @@ -332,8 +335,10 @@ impl SleepingTasks { break; }; - handler(); + handlers.push(handler); } + + handlers } /// Get the duration of between the current time and the time of the head. @@ -381,8 +386,17 @@ pub fn wake_task() -> Option { } } - let mut node = MCSNode::new(); - let mut guard = SLEEPING.lock(&mut node); - guard.wake_task(); - guard.time_to_wait() + let (handlers, time_to_wait) = { + let mut node = MCSNode::new(); + let mut guard = SLEEPING.lock(&mut node); + let handlers = guard.take_wake_handlers(); + let time_to_wait = guard.time_to_wait(); + (handlers, time_to_wait) + }; + + for handler in handlers { + handler(); + } + + time_to_wait } diff --git a/awkernel_async_lib/src/task/preempt.rs b/awkernel_async_lib/src/task/preempt.rs index e3bf06b8f..b434d3f7d 100644 --- a/awkernel_async_lib/src/task/preempt.rs +++ b/awkernel_async_lib/src/task/preempt.rs @@ -56,8 +56,12 @@ fn yield_preempted_and_wake_task(current_task: Arc, next_thread: PtrWorker { let mut node = MCSNode::new(); let mut info = current_task.info.lock(&mut node); + let kill_pending = matches!(info.state, super::State::Terminated | super::State::Panicked); info.set_preempt_context(current_ctx.clone()); info.state = super::State::Preempted; + if kill_pending { + info.kill_pending = true; + } info.num_preempt += 1; } diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/Makefile b/specification/awkernel_async_lib/src/task/preemptive_spin/Makefile index f0dcf6c1f..b46e96662 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/Makefile +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/Makefile @@ -16,6 +16,10 @@ kill-test: grep -q "errors: 0" kill-test-killed.log ./pan -a -n -m30000 -N kill_pending_eventually_terminated | tee kill-test-pending.log grep -q "errors: 0" kill-test-pending.log + spin -a -DKILL_RUNNING_PREEMPT_TEST preemptive.pml + gcc -O3 -DCOLLAPSE -DVECTORSZ=5000 -DNFAIR=3 -o pan pan.c + ./pan -a -n -m30000 -N killed_running_task_eventually_terminated | tee kill-test-running-preempt.log + grep -q "errors: 0" kill-test-running-preempt.log trail: clear diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/README.md b/specification/awkernel_async_lib/src/task/preemptive_spin/README.md index aac5a7b5c..6323a37c8 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/README.md +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/README.md @@ -179,11 +179,14 @@ This keeps `make run` free from the killer process and kill-only state such as ` In the kill-test variant, the model uses `TASK_NUM=2`, `CPU_NUM=1`, `WORKER_NUM=2`, and `IR_HANDLER_NUM=1`. Task 1 is the low-priority kill target, and task 0 is the high-priority task that preempts it. The `killer` process waits until task 1 becomes `Preempted`, then calls `kill_task(1)`. +`make kill-test` also runs `KILL_RUNNING_PREEMPT_TEST`, where `running_preempt_killer` kills task 1 while it is `Running` and an IPI preemption request is pending. +This covers the race where preemption overwrites `Terminated` with `Preempted`; the model requires that `kill_pending` preserves the kill signal and task 1 eventually returns to `Terminated`. Verified properties: 1. A killed task eventually becomes `Terminated` and is not running (`ltl killed_task_eventually_terminated_and_not_running`). 2. A task with `kill_pending` eventually becomes `Terminated` (`ltl kill_pending_eventually_terminated`). +3. A task killed while running with preemption pending eventually becomes `Terminated` (`ltl killed_running_task_eventually_terminated`). Result: @@ -195,6 +198,9 @@ State-vector 400 byte, depth reached 888, errors: 0 ... State-vector 400 byte, depth reached 888, errors: 0 7590 states, stored (8972 visited) +... +State-vector 392 byte, depth reached 20644, errors: 0 + 19514 states, stored ``` No invalid array index was reported. diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml index d31557bf0..e6680443c 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml @@ -16,7 +16,7 @@ typedef TaskInfo { bool need_sched = false; byte id;// This also represents the priority of the task. The lower the value,the higher the priority. bool need_preemption = false; -#ifdef KILL_TEST +#if defined(KILL_TEST) || defined(KILL_RUNNING_PREEMPT_TEST) bool kill_pending = false; #endif short thread = - 1;// tid when this task is preempted, -1 otherwise. diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/for_verification.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/for_verification.pml index 361852082..c3323cafb 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/for_verification.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/for_verification.pml @@ -1,7 +1,7 @@ byte num_terminated = 0 byte waking[TASK_NUM] = 0 -#ifdef KILL_TEST +#if defined(KILL_TEST) || defined(KILL_RUNNING_PREEMPT_TEST) bool killed[TASK_NUM] = false bool kill_requested[TASK_NUM] = false byte num_kill_requests = 0 diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml index 478dbb904..57c393149 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml @@ -1,6 +1,6 @@ bool future_blocked[TASK_NUM] = false -#ifdef KILL_TEST +#if defined(KILL_TEST) || defined(KILL_RUNNING_PREEMPT_TEST) // Kill-test variant: task 1 is the low-priority target, task 0 preempts it. inline future(tid,task,ret) { printf("future(): tid = %d, task = %d\n", tid, task); diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/ltl.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/ltl.pml index be46a2ae9..a8993f425 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/ltl.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/ltl.pml @@ -1,4 +1,4 @@ -#ifdef KILL_TEST +#if defined(KILL_TEST) || defined(KILL_RUNNING_PREEMPT_TEST) ltl killed_task_eventually_terminated_and_not_running { [](!killed[1] || <> (tasks[1].state == Terminated && RUNNING[0] != 1)) } @@ -6,6 +6,12 @@ ltl killed_task_eventually_terminated_and_not_running { ltl kill_pending_eventually_terminated { [](!tasks[1].kill_pending || <> (tasks[1].state == Terminated)) } + +#ifdef KILL_RUNNING_PREEMPT_TEST +ltl killed_running_task_eventually_terminated { + [](!killed[1] || <> (tasks[1].state == Terminated && RUNNING[0] != 1)) +} +#endif #else ltl eventually_terminate { <> (num_terminated == TASK_NUM) diff --git a/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml b/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml index a8b43da93..a4bff26fa 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml @@ -1,4 +1,4 @@ -#ifdef KILL_TEST +#if defined(KILL_TEST) || defined(KILL_RUNNING_PREEMPT_TEST) #define TASK_NUM 2 #define WORKER_NUM 2// One running worker and one preemption context worker. #define IR_HANDLER_NUM 1// One interrupt handler is enough with CPU_NUM == 1. @@ -143,7 +143,7 @@ inline wake(tid,task) { fi } -#ifdef KILL_TEST +#if defined(KILL_TEST) || defined(KILL_RUNNING_PREEMPT_TEST) inline kill_task(tid,task) { bool was_killed; was_killed = false; @@ -159,7 +159,9 @@ inline kill_task(tid,task) { :: !killed[task] -> killed[task] = true; num_kill_requests++; - num_terminated++; +#ifndef KILL_RUNNING_PREEMPT_TEST + num_terminated++; +#endif :: else fi was_killed = true; @@ -304,6 +306,13 @@ inline yield_preempted_and_wake_task(cur_task,cur_tid,next_tid) { lock(cur_tid,lock_info[cur_task]); set_preempt_context(cur_task,cur_tid); d_step { +#if defined(KILL_TEST) || defined(KILL_RUNNING_PREEMPT_TEST) + if + :: tasks[cur_task].state == Terminated || tasks[cur_task].state == Panicked -> + tasks[cur_task].kill_pending = true + :: else -> skip + fi; +#endif tasks[cur_task].state = Preempted; update_runnable_preempted_highest_priority(); update_running_lowest_priority(); @@ -633,6 +642,16 @@ proctype killer(byte tid) { } #endif +#ifdef KILL_RUNNING_PREEMPT_TEST +proctype running_preempt_killer(byte tid) { + do + :: tasks[1].state == Running && len(ipi_requests[0]) > 0 -> break + :: else -> skip + od; + kill_task(tid,1); +} +#endif + init { byte i; #ifdef KILL_TEST @@ -643,7 +662,7 @@ init { tasks[i].id = i; } tasks[0].scheduler_type = 0; -#ifdef KILL_TEST +#if defined(KILL_TEST) || defined(KILL_RUNNING_PREEMPT_TEST) tasks[1].scheduler_type = 0; #else #if SCHED_TYPE_PATTERN==0 From e99f32ef0d5d0e7474bdffc8d89046a1fa3486c8 Mon Sep 17 00:00:00 2001 From: Yuuki Takano Date: Wed, 17 Jun 2026 20:43:29 +0900 Subject: [PATCH 22/22] fmt Signed-off-by: Yuuki Takano --- awkernel_async_lib/src/scheduler.rs | 2 +- awkernel_async_lib/src/task/preempt.rs | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/awkernel_async_lib/src/scheduler.rs b/awkernel_async_lib/src/scheduler.rs index 079177f42..fa3a15fff 100644 --- a/awkernel_async_lib/src/scheduler.rs +++ b/awkernel_async_lib/src/scheduler.rs @@ -7,8 +7,8 @@ use core::time::Duration; use crate::task::Task; use crate::task::{get_current_task, get_scheduler_type_by_task_id}; use alloc::collections::{binary_heap::BinaryHeap, btree_map::BTreeMap}; -use alloc::vec::Vec; use alloc::sync::Arc; +use alloc::vec::Vec; use awkernel_async_lib_verified::delta_list::DeltaList; use awkernel_lib::{ cpu::num_cpu, diff --git a/awkernel_async_lib/src/task/preempt.rs b/awkernel_async_lib/src/task/preempt.rs index b434d3f7d..8df4823d6 100644 --- a/awkernel_async_lib/src/task/preempt.rs +++ b/awkernel_async_lib/src/task/preempt.rs @@ -56,7 +56,10 @@ fn yield_preempted_and_wake_task(current_task: Arc, next_thread: PtrWorker { let mut node = MCSNode::new(); let mut info = current_task.info.lock(&mut node); - let kill_pending = matches!(info.state, super::State::Terminated | super::State::Panicked); + let kill_pending = matches!( + info.state, + super::State::Terminated | super::State::Panicked + ); info.set_preempt_context(current_ctx.clone()); info.state = super::State::Preempted; if kill_pending {