From 8983a7cacd51d8f20f418eb130a167e9de9670d9 Mon Sep 17 00:00:00 2001 From: sgdxbc Date: Mon, 8 Jul 2024 11:59:47 +0800 Subject: [PATCH] Optimize model checker --- examples/unreplicated-check.rs | 34 +++------- src/model/search.rs | 109 +++++++++++++++------------------ 2 files changed, 57 insertions(+), 86 deletions(-) diff --git a/examples/unreplicated-check.rs b/examples/unreplicated-check.rs index 959abfad..02ce5b69 100644 --- a/examples/unreplicated-check.rs +++ b/examples/unreplicated-check.rs @@ -48,12 +48,7 @@ fn main() -> anyhow::Result<()> { prune: |_: &_| false, max_depth: None, }; - let result = breadth_first::<_, State<_>, _, _, _>( - state.clone(), - settings.clone(), - 1.try_into().unwrap(), - None, - )?; + let result = breadth_first(state.clone(), settings.clone(), 1.try_into().unwrap(), None)?; println!("{result:?}"); let settings = Settings { @@ -62,8 +57,7 @@ fn main() -> anyhow::Result<()> { prune: settings.goal, max_depth: None, }; - let result = - breadth_first::<_, State<_>, _, _, _>(state, settings, 1.try_into().unwrap(), None)?; + let result = breadth_first(state, settings, 1.try_into().unwrap(), None)?; println!("{result:?}"); println!("* Multi-client different keys"); @@ -89,12 +83,7 @@ fn main() -> anyhow::Result<()> { prune: |_: &_| false, max_depth: None, }; - let result = breadth_first::<_, State<_>, _, _, _>( - state.clone(), - settings.clone(), - 1.try_into().unwrap(), - None, - )?; + let result = breadth_first(state.clone(), settings.clone(), 1.try_into().unwrap(), None)?; println!("{result:?}"); let settings = Settings { @@ -103,8 +92,7 @@ fn main() -> anyhow::Result<()> { prune: settings.goal, max_depth: None, }; - let result = - breadth_first::<_, State<_>, _, _, _>(state, settings, 1.try_into().unwrap(), None)?; + let result = breadth_first(state, settings, 1.try_into().unwrap(), None)?; println!("{result:?}"); println!("* Multi-client same key"); @@ -158,12 +146,7 @@ fn main() -> anyhow::Result<()> { prune: |_: &_| false, max_depth: None, }; - let result = breadth_first::<_, State<_>, _, _, _>( - state.clone(), - settings.clone(), - 1.try_into().unwrap(), - None, - )?; + let result = breadth_first(state.clone(), settings.clone(), 1.try_into().unwrap(), None)?; println!("{result:?}"); let settings = Settings { @@ -172,8 +155,7 @@ fn main() -> anyhow::Result<()> { prune: settings.goal, max_depth: None, }; - let result = - breadth_first::<_, State<_>, _, _, _>(state, settings, 1.try_into().unwrap(), None)?; + let result = breadth_first(state, settings, 1.try_into().unwrap(), None)?; println!("{result:?}"); println!("* Infinite workload searches (with 2 clients)"); @@ -187,7 +169,7 @@ fn main() -> anyhow::Result<()> { prune: |_: &_| false, max_depth: None, }; - let result = breadth_first::<_, State<_>, _, _, _>( + let result = breadth_first( state.clone(), settings.clone(), available_parallelism()?, @@ -196,7 +178,7 @@ fn main() -> anyhow::Result<()> { )?; println!("{result:?}"); settings.max_depth = Some(1000.try_into().unwrap()); - let result = random_depth_first::<_, State<_>, _, _, _>( + let result = random_depth_first( state, settings, available_parallelism()?, diff --git a/src/model/search.rs b/src/model/search.rs index e6046352..e2f45cd5 100644 --- a/src/model/search.rs +++ b/src/model/search.rs @@ -5,7 +5,7 @@ use std::{ hash::{BuildHasherDefault, Hash}, iter::repeat, num::NonZeroUsize, - panic::{catch_unwind, AssertUnwindSafe, UnwindSafe}, + panic::{catch_unwind, AssertUnwindSafe}, sync::{ atomic::{AtomicBool, AtomicU32, AtomicUsize, Ordering::SeqCst}, Arc, Barrier, Condvar, Mutex, @@ -38,15 +38,15 @@ pub struct Settings { pub max_depth: Option, } -pub enum SearchResult { - Err(Vec<(E, T)>, E, anyhow::Error), - InvariantViolation(Vec<(E, T)>, anyhow::Error), +pub enum SearchResult { + Err(Vec<(E, S)>, E, anyhow::Error), + InvariantViolation(Vec<(E, S)>, anyhow::Error), GoalFound(S), SpaceExhausted, Timeout, } -impl Debug for SearchResult { +impl Debug for SearchResult { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { Self::Err(_, _, err) => write!(f, "Err({err})"), @@ -58,7 +58,7 @@ impl Debug for SearchResult { } } -impl Display for SearchResult { +impl Display for SearchResult { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { Self::Err(trace, event, err) => { @@ -81,26 +81,15 @@ impl Display for SearchResult { } } -// historically there are two state types: the original state `S` and the "dry" state `T` -// the rationale is that it could be unreasonable to ask `S`, which may contain moving parts (i.e. -// `impl SendEvent<_>`s) that prepared for interacting with the real world, to be as "pure" as -// `impl Eq + Hash` -// the solution has been improved into a `derive_where`-based opt-out approach, which means `S` may -// be `impl Eq + Hash` on its own and probably `T = S` -// the interface is left in the form of distinct `S` and `T` in case of design rollback, and also -// the code is more readable in current form, where `S` represents the constantly involving states -// and `T` represents explored achieved states (which is still called "dry state" below) -// the `S: Into` should become no-op and zero cost, hopefully -pub fn breadth_first( +pub fn breadth_first( initial_state: S, settings: Settings, num_worker: NonZeroUsize, max_duration: impl Into>, -) -> anyhow::Result> +) -> anyhow::Result> where - S: State + Clone + Into + Send + UnwindSafe + 'static, - S::Event: Clone + Send + Sync + UnwindSafe, - T: Clone + Eq + Hash + Send + Sync + 'static, + S: State + Clone + Eq + Hash + Send + Sync + 'static, + S::Event: Clone + Send + Sync, I: Fn(&S) -> anyhow::Result<()> + Clone + Send + 'static, G: Fn(&S) -> bool + Clone + Send + 'static, P: Fn(&S) -> bool + Clone + Send + 'static, @@ -114,11 +103,11 @@ where let depth_barrier = Arc::new(Barrier::new(num_worker.get())); let search_finished = Arc::new((Mutex::new(None), Condvar::new(), AtomicBool::new(false))); - let initial_dry_state = Arc::new(initial_state.clone().into()); - queue.push((initial_state, initial_dry_state.clone())); + let initial_state = Arc::new(initial_state); + queue.push(initial_state.clone()); discovered .insert( - initial_dry_state, + initial_state, StateInfo { prev: None, depth: 0, @@ -160,36 +149,35 @@ where }, search_finished, )?; - println!("search internal done"); + // println!("search internal done"); let Some(result) = result else { return Ok(SearchResult::Timeout); }; let result = match result { SearchWorkerResult::Error(state, event, err) => { - SearchResult::Err(trace(&discovered, state.into()), event, err) + SearchResult::Err(trace(&discovered, state), event, err) } SearchWorkerResult::InvariantViolation(state, err) => { - SearchResult::InvariantViolation(trace(&discovered, state.into()), err) + SearchResult::InvariantViolation(trace(&discovered, state), err) } SearchWorkerResult::GoalFound(state) => SearchResult::GoalFound(state), SearchWorkerResult::SpaceExhausted => SearchResult::SpaceExhausted, }; - println!("search exit"); + // println!("search exit"); Ok(result) } // the discussion above on `S` and `T` also applies here -pub fn random_depth_first( +pub fn random_depth_first( initial_state: S, settings: Settings, num_worker: NonZeroUsize, max_duration: impl Into>, -) -> anyhow::Result> +) -> anyhow::Result> where - S: State + Clone + Into + Send + UnwindSafe + 'static, - S::Event: Clone + Send + Sync + UnwindSafe, - T: Eq + Hash + Send + Sync + 'static, + S: State + Clone + Eq + Hash + Send + Sync + 'static, + S::Event: Clone + Send + Sync, I: Fn(&S) -> anyhow::Result<()> + Clone + Send + 'static, G: Fn(&S) -> bool + Clone + Send + 'static, P: Fn(&S) -> bool + Clone + Send + 'static, @@ -310,20 +298,20 @@ fn status_worker(status: impl Fn(Duration) -> String, search_finished: Search } #[derive_where(Clone; E)] -struct StateInfo { - prev: Option<(E, Arc)>, +struct StateInfo { + prev: Option<(E, Arc)>, #[allow(unused)] depth: usize, // to assert trace correctness? } -type Discovered = HashMap, StateInfo, BuildHasherDefault>; +type Discovered = HashMap, StateInfo, BuildHasherDefault>; -fn trace(discovered: &Discovered, target: T) -> Vec<(E, T)> { +fn trace(discovered: &Discovered, target: S) -> Vec<(E, S)> { let info = discovered.get(&target).unwrap(); let Some((prev_event, prev_state)) = &info.get().prev else { return Vec::new(); }; - let prev_state = T::clone(prev_state); + let prev_state = S::clone(prev_state); let prev_event = prev_event.clone(); drop(info); let mut trace = trace(discovered, prev_state); @@ -338,18 +326,17 @@ enum SearchWorkerResult { SpaceExhausted, } -fn breath_first_worker( +fn breath_first_worker( settings: Settings, - discovered: Arc>, - mut queue: Arc)>>, - mut pushing_queue: Arc)>>, + discovered: Arc>, + mut queue: Arc>>, + mut pushing_queue: Arc>>, depth: Arc, depth_barrier: Arc, search_finished: SearchFinished>, ) where - S: State + Clone + Into + UnwindSafe, - S::Event: Clone + UnwindSafe, - T: Eq + Hash, + S: State + Clone + Eq + Hash + Send + Sync + 'static, + S::Event: Clone + Send + Sync, I: Fn(&S) -> anyhow::Result<()>, G: Fn(&S) -> bool, P: Fn(&S) -> bool, @@ -363,24 +350,24 @@ fn breath_first_worker( }; for local_depth in 0.. { // println!("start depth {local_depth}"); - 'depth: while let Some((state, dry_state)) = queue.pop() { + 'depth: while let Some(state) = queue.pop() { // TODO check initial state // println!("check events"); for event in state.events() { // println!("step {event:?}"); - let mut next_state = state.clone(); + let mut next_state = S::clone(&state); if let Err(err) = step(&mut next_state, event.clone()) { - search_finish(SearchWorkerResult::Error(state, event, err)); + search_finish(SearchWorkerResult::Error(S::clone(&state), event, err)); break 'depth; } - let next_dry_state = Arc::new(next_state.clone().into()); + let next_state = Arc::new(next_state); // do not replace a previously-found state, which may be reached with a shorter // trace from initial state let mut inserted = false; - discovered.entry(next_dry_state.clone()).or_insert_with(|| { + discovered.entry(next_state.clone()).or_insert_with(|| { inserted = true; StateInfo { - prev: Some((event, dry_state.clone())), + prev: Some((event, state.clone())), depth: local_depth + 1, } }); @@ -390,18 +377,21 @@ fn breath_first_worker( } // println!("check invariant"); if let Err(err) = (settings.invariant)(&next_state) { - search_finish(SearchWorkerResult::InvariantViolation(next_state, err)); + search_finish(SearchWorkerResult::InvariantViolation( + S::clone(&next_state), + err, + )); break 'depth; } // println!("check goal"); if (settings.goal)(&next_state) { - search_finish(SearchWorkerResult::GoalFound(next_state)); + search_finish(SearchWorkerResult::GoalFound(S::clone(&next_state))); break 'depth; } if Some(local_depth + 1) != settings.max_depth.map(Into::into) && !(settings.prune)(&next_state) { - pushing_queue.push((next_state, next_dry_state)) + pushing_queue.push(next_state) } } if search_finished.2.load(SeqCst) { @@ -438,16 +428,15 @@ fn breath_first_worker( // println!("worker exit"); } -fn random_depth_first_worker( +fn random_depth_first_worker( settings: Settings, initial_state: S, num_probe: Arc, num_state: Arc, - search_finished: SearchFinished>, + search_finished: SearchFinished>, ) where - S: State + Clone + Into + UnwindSafe, - S::Event: Clone + UnwindSafe, - T: Eq + Hash, + S: State + Clone, + S::Event: Clone, I: Fn(&S) -> anyhow::Result<()>, G: Fn(&S) -> bool, P: Fn(&S) -> bool, @@ -472,7 +461,7 @@ fn random_depth_first_worker( break; } num_state.fetch_add(1, SeqCst); - trace.push((event, state.clone().into())); + trace.push((event, state.clone())); if let Err(err) = (settings.invariant)(&state) { search_finish(SearchResult::InvariantViolation(trace, err)); break;