fix: Renaming the Task State (Ready to Initialized)

[nokosaaan]

Description

・The Ready state and Runnable state are treated as synonymous in the OS industry.
・If the intent is to indicate that task initialization is complete, Initialized is more appropriate than Ready.

Related links

google slide (Reported at the meeting on November 18, 2025)

How was this PR tested?

• environment
  • Raspberry Pi 4 (AArch64)
• test applications
  • test_dag
• result
  • I added logging to the state transition section within wake in task.rs. After changing from Ready to Initialized, you can confirm that task execution and state transitions are functioning correctly.

[before]
[ 11208 DEBUG] /home/nokosan/azumi-lab/awkernel6/applications/tests/test_dag/src/lib.rs:18: period is 1000000000 [ns]
[ 11208 INFO] task#12 state: Ready-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 11208 INFO] task#13 state: Ready-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 2 })
[ 11208 INFO] task#14 state: Ready-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 3 })
[ 11208 INFO] task#15 state: Ready-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 4 })
[ 11208 INFO] task#16 state: Ready-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 0 })
[ 11209 INFO] task#16 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 0 })
[ 11309 INFO] task#12 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 11309 INFO] task#16 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 0 })
[ 11309 INFO] task#13 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 2 })
[ 11309 INFO] task#12 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 11309 INFO] task#15 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 4 })
[ 11309 INFO] task#14 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 3 })
[ 11309 INFO] task#13 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 2 })
[ 11309 INFO] task#14 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 3 })
[ 11309 INFO] task#12 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 12209 INFO] task#16 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 0 })
[ 12309 INFO] task#12 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 12309 INFO] task#16 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 0 })
[ 12309 INFO] task#13 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 2 })
[ 12309 INFO] task#12 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 12309 INFO] task#15 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 4 })
[ 12309 INFO] task#14 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 3 })
[ 12309 INFO] task#13 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 2 })
[ 12309 INFO] task#14 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 3 })
[ 12309 INFO] task#12 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 13209 INFO] task#16 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 0 })

[after]
[ 11208 DEBUG] /home/nokosan/azumi-lab/awkernel5/applications/tests/test_dag/src/lib.rs:18: period is 1000000000 [ns]
[ 11209 INFO] task#12 state: Initialized-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 11209 INFO] task#13 state: Initialized-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 2 })
[ 11209 INFO] task#14 state: Initialized-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 3 })
[ 11209 INFO] task#15 state: Initialized-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 4 })
[ 11209 INFO] task#16 state: Initialized-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 0 })
[ 11209 INFO] task#16 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 0 })
[ 11309 INFO] task#12 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 11309 INFO] task#16 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 0 })
[ 11309 INFO] task#13 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 2 })
[ 11309 INFO] task#12 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 11309 INFO] task#15 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 4 })
[ 11309 INFO] task#14 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 3 })
[ 11309 INFO] task#13 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 2 })
[ 11309 INFO] task#15 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 4 })
[ 11309 INFO] task#12 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 11309 INFO] task#14 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 3 })
[ 12209 INFO] task#16 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 0 })
[ 12309 INFO] task#12 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 12309 INFO] task#16 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 0 })
[ 12309 INFO] task#13 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 2 })
[ 12309 INFO] task#12 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 12309 INFO] task#15 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 4 })
[ 12309 INFO] task#14 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 3 })
[ 12309 INFO] task#13 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 2 })
[ 12309 INFO] task#14 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 3 })
[ 12309 INFO] task#12 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 1 })
[ 13209 INFO] task#16 state: Waiting-> Runnable dag_info: Some(DagInfo { dag_id: 1, node_id: 0 })

Notes for reviewers

[Copilot]

Pull Request Overview

This PR renames the Ready task state to Initialized across the awkernel codebase to better align with OS industry terminology, where Ready and Runnable are typically synonymous. The change aims to make it clearer that tasks in this state have completed initialization but are not yet runnable.

Key changes:

• Renamed State::Ready to State::Initialized in the task state enum
• Updated all references in Rust source code and formal specifications (Promela/TLA+)
• Updated state transition checks and initializations across cooperative and preemptive schedulers

Reviewed Changes

Copilot reviewed 8 out of 8 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
awkernel_async_lib/src/task.rs	Updated State enum definition and state checks in task implementation
specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml	Updated state check in wake() function
specification/awkernel_async_lib/src/task/preemptive_spin/data_structure.pml	Updated mtype definition and default task state
specification/awkernel_async_lib/src/task/preemptive_spin/README.md	Updated verification output examples
specification/awkernel_async_lib/src/task/cooperative_with_infinite_loop/cooperative_with_infinite_loop.tla	Updated state initialization and checks in TLA+ spec
specification/awkernel_async_lib/src/task/cooperative_spin/cooperative.pml	Updated mtype definition and state checks
specification/awkernel_async_lib/src/task/cooperative/cooperative.tla	Updated state initialization and checks in TLA+ spec
specification/awkernel_async_lib/src/task/cooperative/README.md	Updated documentation and state diagram

Comments suppressed due to low confidence (3)

specification/awkernel_async_lib/src/task/cooperative_spin/cooperative.pml:243

• The value Ready is no longer defined in the mtype after being renamed to Initialized on line 11. This should be tasks[i].state = Initialized; to match the updated mtype definition.

        tasks[i].state = Ready;

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

• This verification output shows state = Ready but should show state = Initialized to reflect the renamed task state. This trace output needs to be regenerated or manually updated to match the code changes.

                                          wake() call wake_task(): tid = 2,task = 1,state = Ready

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

• This verification output shows state = Ready but should show state = Initialized to reflect the renamed task state. This trace output needs to be regenerated or manually updated to match the code changes.

                                          wake() call wake_task(): tid = 2,task = 0,state = Ready

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull Request Overview

Copilot reviewed 8 out of 8 changed files in this pull request and generated no new comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[atsushi421]

@nokosaaan
Could you run the some related test applications?

[nokosaaan]

I conducted the test and added the results to “How was this PR tested?”.
Please let me know if I've misunderstood.

[atsushi421]

@nokosaaan
Thank you for addressing.
Then, I found that the Ready remains in some files in specification (e.g., cooperrative.tla and preemptive.pml). So, could you fix it?

[nokosaaan]

@atsushi421
Upon verification, I believe the remaining Ready likely refers to the Ready from the Future trait's Poll method. For example, in preemptive.pml, since poll_result == Ready, I interpreted this as indicating Poll::Ready rather than Ready as a task state. Since the Poll method relies on Rust's built-in functionality, I considered it outside the scope of this change. Should this also be modified?

[atsushi421]

@atsushi421 Upon verification, I believe the remaining Ready likely refers to the Ready from the Future trait's Poll method. For example, in preemptive.pml, since poll_result == Ready, I interpreted this as indicating Poll::Ready rather than Ready as a task state. Since the Poll method relies on Rust's built-in functionality, I considered it outside the scope of this change. Should this also be modified?

Oh, sorry. It's my falut.