diff --git a/applications/tests/test_multi_prioritized_scheduler/Cargo.toml b/applications/tests/test_multi_prioritized_scheduler/Cargo.toml
new file mode 100644
index 000000000..07fbc1f3c
--- /dev/null
+++ b/applications/tests/test_multi_prioritized_scheduler/Cargo.toml
@@ -0,0 +1,15 @@
+[package]
+name = "test_multi_prioritized_scheduler"
+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_multi_prioritized_scheduler/src/lib.rs b/applications/tests/test_multi_prioritized_scheduler/src/lib.rs
new file mode 100644
index 000000000..349788884
--- /dev/null
+++ b/applications/tests/test_multi_prioritized_scheduler/src/lib.rs
@@ -0,0 +1,51 @@
+#![no_std]
+
+extern crate alloc;
+
+use awkernel_async_lib::{scheduler::SchedulerType, spawn};
+use awkernel_lib::{cpu::num_cpu, delay::wait_millisec};
+
+pub async fn run() {
+    wait_millisec(1000);
+    for i in 1..num_cpu() {
+        let sched_type = if i % 3 == 0 {
+            SchedulerType::PrioritizedFIFO(0)
+        } else if i % 3 == 1 {
+            SchedulerType::PrioritizedRR(0)
+        } else {
+            SchedulerType::GEDF(1000)
+        };
+
+        spawn(
+            "low_priority".into(),
+            async move {
+                log::debug!("low priority task {i} started. sched_type = {sched_type:?}");
+                wait_millisec(1000);
+                log::debug!("low priority task {i} finished. sched_type = {sched_type:?}");
+            },
+            sched_type,
+        )
+        .await;
+    }
+
+    for i in 1..num_cpu() {
+        let sched_type = if i % 3 == 0 {
+            SchedulerType::PrioritizedFIFO(1)
+        } else if i % 3 == 1 {
+            SchedulerType::PrioritizedRR(1)
+        } else {
+            SchedulerType::GEDF(500)
+        };
+
+        spawn(
+            "high_priority".into(),
+            async move {
+                log::debug!("high priority task {i} started. sched_type = {sched_type:?}");
+                wait_millisec(100);
+                log::debug!("high priority task {i} finished. sched_type = {sched_type:?}");
+            },
+            sched_type,
+        )
+        .await;
+    }
+}
diff --git a/awkernel_async_lib/src/scheduler.rs b/awkernel_async_lib/src/scheduler.rs
index b85f8b50a..9371dd7ea 100644
--- a/awkernel_async_lib/src/scheduler.rs
+++ b/awkernel_async_lib/src/scheduler.rs
@@ -116,6 +116,11 @@ static PRIORITY_LIST: [SchedulerType; 4] = [
     SchedulerType::Panicked,
 ];
 
+/// For exclusion execution of `wake_task` and `get_next` across all schedulers.
+/// In order to resolve priority inversion in multiple priority-based schedulers,
+/// the decision to preempt, dequeuing, enqueuing, and updating of RUNNING must be executed exclusively.
+static GLOBAL_WAKE_GET_MUTEX: Mutex<()> = Mutex::new(());
+
 pub(crate) trait Scheduler {
     /// Enqueue an executable task.
     /// The enqueued task will be taken by `get_next()`.
@@ -134,6 +139,9 @@ pub(crate) trait Scheduler {
 /// Get the next executable task.
 #[inline]
 pub(crate) fn get_next_task(execution_ensured: bool) -> Option<Arc<Task>> {
+    let mut node = MCSNode::new();
+    let _guard = GLOBAL_WAKE_GET_MUTEX.lock(&mut node);
+
     let task = PRIORITY_LIST
         .iter()
         .find_map(|&scheduler_type| get_scheduler(scheduler_type).get_next(execution_ensured));
diff --git a/awkernel_async_lib/src/scheduler/gedf.rs b/awkernel_async_lib/src/scheduler/gedf.rs
index 82bacdde2..09ec0d4f3 100644
--- a/awkernel_async_lib/src/scheduler/gedf.rs
+++ b/awkernel_async_lib/src/scheduler/gedf.rs
@@ -5,6 +5,7 @@ use core::cmp::max;
 use super::{Scheduler, SchedulerType, Task};
 use crate::{
     dag::{get_dag, get_dag_absolute_deadline, set_dag_absolute_deadline, to_node_index},
+    scheduler::GLOBAL_WAKE_GET_MUTEX,
     scheduler::{get_priority, peek_preemption_pending, push_preemption_pending},
     task::{
         get_task, get_tasks_running, set_current_task, set_need_preemption, DagInfo, State,
@@ -62,13 +63,6 @@ impl GEDFData {
 
 impl Scheduler for GEDFScheduler {
     fn wake_task(&self, task: Arc<Task>) {
-        let mut node = MCSNode::new();
-        // The reason for acquiring this lock before invoke_preemption() is to prevent priority inversion from occurring
-        // when invoke_preemption() is executed between the time the next task is determined and the RUNNING is updated
-        // within the scheduler's get_next().
-        let mut data = self.data.lock(&mut node);
-        let internal_data = data.get_or_insert_with(GEDFData::new);
-
         let (wake_time, absolute_deadline) = {
             let mut node_inner = MCSNode::new();
             let mut info = task.info.lock(&mut node_inner);
@@ -94,7 +88,12 @@ impl Scheduler for GEDFScheduler {
             }
         };
 
+        let mut node = MCSNode::new();
+        let _guard = GLOBAL_WAKE_GET_MUTEX.lock(&mut node);
         if !self.invoke_preemption(task.clone()) {
+            let mut node_inner = MCSNode::new();
+            let mut data = self.data.lock(&mut node_inner);
+            let internal_data = data.get_or_insert_with(GEDFData::new);
             internal_data.queue.push(GEDFTask {
                 task: task.clone(),
                 absolute_deadline,
diff --git a/awkernel_async_lib/src/scheduler/prioritized_fifo.rs b/awkernel_async_lib/src/scheduler/prioritized_fifo.rs
index 2f387249f..da125cf3b 100644
--- a/awkernel_async_lib/src/scheduler/prioritized_fifo.rs
+++ b/awkernel_async_lib/src/scheduler/prioritized_fifo.rs
@@ -3,7 +3,7 @@
 use core::cmp::max;
 
 use super::{Scheduler, SchedulerType, Task};
-use crate::scheduler::{peek_preemption_pending, push_preemption_pending};
+use crate::scheduler::{peek_preemption_pending, push_preemption_pending, GLOBAL_WAKE_GET_MUTEX};
 use crate::task::{get_task, get_tasks_running, set_current_task, set_need_preemption};
 use crate::{scheduler::get_priority, task::State};
 use alloc::sync::Arc;
@@ -35,12 +35,6 @@ impl PrioritizedFIFOData {
 
 impl Scheduler for PrioritizedFIFOScheduler {
     fn wake_task(&self, task: Arc<Task>) {
-        let mut node = MCSNode::new();
-        // The reason for acquiring this lock before invoke_preemption() is to prevent priority inversion from occurring
-        // when invoke_preemption() is executed between the time the next task is determined and the RUNNING is updated
-        // within the scheduler's get_next().
-        let mut data = self.data.lock(&mut node);
-        let internal_data = data.get_or_insert_with(PrioritizedFIFOData::new);
         let priority = {
             let mut node_inner = MCSNode::new();
             let info = task.info.lock(&mut node_inner);
@@ -50,7 +44,12 @@ impl Scheduler for PrioritizedFIFOScheduler {
             }
         };
 
+        let mut node = MCSNode::new();
+        let _guard = GLOBAL_WAKE_GET_MUTEX.lock(&mut node);
         if !self.invoke_preemption(task.clone()) {
+            let mut node_inner = MCSNode::new();
+            let mut data = self.data.lock(&mut node_inner);
+            let internal_data = data.get_or_insert_with(PrioritizedFIFOData::new);
             internal_data.queue.push(
                 priority,
                 PrioritizedFIFOTask {
diff --git a/awkernel_async_lib/src/scheduler/prioritized_rr.rs b/awkernel_async_lib/src/scheduler/prioritized_rr.rs
index c109cea26..d06b3fe63 100644
--- a/awkernel_async_lib/src/scheduler/prioritized_rr.rs
+++ b/awkernel_async_lib/src/scheduler/prioritized_rr.rs
@@ -4,7 +4,10 @@ use core::cmp::max;
 
 use super::{Scheduler, SchedulerType, Task};
 use crate::{
-    scheduler::{get_next_task, get_priority, peek_preemption_pending, push_preemption_pending},
+    scheduler::{
+        get_next_task, get_priority, peek_preemption_pending, push_preemption_pending,
+        GLOBAL_WAKE_GET_MUTEX,
+    },
     task::{
         get_last_executed_by_task_id, get_task, get_tasks_running, set_current_task,
         set_need_preemption, State,
@@ -40,12 +43,6 @@ impl PrioritizedRRData {
 
 impl Scheduler for PrioritizedRRScheduler {
     fn wake_task(&self, task: Arc<Task>) {
-        let mut node = MCSNode::new();
-        // The reason for acquiring this lock before invoke_preemption() is to prevent priority inversion from occurring
-        // when invoke_preemption() is executed between the time the next task is determined and the RUNNING is updated
-        // within the scheduler's get_next().
-        let mut data = self.data.lock(&mut node);
-        let internal_data = data.get_or_insert_with(PrioritizedRRData::new);
         let priority = {
             let mut node_inner = MCSNode::new();
             let info = task.info.lock(&mut node_inner);
@@ -55,7 +52,12 @@ impl Scheduler for PrioritizedRRScheduler {
             }
         };
 
+        let mut node = MCSNode::new();
+        let _guard = GLOBAL_WAKE_GET_MUTEX.lock(&mut node);
         if !self.invoke_preemption_wake(task.clone()) {
+            let mut node_inner = MCSNode::new();
+            let mut data = self.data.lock(&mut node_inner);
+            let internal_data = data.get_or_insert_with(PrioritizedRRData::new);
             internal_data.queue.push(
                 priority,
                 PrioritizedRRTask {
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 d4d2171de..6a96dc29f 100644
--- a/specification/awkernel_async_lib/src/task/preemptive_spin/README.md
+++ b/specification/awkernel_async_lib/src/task/preemptive_spin/README.md
@@ -185,7 +185,7 @@ To keep the model less complex, please note the following abstractions compared
 - For priority comparison, we use the simple priority value (`TaskInfo.id`) as before, rather than `combine_priority`.
   - This is ensured by guaranteeing that tasks with larger ids are never assigned to scheduler types with higher priority.
 
-### Results
+### First Results (The errors are found)
 
 [Used Version](https://github.com/tier4/awkernel/commit/8ee41ca90485ed3360e4e4c0345d9882833be7cb)
 
@@ -306,3 +306,586 @@ spin: _spin_nvr.tmp:21, Error: assertion violated
 spin: text of failed assertion: assert(!(!((!(((((((((((((((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)))))
 spin: trail ends after 1632 steps
 ```
+
+### Results of Fixed Version
+
+[Used Version](https://github.com/tier4/awkernel/pull/655/commits/a536ecfa06e0225a3b688c9cf13a356249664eae)
+
+The Promela model was updated to solve inter-scheduler priority inversion by adding a new global mutex `lock_global_wake_get_mutex` to ensure atomic operations during critical scheduler interactions, i.e., `wake_task()` and `scheduler_get_next()`. There are no errors in the all verification.
+
+```
+===============================================================
+Verifying with LTL=ensure_priority and sched_type_pattern=0
+===============================================================
+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)))
+  the model contains 3 never claims: ensure_priority, eventually_prerequisites, eventually_terminate
+  only one claim is used in a verification run
+  choose which one with ./pan -a -N name (defaults to -N eventually_terminate)
+  or use e.g.: spin -search -ltl eventually_terminate mutex.pml
+pan: ltl formula ensure_priority
+Depth=    2521 States=    1e+06 Transitions= 1.95e+06 Memory=   199.926 t=     4.87 R=   2e+05
+...
+Depth=    2537 States= 1.51e+08 Transitions= 2.97e+08 Memory= 13056.271 t=      841 R=   2e+05
+
+(Spin Version 6.5.2 -- 6 December 2019)
+        + Partial Order Reduction
+        + Compression
+
+Full statespace search for:
+        never claim             + (ensure_priority)
+        assertion violations    + (if within scope of claim)
+        acceptance   cycles     + (fairness disabled)
+        invalid end states      - (disabled by never claim)
+
+State-vector 1216 byte, depth reached 2537, errors: 0
+1.5199774e+08 states, stored
+1.4726137e+08 states, matched
+2.9925911e+08 transitions (= stored+matched)
+ 64924427 atomic steps
+hash conflicts: 1.0527649e+08 (resolved)
+
+Stats on memory usage (in Megabytes):
+181485.341      equivalent memory usage for states (stored*(State-vector + overhead))
+11076.686       actual memory usage for states (compression: 6.10%)
+                state-vector as stored = 40 byte + 36 byte overhead
+ 2048.000       memory used for hash table (-w28)
+    1.831       memory used for DFS stack (-m30000)
+    1.410       memory lost to fragmentation
+13125.412       total actual memory usage
+
+
+nr of templates: [ 0:globals 1:chans 2:procs ]
+collapse counts: [ 0:2234872 2:12 3:10244 4:99926 5:107 8:1 ]
+
+pan: elapsed time 847 seconds
+pan: rate 179530.55 states/second
+
+===============================================================
+Verifying with LTL=eventually_prerequisites and sched_type_pattern=0
+===============================================================
+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)))
+  the model contains 3 never claims: ensure_priority, eventually_prerequisites, eventually_terminate
+  only one claim is used in a verification run
+  choose which one with ./pan -a -N name (defaults to -N eventually_terminate)
+  or use e.g.: spin -search -ltl eventually_terminate mutex.pml
+pan: ltl formula eventually_prerequisites
+Depth=    2399 States=    1e+06 Transitions= 2.36e+06 Memory=   166.548 t=     5.62 R=   2e+05
+...
+Depth=    2537 States= 3.52e+08 Transitions= 9.75e+08 Memory= 19733.899 t= 2.51e+03 R=   1e+05
+
+(Spin Version 6.5.2 -- 6 December 2019)
+        + Partial Order Reduction
+        + Compression
+
+Full statespace search for:
+        never claim             + (eventually_prerequisites)
+        assertion violations    + (if within scope of claim)
+        acceptance   cycles     + (fairness disabled)
+        invalid end states      - (disabled by never claim)
+
+State-vector 1216 byte, depth reached 2537, errors: 0
+2.5216786e+08 states, stored (3.52338e+08 visited)
+6.2338335e+08 states, matched
+9.7572132e+08 transitions (= visited+matched)
+1.9231417e+08 atomic steps
+hash conflicts: 2.239899e+08 (resolved)
+
+Stats on memory usage (in Megabytes):
+301088.483      equivalent memory usage for states (stored*(State-vector + overhead))
+17700.405       actual memory usage for states (compression: 5.88%)
+                state-vector as stored = 38 byte + 36 byte overhead
+ 2048.000       memory used for hash table (-w28)
+    1.831       memory used for DFS stack (-m30000)
+    1.384       memory lost to fragmentation
+19749.157       total actual memory usage
+
+
+nr of templates: [ 0:globals 1:chans 2:procs ]
+collapse counts: [ 0:2372787 2:12 3:10244 4:99926 5:107 7:2 ]
+
+pan: elapsed time 2.51e+03 seconds
+pan: rate 140471.63 states/second
+
+===============================================================
+Verifying with LTL=eventually_terminate and sched_type_pattern=0
+===============================================================
+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)))
+  the model contains 3 never claims: ensure_priority, eventually_prerequisites, eventually_terminate
+  only one claim is used in a verification run
+  choose which one with ./pan -a -N name (defaults to -N eventually_terminate)
+  or use e.g.: spin -search -ltl eventually_terminate mutex.pml
+pan: ltl formula eventually_terminate
+Depth=    2496 States=    1e+06 Transitions= 2.43e+06 Memory=   167.501 t=     5.79 R=   2e+05
+...
+Depth=    2512 States= 2.91e+08 Transitions= 7.17e+08 Memory= 12709.610 t=  1.8e+03 R=   2e+05
+
+(Spin Version 6.5.2 -- 6 December 2019)
+        + Partial Order Reduction
+        + Compression
+
+Full statespace search for:
+        never claim             + (eventually_terminate)
+        assertion violations    + (if within scope of claim)
+        acceptance   cycles     + (fairness disabled)
+        invalid end states      - (disabled by never claim)
+
+State-vector 1216 byte, depth reached 2512, errors: 0
+1.4578084e+08 states, stored (2.91562e+08 visited)
+4.2640196e+08 states, matched
+7.1796364e+08 transitions (= visited+matched)
+1.2395589e+08 atomic steps
+hash conflicts: 1.4005791e+08 (resolved)
+
+Stats on memory usage (in Megabytes):
+174062.359      equivalent memory usage for states (stored*(State-vector + overhead))
+10679.490       actual memory usage for states (compression: 6.14%)
+                state-vector as stored = 41 byte + 36 byte overhead
+ 2048.000       memory used for hash table (-w28)
+    1.831       memory used for DFS stack (-m30000)
+12728.684       total actual memory usage
+
+
+nr of templates: [ 0:globals 1:chans 2:procs ]
+collapse counts: [ 0:2326966 2:8 3:10244 4:97573 5:107 6:1 ]
+
+pan: elapsed time 1.8e+03 seconds
+pan: rate 161671.54 states/second
+
+===============================================================
+Verifying with LTL=ensure_priority and sched_type_pattern=1
+===============================================================
+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)))
+  the model contains 3 never claims: ensure_priority, eventually_prerequisites, eventually_terminate
+  only one claim is used in a verification run
+  choose which one with ./pan -a -N name (defaults to -N eventually_terminate)
+  or use e.g.: spin -search -ltl eventually_terminate mutex.pml
+pan: ltl formula ensure_priority
+Depth=    2584 States=    1e+06 Transitions= 1.95e+06 Memory=   199.926 t=     4.85 R=   2e+05
+...
+Depth=    2600 States=  1.6e+08 Transitions= 3.15e+08 Memory= 13661.377 t=      884 R=   2e+05
+
+(Spin Version 6.5.2 -- 6 December 2019)
+        + Partial Order Reduction
+        + Compression
+
+Full statespace search for:
+        never claim             + (ensure_priority)
+        assertion violations    + (if within scope of claim)
+        acceptance   cycles     + (fairness disabled)
+        invalid end states      - (disabled by never claim)
+
+State-vector 1216 byte, depth reached 2600, errors: 0
+1.6056036e+08 states, stored
+1.5560281e+08 states, matched
+3.1616317e+08 transitions (= stored+matched)
+ 67761969 atomic steps
+hash conflicts: 1.0781288e+08 (resolved)
+
+Stats on memory usage (in Megabytes):
+191709.111      equivalent memory usage for states (stored*(State-vector + overhead))
+11651.303       actual memory usage for states (compression: 6.08%)
+                state-vector as stored = 40 byte + 36 byte overhead
+ 2048.000       memory used for hash table (-w28)
+    1.831       memory used for DFS stack (-m30000)
+    1.445       memory lost to fragmentation
+13700.001       total actual memory usage
+
+
+nr of templates: [ 0:globals 1:chans 2:procs ]
+collapse counts: [ 0:2279607 2:12 3:10244 4:99926 5:107 8:1 ]
+
+pan: elapsed time 887 seconds
+pan: rate 180941.63 states/second
+
+===============================================================
+Verifying with LTL=eventually_prerequisites and sched_type_pattern=1
+===============================================================
+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)))
+  the model contains 3 never claims: ensure_priority, eventually_prerequisites, eventually_terminate
+  only one claim is used in a verification run
+  choose which one with ./pan -a -N name (defaults to -N eventually_terminate)
+  or use e.g.: spin -search -ltl eventually_terminate mutex.pml
+pan: ltl formula eventually_prerequisites
+Depth=    2462 States=    1e+06 Transitions= 2.36e+06 Memory=   166.071 t=     5.59 R=   2e+05
+...
+Depth=    2600 States= 3.69e+08 Transitions= 1.02e+09 Memory= 20566.933 t= 2.61e+03 R=   1e+05
+
+(Spin Version 6.5.2 -- 6 December 2019)
+        + Partial Order Reduction
+        + Compression
+
+Full statespace search for:
+        never claim             + (eventually_prerequisites)
+        assertion violations    + (if within scope of claim)
+        acceptance   cycles     + (fairness disabled)
+        invalid end states      - (disabled by never claim)
+
+State-vector 1216 byte, depth reached 2600, errors: 0
+2.6514649e+08 states, stored (3.69733e+08 visited)
+6.5238061e+08 states, matched
+1.0221132e+09 transitions (= visited+matched)
+1.9962294e+08 atomic steps
+hash conflicts: 2.3518003e+08 (resolved)
+
+Stats on memory usage (in Megabytes):
+316584.970      equivalent memory usage for states (stored*(State-vector + overhead))
+18558.696       actual memory usage for states (compression: 5.86%)
+                state-vector as stored = 37 byte + 36 byte overhead
+ 2048.000       memory used for hash table (-w28)
+    1.831       memory used for DFS stack (-m30000)
+    1.852       memory lost to fragmentation
+20606.987       total actual memory usage
+
+
+nr of templates: [ 0:globals 1:chans 2:procs ]
+collapse counts: [ 0:2385079 2:12 3:10244 4:99926 5:107 7:2 ]
+
+pan: elapsed time 2.61e+03 seconds
+pan: rate 141555.33 states/second
+
+===============================================================
+Verifying with LTL=eventually_terminate and sched_type_pattern=1
+===============================================================
+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)))
+  the model contains 3 never claims: ensure_priority, eventually_prerequisites, eventually_terminate
+  only one claim is used in a verification run
+  choose which one with ./pan -a -N name (defaults to -N eventually_terminate)
+  or use e.g.: spin -search -ltl eventually_terminate mutex.pml
+pan: ltl formula eventually_terminate
+Depth=    2559 States=    1e+06 Transitions= 2.43e+06 Memory=   167.501 t=      5.8 R=   2e+05
+...
+Depth=    2575 States= 3.08e+08 Transitions= 7.59e+08 Memory= 13280.861 t= 1.89e+03 R=   2e+05
+
+(Spin Version 6.5.2 -- 6 December 2019)
+        + Partial Order Reduction
+        + Compression
+
+Full statespace search for:
+        never claim             + (eventually_terminate)
+        assertion violations    + (if within scope of claim)
+        acceptance   cycles     + (fairness disabled)
+        invalid end states      - (disabled by never claim)
+
+State-vector 1216 byte, depth reached 2575, errors: 0
+1.5434346e+08 states, stored (3.08687e+08 visited)
+4.5164746e+08 states, matched
+7.6033438e+08 transitions (= visited+matched)
+1.2963097e+08 atomic steps
+hash conflicts: 1.474679e+08 (resolved)
+
+Stats on memory usage (in Megabytes):
+184286.129      equivalent memory usage for states (stored*(State-vector + overhead))
+11255.509       actual memory usage for states (compression: 6.11%)
+                state-vector as stored = 40 byte + 36 byte overhead
+ 2048.000       memory used for hash table (-w28)
+    1.831       memory used for DFS stack (-m30000)
+    1.424       memory lost to fragmentation
+13304.226       total actual memory usage
+
+
+nr of templates: [ 0:globals 1:chans 2:procs ]
+collapse counts: [ 0:2372745 2:8 3:10244 4:97573 5:107 6:1 ]
+
+pan: elapsed time 1.9e+03 seconds
+pan: rate 162877.42 states/second
+
+===============================================================
+Verifying with LTL=ensure_priority and sched_type_pattern=2
+===============================================================
+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)))
+  the model contains 3 never claims: ensure_priority, eventually_prerequisites, eventually_terminate
+  only one claim is used in a verification run
+  choose which one with ./pan -a -N name (defaults to -N eventually_terminate)
+  or use e.g.: spin -search -ltl eventually_terminate mutex.pml
+pan: ltl formula ensure_priority
+Depth=    2605 States=    1e+06 Transitions= 1.95e+06 Memory=   199.926 t=     4.85 R=   2e+05
+...
+Depth=    2621 States= 1.65e+08 Transitions= 3.25e+08 Memory= 13996.594 t=      914 R=   2e+05
+
+(Spin Version 6.5.2 -- 6 December 2019)
+        + Partial Order Reduction
+        + Compression
+
+Full statespace search for:
+        never claim             + (ensure_priority)
+        assertion violations    + (if within scope of claim)
+        acceptance   cycles     + (fairness disabled)
+        invalid end states      - (disabled by never claim)
+
+State-vector 1216 byte, depth reached 2621, errors: 0
+1.6590364e+08 states, stored
+1.6078225e+08 states, matched
+3.2668589e+08 transitions (= stored+matched)
+ 69309657 atomic steps
+hash conflicts: 1.1019065e+08 (resolved)
+
+Stats on memory usage (in Megabytes):
+198088.989      equivalent memory usage for states (stored*(State-vector + overhead))
+12009.880       actual memory usage for states (compression: 6.06%)
+                state-vector as stored = 40 byte + 36 byte overhead
+ 2048.000       memory used for hash table (-w28)
+    1.831       memory used for DFS stack (-m30000)
+    1.443       memory lost to fragmentation
+14058.583       total actual memory usage
+
+
+nr of templates: [ 0:globals 1:chans 2:procs ]
+collapse counts: [ 0:2303822 2:12 3:10244 4:99926 5:107 8:1 ]
+
+pan: elapsed time 919 seconds
+pan: rate 180477.17 states/second
+
+===============================================================
+Verifying with LTL=eventually_prerequisites and sched_type_pattern=2
+===============================================================
+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)))
+  the model contains 3 never claims: ensure_priority, eventually_prerequisites, eventually_terminate
+  only one claim is used in a verification run
+  choose which one with ./pan -a -N name (defaults to -N eventually_terminate)
+  or use e.g.: spin -search -ltl eventually_terminate mutex.pml
+pan: ltl formula eventually_prerequisites
+Depth=    2462 States=    1e+06 Transitions= 2.35e+06 Memory=   166.071 t=     5.62 R=   2e+05
+...
+Depth=    2621 States=  3.8e+08 Transitions= 1.05e+09 Memory= 21112.912 t= 2.71e+03 R=   1e+05
+
+(Spin Version 6.5.2 -- 6 December 2019)
+        + Partial Order Reduction
+        + Compression
+
+Full statespace search for:
+        never claim             + (eventually_prerequisites)
+        assertion violations    + (if within scope of claim)
+        acceptance   cycles     + (fairness disabled)
+        invalid end states      - (disabled by never claim)
+
+State-vector 1216 byte, depth reached 2621, errors: 0
+2.7328853e+08 states, stored (3.80673e+08 visited)
+6.7071401e+08 states, matched
+1.0513874e+09 transitions (= visited+matched)
+2.035583e+08 atomic steps
+hash conflicts: 2.4233126e+08 (resolved)
+
+Stats on memory usage (in Megabytes):
+326306.568      equivalent memory usage for states (stored*(State-vector + overhead))
+19099.799       actual memory usage for states (compression: 5.85%)
+                state-vector as stored = 37 byte + 36 byte overhead
+ 2048.000       memory used for hash table (-w28)
+    1.831       memory used for DFS stack (-m30000)
+    1.747       memory lost to fragmentation
+21148.198       total actual memory usage
+
+
+nr of templates: [ 0:globals 1:chans 2:procs ]
+collapse counts: [ 0:2398685 2:12 3:10244 4:99926 5:107 7:2 ]
+
+pan: elapsed time 2.71e+03 seconds
+pan: rate 140251.49 states/second
+
+===============================================================
+Verifying with LTL=eventually_terminate and sched_type_pattern=2
+===============================================================
+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)))
+  the model contains 3 never claims: ensure_priority, eventually_prerequisites, eventually_terminate
+  only one claim is used in a verification run
+  choose which one with ./pan -a -N name (defaults to -N eventually_terminate)
+  or use e.g.: spin -search -ltl eventually_terminate mutex.pml
+pan: ltl formula eventually_terminate
+Depth=    2514 States=    1e+06 Transitions= 2.42e+06 Memory=   167.025 t=     5.84 R=   2e+05
+...
+Depth=    2596 States= 3.19e+08 Transitions= 7.86e+08 Memory= 13650.887 t= 1.96e+03 R=   2e+05
+
+(Spin Version 6.5.2 -- 6 December 2019)
+        + Partial Order Reduction
+        + Compression
+
+Full statespace search for:
+        never claim             + (eventually_terminate)
+        assertion violations    + (if within scope of claim)
+        acceptance   cycles     + (fairness disabled)
+        invalid end states      - (disabled by never claim)
+
+State-vector 1216 byte, depth reached 2596, errors: 0
+1.5968674e+08 states, stored (3.19373e+08 visited)
+4.6734962e+08 states, matched
+7.867231e+08 transitions (= visited+matched)
+1.3272635e+08 atomic steps
+hash conflicts: 1.5217597e+08 (resolved)
+
+Stats on memory usage (in Megabytes):
+190666.007      equivalent memory usage for states (stored*(State-vector + overhead))
+11615.225       actual memory usage for states (compression: 6.09%)
+                state-vector as stored = 40 byte + 36 byte overhead
+ 2048.000       memory used for hash table (-w28)
+    1.831       memory used for DFS stack (-m30000)
+    1.607       memory lost to fragmentation
+13663.762       total actual memory usage
+
+
+nr of templates: [ 0:globals 1:chans 2:procs ]
+collapse counts: [ 0:2398642 2:8 3:10244 4:97573 5:107 6:1 ]
+
+pan: elapsed time 1.96e+03 seconds
+pan: rate 162755.49 states/second
+
+===============================================================
+Verifying with LTL=ensure_priority and sched_type_pattern=3
+===============================================================
+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)))
+  the model contains 3 never claims: ensure_priority, eventually_prerequisites, eventually_terminate
+  only one claim is used in a verification run
+  choose which one with ./pan -a -N name (defaults to -N eventually_terminate)
+  or use e.g.: spin -search -ltl eventually_terminate mutex.pml
+pan: ltl formula ensure_priority
+Depth=    2605 States=    1e+06 Transitions= 1.95e+06 Memory=   199.926 t=     4.86 R=   2e+05
+...
+Depth=    2621 States= 1.66e+08 Transitions= 3.27e+08 Memory= 14063.828 t=      922 R=   2e+05
+
+(Spin Version 6.5.2 -- 6 December 2019)
+        + Partial Order Reduction
+        + Compression
+
+Full statespace search for:
+        never claim             + (ensure_priority)
+        assertion violations    + (if within scope of claim)
+        acceptance   cycles     + (fairness disabled)
+        invalid end states      - (disabled by never claim)
+
+State-vector 1216 byte, depth reached 2621, errors: 0
+1.6659906e+08 states, stored
+1.6142545e+08 states, matched
+3.2802451e+08 transitions (= stored+matched)
+ 69507259 atomic steps
+hash conflicts: 1.1052438e+08 (resolved)
+
+Stats on memory usage (in Megabytes):
+198919.321      equivalent memory usage for states (stored*(State-vector + overhead))
+12056.346       actual memory usage for states (compression: 6.06%)
+                state-vector as stored = 40 byte + 36 byte overhead
+ 2048.000       memory used for hash table (-w28)
+    1.831       memory used for DFS stack (-m30000)
+    1.179       memory lost to fragmentation
+14105.313       total actual memory usage
+
+
+nr of templates: [ 0:globals 1:chans 2:procs ]
+collapse counts: [ 0:2308890 2:12 3:10244 4:99926 5:107 8:1 ]
+
+pan: elapsed time 926 seconds
+pan: rate 179976.73 states/second
+
+===============================================================
+Verifying with LTL=eventually_prerequisites and sched_type_pattern=3
+===============================================================
+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)))
+  the model contains 3 never claims: ensure_priority, eventually_prerequisites, eventually_terminate
+  only one claim is used in a verification run
+  choose which one with ./pan -a -N name (defaults to -N eventually_terminate)
+  or use e.g.: spin -search -ltl eventually_terminate mutex.pml
+pan: ltl formula eventually_prerequisites
+Depth=    2462 States=    1e+06 Transitions= 2.35e+06 Memory=   166.071 t=     5.61 R=   2e+05
+...
+Depth=    2621 States= 3.81e+08 Transitions= 1.05e+09 Memory= 21163.933 t=  2.7e+03 R=   1e+05
+
+(Spin Version 6.5.2 -- 6 December 2019)
+        + Partial Order Reduction
+        + Compression
+
+Full statespace search for:
+        never claim             + (eventually_prerequisites)
+        assertion violations    + (if within scope of claim)
+        acceptance   cycles     + (fairness disabled)
+        invalid end states      - (disabled by never claim)
+
+State-vector 1216 byte, depth reached 2621, errors: 0
+2.7420845e+08 states, stored (3.81818e+08 visited)
+6.7227963e+08 states, matched
+1.0540975e+09 transitions (= visited+matched)
+2.0391055e+08 atomic steps
+hash conflicts: 2.4299923e+08 (resolved)
+
+Stats on memory usage (in Megabytes):
+327404.953      equivalent memory usage for states (stored*(State-vector + overhead))
+19160.768       actual memory usage for states (compression: 5.85%)
+                state-vector as stored = 37 byte + 36 byte overhead
+ 2048.000       memory used for hash table (-w28)
+    1.831       memory used for DFS stack (-m30000)
+    1.681       memory lost to fragmentation
+21209.233       total actual memory usage
+
+
+nr of templates: [ 0:globals 1:chans 2:procs ]
+collapse counts: [ 0:2403040 2:12 3:10244 4:99926 5:107 7:2 ]
+
+pan: elapsed time 2.7e+03 seconds
+pan: rate 141177.15 states/second
+
+===============================================================
+Verifying with LTL=eventually_terminate and sched_type_pattern=3
+===============================================================
+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)))
+  the model contains 3 never claims: ensure_priority, eventually_prerequisites, eventually_terminate
+  only one claim is used in a verification run
+  choose which one with ./pan -a -N name (defaults to -N eventually_terminate)
+  or use e.g.: spin -search -ltl eventually_terminate mutex.pml
+pan: ltl formula eventually_terminate
+Depth=    2514 States=    1e+06 Transitions= 2.42e+06 Memory=   167.025 t=     5.76 R=   2e+05
+...
+Depth=    2596 States=  3.2e+08 Transitions= 7.88e+08 Memory= 13684.266 t= 1.97e+03 R=   2e+05
+
+(Spin Version 6.5.2 -- 6 December 2019)
+        + Partial Order Reduction
+        + Compression
+
+Full statespace search for:
+        never claim             + (eventually_terminate)
+        assertion violations    + (if within scope of claim)
+        acceptance   cycles     + (fairness disabled)
+        invalid end states      - (disabled by never claim)
+
+State-vector 1216 byte, depth reached 2596, errors: 0
+1.6038216e+08 states, stored (3.20764e+08 visited)
+4.6933144e+08 states, matched
+7.9009576e+08 transitions (= visited+matched)
+1.3312155e+08 atomic steps
+hash conflicts: 1.5295385e+08 (resolved)
+
+Stats on memory usage (in Megabytes):
+191496.338      equivalent memory usage for states (stored*(State-vector + overhead))
+11661.187       actual memory usage for states (compression: 6.09%)
+                state-vector as stored = 40 byte + 36 byte overhead
+ 2048.000       memory used for hash table (-w28)
+    1.831       memory used for DFS stack (-m30000)
+    1.316       memory lost to fragmentation
+13710.015       total actual memory usage
+
+
+nr of templates: [ 0:globals 1:chans 2:procs ]
+collapse counts: [ 0:2404383 2:8 3:10244 4:97573 5:107 6:1 ]
+
+pan: elapsed time 1.97e+03 seconds
+pan: rate  162512.7 states/second
+```
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 122caedea..397e5ea72 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
@@ -35,5 +35,6 @@ chan queue[SCHEDULER_TYPE_NUM] = [TASK_NUM] of { byte }// task_ids in ascending
 #include "mutex.pml"
 Mutex lock_info[TASK_NUM]
 Mutex lock_queue[SCHEDULER_TYPE_NUM]
+Mutex lock_global_wake_get_mutex
 
 #define BYTE_MAX 255
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 110de2ca1..dce3d2be4 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
@@ -34,7 +34,7 @@ inline update_running_lowest_priority() {
 	}
 }
 
-#define MAX_CONSECUTIVE_RUN_MAIN_LOOP 5
+#define MAX_CONSECUTIVE_RUN_MAIN_LOOP 2
 byte consecutive_run_main_loop[WORKER_NUM] = 0
 bool wait_for_weak_fairness[WORKER_NUM] = false
 chan resume_requests = [WORKER_NUM] of { byte }// tid that requested to resume execution.
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 25a5344f5..af53bd98f 100644
--- a/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml
+++ b/specification/awkernel_async_lib/src/task/preemptive_spin/preemptive.pml
@@ -82,19 +82,21 @@ inline invoke_preemption(tid,task,ret) {
 /* awkernel_async_lib::scheduler::fifo::PrioritizedFIFOScheduler::wake_task()*/ 
 inline wake_task(tid,task) {
 	bool preemption_invoked;
-	lock(tid,lock_queue[tasks[task].scheduler_type]);
+	lock(tid,lock_global_wake_get_mutex);
 	invoke_preemption(tid,task,preemption_invoked);
 	
 	if
 	:: !preemption_invoked -> 
+		lock(tid,lock_queue[tasks[task].scheduler_type]);
 		d_step{
 			printf("wake_task(): push to queue: tid = %d,task = %d\n",tid,task);
 			queue[tasks[task].scheduler_type]!!task
 		}
+		unlock(tid,lock_queue[tasks[task].scheduler_type]);
 	:: else
 	fi
 	
-	unlock(tid,lock_queue[tasks[task].scheduler_type]);
+	unlock(tid,lock_global_wake_get_mutex);
 	d_step {
 		assert(waking[task] > 0);
 		waking[task]--
@@ -167,16 +169,17 @@ inline get_next_each_scheduler(tid,ret,sched_type) {
 		}
 		
 		unlock(tid,lock_info[head]);
-		unlock(tid,lock_queue[sched_type]);
 		ret = head
 	:: else -> 
-		unlock(tid,lock_queue[sched_type]);
 		ret = - 1
 	fi
+
+	unlock(tid,lock_queue[sched_type]);
 }
 
 /* awkernel_async_lib::task::scheduler::get_next_task() */
 inline scheduler_get_next(tid,ret) {
+	lock(tid,lock_global_wake_get_mutex);
 	byte sched_i;
 	for (sched_i : 0 .. SCHEDULER_TYPE_NUM - 1) {
 		get_next_each_scheduler(tid,ret,sched_i);
@@ -185,6 +188,7 @@ inline scheduler_get_next(tid,ret) {
 		:: else
 		fi
 	}
+	unlock(tid,lock_global_wake_get_mutex);
 }
 
 /* awkernel_async_lib::task::preempt::get_next_task()*/ 
diff --git a/userland/Cargo.toml b/userland/Cargo.toml
index 96e582732..664ec35f3 100644
--- a/userland/Cargo.toml
+++ b/userland/Cargo.toml
@@ -38,6 +38,10 @@ optional = true
 path = "../applications/tests/test_prioritized_fifo"
 optional = true
 
+[dependencies.test_multi_prioritized_scheduler]
+path = "../applications/tests/test_multi_prioritized_scheduler"
+optional = true
+
 [dependencies.test_prioritized_rr]
 path = "../applications/tests/test_prioritized_rr"
 optional = true
diff --git a/userland/src/lib.rs b/userland/src/lib.rs
index 60123208c..01a66fe18 100644
--- a/userland/src/lib.rs
+++ b/userland/src/lib.rs
@@ -25,6 +25,9 @@ pub async fn main() -> Result<(), Cow<'static, str>> {
     #[cfg(feature = "test_prioritized_fifo")]
     test_prioritized_fifo::run().await; // test for prioritized_fifo
 
+    #[cfg(feature = "test_multi_prioritized_scheduler")]
+    test_multi_prioritized_scheduler::run().await; // test for multi prioritized scheduler
+
     #[cfg(feature = "test_prioritized_rr")]
     test_prioritized_rr::run().await; // test for prioritized_rr