From 8a60d560c6403b0e90aa7108b0aa714a53d249d9 Mon Sep 17 00:00:00 2001
From: Cookiebowser <lucas.doering@live.de>
Date: Wed, 11 May 2022 15:28:11 +0200
Subject: [PATCH] increased rust MC MT performance
decreased time it takes for a new task to spawn if a new state is available
---
benchmarks/model_checking/Rust/CAN_BUS_tlc.rs | 9 ++++-----
.../Rust/Cruise_finite1_deterministic_MC.rs | 9 ++++-----
benchmarks/model_checking/Rust/LandingGear_R6.rs | 9 ++++-----
benchmarks/model_checking/Rust/Lift_MC_Large.rs | 9 ++++-----
benchmarks/model_checking/Rust/QueensWithEvents_4.rs | 9 ++++-----
benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs | 9 ++++-----
.../Rust/Train_1_beebook_deterministic_MC_POR_v2.rs | 9 ++++-----
benchmarks/model_checking/Rust/nota_v2.rs | 9 ++++-----
benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs | 9 ++++-----
.../src/main/rust/btypes/src/brelation.rs | 10 ----------
.../de/hhu/stups/codegenerator/RustTemplate.stg | 9 ++++-----
11 files changed, 40 insertions(+), 60 deletions(-)
diff --git a/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs b/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs
index 564a59a40..66dffc50d 100644
--- a/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs
+++ b/benchmarks/model_checking/Rust/CAN_BUS_tlc.rs
@@ -1567,10 +1567,6 @@ impl CAN_BUS_tlc {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -1579,6 +1575,9 @@ impl CAN_BUS_tlc {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -1592,7 +1591,7 @@ impl CAN_BUS_tlc {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs b/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs
index 3c75c4370..54815c760 100644
--- a/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs
+++ b/benchmarks/model_checking/Rust/Cruise_finite1_deterministic_MC.rs
@@ -1876,10 +1876,6 @@ impl Cruise_finite1_deterministic_MC {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -1888,6 +1884,9 @@ impl Cruise_finite1_deterministic_MC {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -1901,7 +1900,7 @@ impl Cruise_finite1_deterministic_MC {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/LandingGear_R6.rs b/benchmarks/model_checking/Rust/LandingGear_R6.rs
index 60e94590d..016ef4e20 100644
--- a/benchmarks/model_checking/Rust/LandingGear_R6.rs
+++ b/benchmarks/model_checking/Rust/LandingGear_R6.rs
@@ -2283,10 +2283,6 @@ impl LandingGear_R6 {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -2295,6 +2291,9 @@ impl LandingGear_R6 {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -2308,7 +2307,7 @@ impl LandingGear_R6 {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/Lift_MC_Large.rs b/benchmarks/model_checking/Rust/Lift_MC_Large.rs
index 3e458e750..a6d2852de 100644
--- a/benchmarks/model_checking/Rust/Lift_MC_Large.rs
+++ b/benchmarks/model_checking/Rust/Lift_MC_Large.rs
@@ -270,10 +270,6 @@ impl Lift_MC_Large {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -282,6 +278,9 @@ impl Lift_MC_Large {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -295,7 +294,7 @@ impl Lift_MC_Large {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/QueensWithEvents_4.rs b/benchmarks/model_checking/Rust/QueensWithEvents_4.rs
index 7af2de3e3..868655dc9 100644
--- a/benchmarks/model_checking/Rust/QueensWithEvents_4.rs
+++ b/benchmarks/model_checking/Rust/QueensWithEvents_4.rs
@@ -356,10 +356,6 @@ impl QueensWithEvents_4 {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -368,6 +364,9 @@ impl QueensWithEvents_4 {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -381,7 +380,7 @@ impl QueensWithEvents_4 {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs b/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs
index 52284d908..f601ad28f 100644
--- a/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs
+++ b/benchmarks/model_checking/Rust/Train1_Lukas_POR_v3.rs
@@ -933,10 +933,6 @@ impl Train1_Lukas_POR_v3 {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -945,6 +941,9 @@ impl Train1_Lukas_POR_v3 {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -958,7 +957,7 @@ impl Train1_Lukas_POR_v3 {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/Train_1_beebook_deterministic_MC_POR_v2.rs b/benchmarks/model_checking/Rust/Train_1_beebook_deterministic_MC_POR_v2.rs
index b74c92f7d..a9a40e693 100644
--- a/benchmarks/model_checking/Rust/Train_1_beebook_deterministic_MC_POR_v2.rs
+++ b/benchmarks/model_checking/Rust/Train_1_beebook_deterministic_MC_POR_v2.rs
@@ -956,10 +956,6 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -968,6 +964,9 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -981,7 +980,7 @@ impl Train_1_beebook_deterministic_MC_POR_v2 {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/nota_v2.rs b/benchmarks/model_checking/Rust/nota_v2.rs
index e4be01aa8..a52fae3f4 100644
--- a/benchmarks/model_checking/Rust/nota_v2.rs
+++ b/benchmarks/model_checking/Rust/nota_v2.rs
@@ -1658,10 +1658,6 @@ impl nota_v2 {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -1670,6 +1666,9 @@ impl nota_v2 {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -1683,7 +1682,7 @@ impl nota_v2 {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs b/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
index 73fe42acf..66673ae8f 100644
--- a/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
+++ b/benchmarks/model_checking/Rust/sort_m2_data1000_MC.rs
@@ -442,10 +442,6 @@ impl sort_m2_data1000_MC {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -454,6 +450,9 @@ impl sort_m2_data1000_MC {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -467,7 +466,7 @@ impl sort_m2_data1000_MC {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
diff --git a/btypes_primitives/src/main/rust/btypes/src/brelation.rs b/btypes_primitives/src/main/rust/btypes/src/brelation.rs
index d1eab3dff..2b9cac648 100644
--- a/btypes_primitives/src/main/rust/btypes/src/brelation.rs
+++ b/btypes_primitives/src/main/rust/btypes/src/brelation.rs
@@ -84,19 +84,9 @@ impl<L: BObject, R: BObject> Hash for BRelation<L, R> {
if cache.is_none() {
let mut hasher = DefaultHasher::new();
self.map.hash(&mut hasher);
- /*
- let mut kvs = self.map.iter().collect::<Vec<(&L, &OrdSet<R>)>>();
- kvs.sort_by(|(k1, _v1), (k2, _v2)| k1.cmp(k2));
- for (key, value) in kvs {
- key.hash(&mut hasher);
- value.iter().for_each(|v| v.hash(&mut hasher));
- }
- */
hash = hasher.finish();
- //println!("BRelation: cache miss");
self.hash_cache.replace(Option::Some(hash));
} else {
- //println!("BRelation: cache hit");
hash = cache.unwrap();
}
hash.hash(state);
diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
index b0171b192..63e8c5dab 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
@@ -951,10 +951,6 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
let tx = tx.clone();
//println!("Thread {:?} spawning a thread", thread::current().id());
threadPool.execute(move|| {
- if !Self::checkInvariants(&state, last_op, is_caching) {
- let _ = tx.send(Err("INVARIANT VIOLATED"));
- }
-
let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
@@ -963,6 +959,9 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
+ if !Self::checkInvariants(&state, last_op, is_caching) {
+ let _ = tx.send(Err("INVARIANT VIOLATED"));
+ }
//println!("Thread {:?} done", thread::current().id());
let _ = tx.send(Ok(1));
});
@@ -976,7 +975,7 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
//println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
- match rx.recv_timeout(Duration::from_secs(1)) {
+ match rx.try_recv() {
Ok(val) => match val {
Ok(_) => finished_tasks += 1,
Err(msg) => { println!("{}", msg); stop_threads = true; },
--
GitLab