fix: Renaming the Task State (Ready to Initialized)

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,

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,15 +77,15 @@ 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`,
 and `Preempted` state is also omitted because this verification is for cooperative multitask.
 
 ```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;

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

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]);
@@ -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);
 

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

specification/awkernel_async_lib/src/task/preemptive_spin/README.md

@@ -250,15 +250,15 @@ 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<runnable_preempted_highest_priority)))
 Never claim moves to line 22    [(1)]
-              wake() call wake_task(): tid = 0,task = 3,state = Ready
+              wake() call wake_task(): tid = 0,task = 3,state = Initialized
               get_lowest_priority_task(): task = 3
               invoke_preemption() no need to preempt: hp_task = 3,lp_task = 0
               wake_task(): push to queue: tid = 0,task = 3
                                       proc 7 (run_main),tid = 1
                                       scheduler_get_next(): tid = 1,Chosen task = 3
                                       RUNNING[1] = 3
                                       future(): tid = 1, task = 3
-                                      wake() call wake_task(): tid = 1,task = 2,state = Ready
+                                      wake() call wake_task(): tid = 1,task = 2,state = Initialized
                                       get_lowest_priority_task(): task = 2
                                       invoke_preemption() send IPI: hp_task = 2,lp_task = 3,lp_cpu_id = 1,interrupt_enabled[lp_cpu_id] = 0
                                   proc 6 (run_main),tid = 0
@@ -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

specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml

@@ -7,11 +7,11 @@ typedef Worker {
 
 Worker workers[WORKER_NUM]
 
-mtype = { Ready,Runnable,Running,Waiting,Terminated,Pending,Preempted }// Panic is not considered.
+mtype = { Initialized,Runnable,Running,Waiting,Terminated,Pending,Preempted }// Panic is not considered.
 
 /* awkernel_async_lib::task::TaskInfo */
 typedef TaskInfo {
-	mtype state = Ready;
+	mtype state = Initialized;
 	byte scheduler_type;// The lower the value, the higher the priority.
 	bool need_sched = false;
 	byte id;// This also represents the priority of the task. The lower the value,the higher the priority.

specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml

@@ -124,7 +124,7 @@ inline wake(tid,task) {
 			waking[task]--;
 		}
 		unlock(tid,lock_info[task])
-	:: tasks[task].state == Waiting || tasks[task].state == Ready -> 
+	:: 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;