Skip to content

Comments

fix(scheduler): solve inter-scheduler priority inversion#655

Merged
ytakano merged 8 commits intomainfrom
solve_inter_scheduler_priority_inversion
Oct 3, 2025
Merged

fix(scheduler): solve inter-scheduler priority inversion#655
ytakano merged 8 commits intomainfrom
solve_inter_scheduler_priority_inversion

Conversation

@atsushi421
Copy link
Contributor

@atsushi421 atsushi421 commented Sep 24, 2025

Description

This solves the inter-scheduler priority inversion. This also changes the promela model and verifies it.

Related links

How was this PR tested?

  • Model checking. Please see README.md for detail.
  • Test application (test_multi_prioritized_scheduler). The log is as follows.
[         3804 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 1 started. sched_type = PrioritizedRR(0)
[         3811 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 2 started. sched_type = GEDF(1000)
[         3820 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 3 started. sched_type = PrioritizedFIFO(0)
[         3836 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 5 started. sched_type = GEDF(1000)
[         3852 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 6 started. sched_type = PrioritizedFIFO(0)
[         3852 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 8 started. sched_type = GEDF(1000)
[         3853 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 4 started. sched_type = PrioritizedRR(0)
[         3854 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 7 started. sched_type = PrioritizedRR(0)
[         3885 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 9 started. sched_type = PrioritizedFIFO(0)
[         3916 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 11 started. sched_type = GEDF(1000)
[         4044 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 12 started. sched_type = PrioritizedFIFO(0)
[         4124 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 14 started. sched_type = GEDF(1000)
[         4188 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 15 started. sched_type = PrioritizedFIFO(0)
[         4620 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 2 started. sched_type = GEDF(500)
[         4636 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 3 started. sched_type = PrioritizedFIFO(1)
[         4732 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 2 finished. sched_type = GEDF(500)
[         4764 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 5 started. sched_type = GEDF(500)
[         4764 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 3 finished. sched_type = PrioritizedFIFO(1)
[         4812 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 6 started. sched_type = PrioritizedFIFO(1)
[         4892 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 8 finished. sched_type = GEDF(1000)
[         4908 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 5 finished. sched_type = GEDF(1000)
[         4924 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 5 finished. sched_type = GEDF(500)
[         4924 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 6 finished. sched_type = PrioritizedFIFO(0)
[         4940 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 3 finished. sched_type = PrioritizedFIFO(0)
[         4940 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 1 started. sched_type = PrioritizedRR(1)
[         4972 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 8 started. sched_type = GEDF(500)
[         4972 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 11 finished. sched_type = GEDF(1000)
[         4988 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 6 finished. sched_type = PrioritizedFIFO(1)
[         5004 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 7 started. sched_type = PrioritizedRR(1)
[         5004 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 2 finished. sched_type = GEDF(1000)
[         5004 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 9 started. sched_type = PrioritizedFIFO(1)
[         5004 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 9 finished. sched_type = PrioritizedFIFO(0)
[         5004 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 4 started. sched_type = PrioritizedRR(1)
[         5005 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 10 started. sched_type = PrioritizedRR(1)
[         5036 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 11 started. sched_type = GEDF(500)
[         5052 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 12 started. sched_type = PrioritizedFIFO(1)
[         5100 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 13 started. sched_type = PrioritizedRR(1)
[         5100 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 14 started. sched_type = GEDF(500)
[         5100 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 8 finished. sched_type = GEDF(500)
[         5132 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 1 finished. sched_type = PrioritizedRR(1)
[         5132 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 9 finished. sched_type = PrioritizedFIFO(1)
[         5132 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 14 finished. sched_type = GEDF(1000)
[         5133 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:43: high priority task 15 started. sched_type = PrioritizedFIFO(1)
[         5148 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 10 finished. sched_type = PrioritizedRR(1)
[         5180 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 12 finished. sched_type = PrioritizedFIFO(1)
[         5196 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 15 finished. sched_type = PrioritizedFIFO(0)
[         5212 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 11 finished. sched_type = GEDF(500)
[         5212 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 4 finished. sched_type = PrioritizedRR(0)
[         5212 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 12 finished. sched_type = PrioritizedFIFO(0)
[         5212 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 7 finished. sched_type = PrioritizedRR(0)
[         5292 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 4 finished. sched_type = PrioritizedRR(1)
[         5292 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 13 finished. sched_type = PrioritizedRR(1)
[         5292 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 15 finished. sched_type = PrioritizedFIFO(1)
[         5292 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 13 started. sched_type = PrioritizedRR(0)
[         5292 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 1 finished. sched_type = PrioritizedRR(0)
[         5293 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 14 finished. sched_type = GEDF(500)
[         5293 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:22: low priority task 10 started. sched_type = PrioritizedRR(0)
[         5308 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:45: high priority task 7 finished. sched_type = PrioritizedRR(1)
[         6412 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 13 finished. sched_type = PrioritizedRR(0)
[         6413 DEBUG] /home/atsushi/awkernel/applications/tests/test_multi_prioritized_scheduler/src/lib.rs:24: low priority task 10 finished. sched_type = PrioritizedRR(0)

Notes for reviewers

The Mutex for each scheduler's data is unnecessary for now, such as

pub static SCHEDULER: PrioritizedFIFOScheduler = PrioritizedFIFOScheduler {
    data: Mutex::new(None),  // <- this
    priority: get_priority(SchedulerType::PrioritizedFIFO(0)),
};

However, RefCell cannot be used for a field in a static object. Therefore, it remains. I would appreciate your comments on this if you have a better idea.

Signed-off-by: atsushi421 <atsushi.yano.2@tier4.jp>
@atsushi421 atsushi421 marked this pull request as ready for review September 24, 2025 20:15
@atsushi421 atsushi421 requested a review from ytakano September 24, 2025 23:59
nokosaaan and others added 2 commits September 26, 2025 17:45
* test: for develop #1

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* test: for develop #2

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* test: whether source_nodes or others & modify DAG struct  #3

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* test: add else process for initial period #4

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* test: absolute deadline setting #5

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: absolute deadline setting #6

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix absolute deadline #7

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* test: change gedf.rs #8

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* test: change gedf.rs #9

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: delete unnecessary code

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: modify get_node_info and etc

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: change function name

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: organizing comments & modify else handling

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: remove unused methods

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: change PRIORITY_LIST & change dag.rs

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: change gedf.rs & task.rs

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: avoid deadlock for GEDFNoArg

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: change spawn logic

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: delete GEDFNoArg

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check cargo fmt

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: adjusting the number of arguments

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check cargo fmt 2

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: improper variable usage in panic! macros

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check doctest

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check doctest 2

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check doctest 3

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check doctest 4

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check doctest 5

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check doctest 6

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check doctest 7

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check doctest 8

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check cargo fmt 3

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check doctest 9

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check doctest 10

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check doctest 11

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: fix unnecessary imports

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: reset the LOG_ENABLE flag to its original state

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: delete unnecessary functions

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: delete unnecessary functions 2

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: delete unnecessary functions 3

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: implement gedf

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check cargo fmt 4

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: refactored the nested sections using helper functions

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: reduced nested structure using early return

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: adding a function and code optimization

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: check cargo fmt 5

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: add a comment in dag.rs

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: format! error

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: To resolve the build error, I used unwrap_or_else instead of expect.

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: delete unnecessary import

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: delete semicolon

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: panic! 2

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: unify the name index to id

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: consolidated the duplicate processing and add a comment

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

* fix: solve let binding

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>

---------

Signed-off-by: nokosaaan <nishimura.r.019@ms.saitama-u.ac.jp>
@ytakano ytakano merged commit b4f90de into main Oct 3, 2025
1 check passed
@ytakano ytakano deleted the solve_inter_scheduler_priority_inversion branch October 3, 2025 06:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants