From 49a56c01ce0a9a51c1e9230a7f558b015b901907 Mon Sep 17 00:00:00 2001 From: nokosaaan Date: Wed, 19 Nov 2025 15:56:44 +0900 Subject: [PATCH 1/2] fix: Ready to Initialized in awkernel Signed-off-by: nokosaaan --- awkernel_async_lib/src/task.rs | 6 +++--- .../awkernel_async_lib/src/task/cooperative/README.md | 8 ++++---- .../src/task/cooperative/cooperative.tla | 8 ++++---- .../src/task/cooperative_spin/cooperative.pml | 6 +++--- .../cooperative_with_infinite_loop.tla | 8 ++++---- .../awkernel_async_lib/src/task/preemptive_spin/README.md | 4 ++-- .../src/task/preemptive_spin/data_structure.pml | 4 ++-- .../src/task/preemptive_spin/preemptive.pml | 2 +- 8 files changed, 23 insertions(+), 23 deletions(-) diff --git a/awkernel_async_lib/src/task.rs b/awkernel_async_lib/src/task.rs index 6e4ee4636..bdb73c447 100644 --- a/awkernel_async_lib/src/task.rs +++ b/awkernel_async_lib/src/task.rs @@ -126,7 +126,7 @@ impl ArcWake for Task { Terminated | Panicked => { return; } - Ready | Waiting => { + Initialized | Waiting => { info.state = Runnable; } } @@ -230,7 +230,7 @@ impl TaskInfo { /// State of task. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum State { - Ready, + Initialized, Running, Runnable, Waiting, @@ -278,7 +278,7 @@ impl Tasks { if let btree_map::Entry::Vacant(e) = self.id_to_task.entry(id) { let info = Mutex::new(TaskInfo { scheduler_type, - state: State::Ready, + state: State::Initialized, num_preempt: 0, last_executed_time: awkernel_lib::time::Time::now(), absolute_deadline: None, diff --git a/specification/awkernel_async_lib/src/task/cooperative/README.md b/specification/awkernel_async_lib/src/task/cooperative/README.md index b4eb38afb..9c0e4a929 100644 --- a/specification/awkernel_async_lib/src/task/cooperative/README.md +++ b/specification/awkernel_async_lib/src/task/cooperative/README.md @@ -63,7 +63,7 @@ lock_future = [x \in 1..TASK_NUM |-> FALSE]; lock_scheduler = FALSE; \* awkernel_async_lib::task::State -state = [x \in 1..TASK_NUM |-> "Ready"]; +state = [x \in 1..TASK_NUM |-> "Initialized"]; is_terminated = [x \in 1..TASK_NUM |-> FALSE]; @@ -77,7 +77,7 @@ wake_other = [x \in ((TASK_NUM \div 2) + 1)..TASK_NUM |-> FALSE]; `result_next` and `result_future` are variable to be stored of results of `get_next` and `future` procedures, respectively. -Each entry of `state` must be `Ready`, `Waiting`, `Runnable`, `Running`, `Panicked`, +Each entry of `state` must be `Initialized`, `Waiting`, `Runnable`, `Running`, `Panicked`, or `Terminated`, as `task::State` defined in `task.rs`, as follows. `Panicked` state is omitted in this verification because it is almost equivalent to `Terminated`, @@ -85,7 +85,7 @@ and `Preempted` state is also omitted because this verification is for cooperati ```rust pub enum State { - Ready, + Initialized, Running, Runnable, Waiting, @@ -97,7 +97,7 @@ pub enum State { ```mermaid graph TD; - Ready-->Runnable; + Initialized-->Runnable; Running-->Preempted-->Running; Running-->Terminated; Running-->Panicked; diff --git a/specification/awkernel_async_lib/src/task/cooperative/cooperative.tla b/specification/awkernel_async_lib/src/task/cooperative/cooperative.tla index 702399f27..d076ef8fa 100644 --- a/specification/awkernel_async_lib/src/task/cooperative/cooperative.tla +++ b/specification/awkernel_async_lib/src/task/cooperative/cooperative.tla @@ -18,7 +18,7 @@ variables need_sched = [x \in 1..TASK_NUM |-> FALSE]; \* awkernel_async_lib::task::State - state = [x \in 1..TASK_NUM |-> "Ready"]; + state = [x \in 1..TASK_NUM |-> "Initialized"]; is_terminated = [x \in 1..TASK_NUM |-> FALSE]; @@ -62,7 +62,7 @@ begin wake_but_terminated: lock_info[task] := FALSE; return; - elsif state[task] \in {"Waiting", "Ready"} then + elsif state[task] \in {"Waiting", "Initialized"} then state[task] := "Runnable"; end if; @@ -283,7 +283,7 @@ Init == (* Global variables *) /\ lock_future = [x \in 1..TASK_NUM |-> FALSE] /\ lock_scheduler = FALSE /\ need_sched = [x \in 1..TASK_NUM |-> FALSE] - /\ state = [x \in 1..TASK_NUM |-> "Ready"] + /\ state = [x \in 1..TASK_NUM |-> "Initialized"] /\ is_terminated = [x \in 1..TASK_NUM |-> FALSE] /\ result_next = [x \in WORKERS |-> -1] /\ result_future = [x \in WORKERS |-> ""] @@ -340,7 +340,7 @@ start_wake(self) == /\ pc[self] = "start_wake" ELSE /\ IF state[task_wa[self]] = "Terminated" THEN /\ pc' = [pc EXCEPT ![self] = "wake_but_terminated"] /\ state' = state - ELSE /\ IF state[task_wa[self]] \in {"Waiting", "Ready"} + ELSE /\ IF state[task_wa[self]] \in {"Waiting", "Initialized"} THEN /\ state' = [state EXCEPT ![task_wa[self]] = "Runnable"] ELSE /\ TRUE /\ state' = state diff --git a/specification/awkernel_async_lib/src/task/cooperative_spin/cooperative.pml b/specification/awkernel_async_lib/src/task/cooperative_spin/cooperative.pml index 762827efe..3afb65656 100644 --- a/specification/awkernel_async_lib/src/task/cooperative_spin/cooperative.pml +++ b/specification/awkernel_async_lib/src/task/cooperative_spin/cooperative.pml @@ -8,9 +8,9 @@ #include "fair_lock.pml" -mtype = { Ready, Runnable, Running, Waiting, Terminated, Pending }; +mtype = { Initialized, Runnable, Running, Waiting, Terminated, Pending }; -mtype state = Ready; +mtype state = Initialized; // awkernel_async_lib::task::TaskInfo typedef TaskInfo { @@ -53,7 +53,7 @@ inline wake(tid, task) { printf("wake(): task = %d, state = %d\n", task, tasks[task].state); unlock(tid, lock_info[task]); :: tasks[task].state == Terminated -> unlock(tid, lock_info[task]); - :: tasks[task].state == Waiting || tasks[task].state == Ready -> + :: tasks[task].state == Waiting || tasks[task].state == Initialized -> printf("wake(): task = %d, state = %d\n", task, tasks[task].state); tasks[task].state = Runnable; unlock(tid, lock_info[task]); diff --git a/specification/awkernel_async_lib/src/task/cooperative_with_infinite_loop/cooperative_with_infinite_loop.tla b/specification/awkernel_async_lib/src/task/cooperative_with_infinite_loop/cooperative_with_infinite_loop.tla index bafcb47c0..8816d4204 100644 --- a/specification/awkernel_async_lib/src/task/cooperative_with_infinite_loop/cooperative_with_infinite_loop.tla +++ b/specification/awkernel_async_lib/src/task/cooperative_with_infinite_loop/cooperative_with_infinite_loop.tla @@ -22,7 +22,7 @@ variables need_sched = [x \in 1..TOTAL_TASK_NUM |-> FALSE]; \* awkernel_async_lib::task::State - state = [x \in 1..TOTAL_TASK_NUM |-> "Ready"]; + state = [x \in 1..TOTAL_TASK_NUM |-> "Initialized"]; is_terminated = [x \in 1..TOTAL_TASK_NUM |-> FALSE]; @@ -64,7 +64,7 @@ begin wake_but_terminated: lock_info[task] := FALSE; return; - elsif state[task] \in {"Waiting", "Ready"} then + elsif state[task] \in {"Waiting", "Initialized"} then state[task] := "Runnable"; end if; @@ -274,7 +274,7 @@ Init == (* Global variables *) /\ lock_future = [x \in 1..TOTAL_TASK_NUM |-> FALSE] /\ lock_scheduler = FALSE /\ need_sched = [x \in 1..TOTAL_TASK_NUM |-> FALSE] - /\ state = [x \in 1..TOTAL_TASK_NUM |-> "Ready"] + /\ state = [x \in 1..TOTAL_TASK_NUM |-> "Initialized"] /\ is_terminated = [x \in 1..TOTAL_TASK_NUM |-> FALSE] /\ result_next = [x \in WORKERS |-> -1] /\ result_future = [x \in WORKERS |-> ""] @@ -329,7 +329,7 @@ start_wake(self) == /\ pc[self] = "start_wake" ELSE /\ IF state[task_wa[self]] = "Terminated" THEN /\ pc' = [pc EXCEPT ![self] = "wake_but_terminated"] /\ state' = state - ELSE /\ IF state[task_wa[self]] \in {"Waiting", "Ready"} + ELSE /\ IF state[task_wa[self]] \in {"Waiting", "Initialized"} THEN /\ state' = [state EXCEPT ![task_wa[self]] = "Runnable"] ELSE /\ TRUE /\ state' = state 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 6a96dc29f..2e7e7806f 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/README.md +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/README.md @@ -250,7 +250,7 @@ ltl eventually_terminate: <> ((num_terminated==4)) ltl eventually_prerequisites: [] (<> (((((((((((waking[0]==0)) && ((waking[1]==0))) && ((waking[2]==0))) && ((waking[3]==0))) && ((len(ipi_requests[0])==0))) && ((len(ipi_requests[1])==0))) && (! (handling_interrupt[0]))) && (! (handling_interrupt[1]))) && (! (handling_interrupt[2]))) && (! (handling_interrupt[3])))) ltl ensure_priority: [] ((! (((((((((((((((waking[0]==0)) && ((waking[1]==0))) && ((waking[2]==0))) && ((waking[3]==0))) && ((len(ipi_requests[0])==0))) && ((RUNNING[0]!=-(1)))) && ((RUNNING[0]!=runnable_preempted_highest_priority))) && ((len(ipi_requests[1])==0))) && ((RUNNING[1]!=-(1)))) && ((RUNNING[1]!=runnable_preempted_highest_priority))) && (! (handling_interrupt[0]))) && (! (handling_interrupt[1]))) && (! (handling_interrupt[2]))) && (! (handling_interrupt[3])))) || ((running_lowest_priority + :: tasks[task].state == Waiting || tasks[task].state == Initialized -> d_step{ printf("wake() call wake_task(): tid = %d,task = %d,state = %e\n",tid,task,tasks[task].state); tasks[task].state = Runnable; From 4b7ff9524f8d42673c6bb27f747e39d6d960d02c Mon Sep 17 00:00:00 2001 From: nokosaaan Date: Thu, 20 Nov 2025 11:01:53 +0900 Subject: [PATCH 2/2] fix: additional Ready to Initialized Signed-off-by: nokosaaan --- .../src/task/cooperative_spin/cooperative.pml | 2 +- .../awkernel_async_lib/src/task/preemptive_spin/README.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/specification/awkernel_async_lib/src/task/cooperative_spin/cooperative.pml b/specification/awkernel_async_lib/src/task/cooperative_spin/cooperative.pml index 3afb65656..b5be8c372 100644 --- a/specification/awkernel_async_lib/src/task/cooperative_spin/cooperative.pml +++ b/specification/awkernel_async_lib/src/task/cooperative_spin/cooperative.pml @@ -240,7 +240,7 @@ init { for (i: 0 .. TASK_NUM - 1) { tasks[i].id = i; - tasks[i].state = Ready; + tasks[i].state = Initialized; printf("tasks[%d].state = %d\n", i, tasks[i].state); 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 2e7e7806f..974e4ea94 100644 --- a/specification/awkernel_async_lib/src/task/preemptive_spin/README.md +++ b/specification/awkernel_async_lib/src/task/preemptive_spin/README.md @@ -273,10 +273,10 @@ Never claim moves to line 22 [(1)] wake_task(): push to queue: tid = 2,task = 3 RUNNING[1] = 2 future(): tid = 2, task = 2 - wake() call wake_task(): tid = 2,task = 1,state = Ready + wake() call wake_task(): tid = 2,task = 1,state = Initialized get_lowest_priority_task(): task = 1 invoke_preemption() send IPI: hp_task = 1,lp_task = 2,lp_cpu_id = 1,interrupt_enabled[lp_cpu_id] = 0 - wake() call wake_task(): tid = 2,task = 0,state = Ready + wake() call wake_task(): tid = 2,task = 0,state = Initialized get_lowest_priority_task(): task = 0 invoke_preemption() send IPI: hp_task = 0,lp_task = 1,lp_cpu_id = 1,interrupt_enabled[lp_cpu_id] = 0 scheduler_get_next(): tid = 0,Chosen task = 3