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 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/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/lib.rs b/applications/awkernel_services/src/lib.rs index 900163ffb..29544a811 100644 --- a/applications/awkernel_services/src/lib.rs +++ b/applications/awkernel_services/src/lib.rs @@ -12,21 +12,21 @@ 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), diff --git a/applications/awkernel_services/src/network_service.rs b/applications/awkernel_services/src/network_service.rs index 261b579ec..4a7e30bf7 100644 --- a/applications/awkernel_services/src/network_service.rs +++ b/applications/awkernel_services/src/network_service.rs @@ -16,14 +16,14 @@ 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), @@ -137,7 +137,7 @@ async fn spawn_handlers( if_status.device_name, ); - awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( name.into(), interrupt_handler(if_status.interface_id, irq, server), SchedulerType::PrioritizedFIFO(0), @@ -155,7 +155,7 @@ async fn spawn_handlers( if_status.device_name, ); - awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( name.into(), poll_handler(if_status.interface_id, server), SchedulerType::PrioritizedFIFO(0), @@ -173,7 +173,7 @@ async fn spawn_handlers( if_status.device_name, ); - awkernel_async_lib::spawn( + let _ = awkernel_async_lib::spawn( name.into(), tick_handler(if_status.interface_id, tick_msec, server), SchedulerType::PrioritizedFIFO(0), 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..889b41a97 --- /dev/null +++ b/applications/tests/test_task_kill/src/lib.rs @@ -0,0 +1,235 @@ +#![no_std] + +extern crate alloc; + +use awkernel_async_lib::{scheduler::SchedulerType, sleep, task}; +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; + log::info!("TASK_KILL_TEST start"); + + kill_sleeping_task().await; + kill_unknown_id(); + kill_idempotent().await; + resources_freed_after_kill().await; + kill_preempted_task().await; + kill_panicked_task().await; + + log::info!("TASK_KILL_TEST done"); +} + +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_millis(40)).await; + } + }, + SchedulerType::PrioritizedFIFO(0), + ); + + sleep(Duration::from_millis(20)).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)"); + } + + 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() { + 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)"); + } +} + +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 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); + + // 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. The dropped Waker should + // drop the future and trigger the DropTracker. + 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); + + if wait_for_drop_count(1, 8).await { + 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) + ); + } +} + +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..fa3a15fff 100644 --- a/awkernel_async_lib/src/scheduler.rs +++ b/awkernel_async_lib/src/scheduler.rs @@ -8,6 +8,7 @@ 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::sync::Arc; +use alloc::vec::Vec; use awkernel_async_lib_verified::delta_list::DeltaList; use awkernel_lib::{ cpu::num_cpu, @@ -314,24 +315,30 @@ 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(); - if dur <= elapsed { - // Timed out. - if let DeltaList::Cons(data) = self.delta_list.pop().unwrap() { - let (_, handler, _) = data.into_inner(); - handler(); // Invoke a handler. + if dur > elapsed { + break; + } - self.base_time += dur; - } + let handler = if let DeltaList::Cons(data) = self.delta_list.pop().unwrap() { + let (_, handler, _) = data.into_inner(); + self.base_time += dur; + handler } else { break; - } + }; + + handlers.push(handler); } + + handlers } /// Get the duration of between the current time and the time of the head. @@ -379,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/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_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/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(); 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(); } }), diff --git a/awkernel_async_lib/src/task.rs b/awkernel_async_lib/src/task.rs index 8f0235260..78aa68205 100644 --- a/awkernel_async_lib/src/task.rs +++ b/awkernel_async_lib/src/task.rs @@ -156,6 +156,22 @@ impl ArcWake for Task { } } +#[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 { pub(crate) state: State, @@ -170,6 +186,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 +210,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 +350,9 @@ impl Tasks { #[cfg(not(feature = "no_preempt"))] thread: None, + + #[cfg(not(feature = "no_preempt"))] + kill_pending: false, }); // Set the task priority. @@ -780,6 +815,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(); @@ -819,6 +860,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; } @@ -882,13 +925,30 @@ 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; + // 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) { + 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); + drop_task_future(&task); + 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(); + } + } + } else { drop(info); - task.clone().wake(); + drop_task_future(&task); } } Ok(Poll::Ready(result)) => { @@ -947,6 +1007,76 @@ 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 +/// 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`. +/// 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. 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. + 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, + #[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, + } + } + + // 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). + drop_task_future(&task); + { + 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(); diff --git a/awkernel_async_lib/src/task/preempt.rs b/awkernel_async_lib/src/task/preempt.rs index b1129cec4..8df4823d6 100644 --- a/awkernel_async_lib/src/task/preempt.rs +++ b/awkernel_async_lib/src/task/preempt.rs @@ -56,8 +56,15 @@ 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; } @@ -135,14 +142,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 +172,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); 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/specification/awkernel_async_lib/src/task/preemptive_spin/Makefile b/specification/awkernel_async_lib/src/task/preemptive_spin/Makefile index 2a77926f6..b46e96662 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/Makefile +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/Makefile @@ -8,9 +8,22 @@ 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 + 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 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..6323a37c8 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,40 @@ 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)`. +`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: + +``` +$ 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) +... +State-vector 392 byte, depth reached 20644, errors: 0 + 19514 states, stored +``` + +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 ab7869074..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 @@ -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,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; +#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 dce3d2be4..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,6 +1,11 @@ byte num_terminated = 0 byte waking[TASK_NUM] = 0 +#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 +#endif bool handling_interrupt[IR_HANDLER_NUM] = false byte runnable_preempted_highest_priority = BYTE_MAX @@ -12,7 +17,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 +31,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 +47,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..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,5 +1,23 @@ bool future_blocked[TASK_NUM] = false +#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); + 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); @@ -9,26 +27,27 @@ 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 } #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 92474bdb5..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,3 +1,18 @@ +#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)) +} + +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) } @@ -17,3 +32,4 @@ ltl ensure_priority { !handling_interrupt[0] && !handling_interrupt[1] && !handling_interrupt[2] && !handling_interrupt[3]) -> (running_lowest_priority < runnable_preempted_highest_priority)) } +#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 26a055ca4..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,7 +1,14 @@ +#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. +#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" @@ -117,9 +124,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 +143,57 @@ inline wake(tid,task) { fi } +#if defined(KILL_TEST) || defined(KILL_RUNNING_PREEMPT_TEST) +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++; +#ifndef KILL_RUNNING_PREEMPT_TEST + num_terminated++; +#endif + :: 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 +} + +#endif + /* 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 +207,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 -> @@ -248,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(); @@ -300,7 +365,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 +379,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 +415,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 +438,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 +576,45 @@ 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 +#ifdef KILL_TEST + :: 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 +#endif + :: 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,13 +632,39 @@ proctype run_main(byte tid) provided (workers[tid].executing_in != - 1 && !worke } +#ifdef KILL_TEST +proctype killer(byte tid) { + do + :: tasks[1].state == Preempted -> break + :: else -> skip + od; + kill_task(tid,1); +} +#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 + run killer(0); +#endif for (i: 0 .. TASK_NUM - 1) { tasks[i].id = i; } tasks[0].scheduler_type = 0; +#if defined(KILL_TEST) || defined(KILL_RUNNING_PREEMPT_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 @@ -518,6 +673,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); 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(()) }