Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add in and out degree for states #45

Draft
wants to merge 10 commits into
base: master
Choose a base branch
from
Draft

Add in and out degree for states #45

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
af28419
Add degree calculations
jeffa5 Feb 13, 2023
272cfb9
Add basic in-degree
jeffa5 Feb 13, 2023
443617b
Fix tests
jeffa5 Feb 13, 2023
d9c0337
Track in_degree and out_degree in more detail
jeffa5 Feb 13, 2023
6eab61b
Update test
jeffa5 Feb 13, 2023
48210eb
Update comments
jeffa5 Feb 13, 2023
3d45939
Pre-filter next_states
jeffa5 Feb 13, 2023
c45e517
Fix average calculations and count out degree after filtering next
jeffa5 Feb 13, 2023
f1ee2ce
Fix average and track all actions in out degree
jeffa5 Feb 13, 2023
6dd8791
Fix test
jeffa5 Feb 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 17 additions & 5 deletions src/checker.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ mod rewrite_plan;
mod visitor;

use crate::report::{ReportData, ReportDiscovery, Reporter};
use crate::{Expectation, Model, Fingerprint};
use crate::{Expectation, Fingerprint, Model};
use std::collections::HashMap;
use std::fmt::{Debug, Display};
use std::hash::Hash;
Expand Down Expand Up @@ -274,6 +274,14 @@ pub trait Checker<M: Model> {
/// Indicates the maximum depth that has been explored.
fn max_depth(&self) -> usize;

/// List of out degree of each state.
/// The out degree is the number of actions generated by the state.
fn out_degrees(&self) -> Vec<usize>;

/// List of in degree of each state.
/// The in degree is the number of actions that lead into the state.
fn in_degrees(&self) -> Vec<usize>;

/// Returns a map from property name to corresponding "discovery" (indicated
/// by a [`Path`]).
fn discoveries(&self) -> HashMap<&'static str, Path<M::State, M::Action>>;
Expand Down Expand Up @@ -308,6 +316,8 @@ pub trait Checker<M: Model> {
total_states: self.state_count(),
unique_states: self.unique_state_count(),
max_depth: self.max_depth(),
out_degrees: self.out_degrees(),
in_degrees: self.in_degrees(),
duration: method_start.elapsed(),
done: false,
});
Expand All @@ -317,6 +327,8 @@ pub trait Checker<M: Model> {
total_states: self.state_count(),
unique_states: self.unique_state_count(),
max_depth: self.max_depth(),
out_degrees: self.out_degrees(),
in_degrees: self.in_degrees(),
duration: method_start.elapsed(),
done: true,
});
Expand Down Expand Up @@ -609,8 +621,8 @@ mod test_report {
assert!(
output.starts_with(
"\
Checking. states=1, unique=1, depth=0\n\
Done. states=15, unique=12, depth=4, sec="
Checking. states=1, unique=1, depth=0, avg out degree=0, avg in degree=0\n\
Done. states=15, unique=12, depth=4, avg out degree=1.1666666666666667, avg in degree=1.1666666666666667, sec="
),
"Output did not start as expected (see test). output={:?}`",
output
Expand All @@ -637,8 +649,8 @@ mod test_report {
assert!(
output.starts_with(
"\
Checking. states=1, unique=1, depth=0\n\
Done. states=55, unique=55, depth=28, sec="
Checking. states=1, unique=1, depth=0, avg out degree=0, avg in degree=0\n\
Done. states=55, unique=55, depth=28, avg out degree=0.9818181818181818, avg in degree=0.9818181818181818, sec="
),
"Output did not start as expected (see test). output={:?}`",
output
Expand Down
72 changes: 54 additions & 18 deletions src/checker/bfs.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,13 @@ use std::sync::atomic::{AtomicUsize, Ordering};
// While this file is currently quite similar to dfs.rs, a refactoring to lift shared
// behavior is being postponed until DPOR is implemented.

#[derive(Default)]
struct NodeData {
in_degree: usize,
out_degree: usize,
parent_fingerprint: Option<Fingerprint>,
}
Comment on lines +19 to +23
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One thing impacting performance is the change from storing Option<Fingerprint> in the map (which encodes to a single u64 as Fingerprint is a NonZeroU64 enabling a memory layout optimization) to this new structure that cannot encode as efficiently.

I don't know whether it would help or hurt performance, but perhaps adopting different maps along the lines of https://en.wikipedia.org/wiki/Data-oriented_design is worth exploring.


pub(crate) struct BfsChecker<M: Model> {
// Immutable state.
model: Arc<M>,
Expand All @@ -25,7 +32,7 @@ pub(crate) struct BfsChecker<M: Model> {
job_market: Arc<Mutex<JobMarket<M::State>>>,
state_count: Arc<AtomicUsize>,
max_depth: Arc<AtomicUsize>,
generated: Arc<DashMap<Fingerprint, Option<Fingerprint>, BuildHasherDefault<NoHashHasher<u64>>>>,
generated: Arc<DashMap<Fingerprint, NodeData, BuildHasherDefault<NoHashHasher<u64>>>>,
discoveries: Arc<DashMap<&'static str, Fingerprint>>,
}
struct JobMarket<State> { wait_count: usize, jobs: Vec<Job<State>> }
Expand All @@ -50,7 +57,7 @@ where M: Model + Send + Sync + 'static,
let max_depth = Arc::new(AtomicUsize::new(0));
let generated = Arc::new({
let generated = DashMap::default();
for s in &init_states { generated.insert(fingerprint(s), None); }
for s in &init_states { generated.insert(fingerprint(s), NodeData::default()); }
generated
});
let ebits = {
Expand Down Expand Up @@ -176,7 +183,7 @@ where M: Model + Send + Sync + 'static,
fn check_block(
model: &M,
state_count: &AtomicUsize,
generated: &DashMap<Fingerprint, Option<Fingerprint>, BuildHasherDefault<NoHashHasher<u64>>>,
generated: &DashMap<Fingerprint, NodeData, BuildHasherDefault<NoHashHasher<u64>>>,
pending: &mut Job<M::State>,
discoveries: &DashMap<&'static str, Fingerprint>,
visitor: &Option<Box<dyn CheckerVisitor<M> + Send + Sync>>,
Expand Down Expand Up @@ -255,6 +262,11 @@ where M: Model + Send + Sync + 'static,
// Otherwise enqueue newly generated states (with related metadata).
let mut is_terminal = true;
model.actions(&state, &mut actions);
let generated_fingerprint = fingerprint(&state);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you reuse state_fp to avoid an extra fingerprint calculation here?

generated
.entry(generated_fingerprint)
.and_modify(|nd| nd.out_degree = actions.len());

let next_states = actions.drain(..).flat_map(|a| model.next_state(&state, a));
for next_state in next_states {
// Skip if outside boundary.
Expand All @@ -270,19 +282,29 @@ where M: Model + Send + Sync + 'static,
// that it holds in the path leading to the second visit -- another
// possible false-negative.
let next_fingerprint = fingerprint(&next_state);
if let Entry::Vacant(next_entry) = generated.entry(next_fingerprint) {
next_entry.insert(Some(state_fp));
} else {
// FIXME: arriving at an already-known state may be a loop (in which case it
// could, in a fancier implementation, be considered a terminal state for
// purposes of eventually-property checking) but it might also be a join in
// a DAG, which makes it non-terminal. These cases can be disambiguated (at
// some cost), but for now we just _don't_ treat them as terminal, and tell
// users they need to explicitly ensure model path-acyclicality when they're
// using eventually properties (using a boundary or empty actions or
// whatever).
is_terminal = false;
continue
match generated.entry(next_fingerprint) {
Entry::Occupied(mut o) => {
let nd = o.get_mut();
nd.in_degree += 1;
// FIXME: arriving at an already-known state may be a loop (in which case it
// could, in a fancier implementation, be considered a terminal state for
// purposes of eventually-property checking) but it might also be a join in
// a DAG, which makes it non-terminal. These cases can be disambiguated (at
// some cost), but for now we just _don't_ treat them as terminal, and tell
// users they need to explicitly ensure model path-acyclicality when they're
// using eventually properties (using a boundary or empty actions or
// whatever).
is_terminal = false;
continue
},
Entry::Vacant(v) => {
let nd = NodeData {
in_degree: 1,
out_degree: 0,
parent_fingerprint: Some(state_fp),
};
v.insert(nd);
},
}

// Otherwise further checking is applicable.
Expand Down Expand Up @@ -322,6 +344,20 @@ where M: Model,
self.max_depth.load(Ordering::Relaxed)
}

fn out_degrees(&self) -> Vec<usize>{
self.generated
.iter()
.map(|kv| kv.value().out_degree)
.collect()
}

fn in_degrees(&self) -> Vec<usize>{
self.generated
.iter()
.map(|kv| kv.value().in_degree)
.collect()
}

fn discoveries(&self) -> HashMap<&'static str, Path<M::State, M::Action>> {
self.discoveries.iter()
.map(|mapref| {
Expand Down Expand Up @@ -349,7 +385,7 @@ where M: Model,

fn reconstruct_path<M>(
model: &M,
generated: &DashMap<Fingerprint, Option<Fingerprint>, BuildHasherDefault<NoHashHasher<u64>>>,
generated: &DashMap<Fingerprint, NodeData, BuildHasherDefault<NoHashHasher<u64>>>,
fp: Fingerprint)
-> Path<M::State, M::Action>
where M: Model,
Expand All @@ -363,7 +399,7 @@ fn reconstruct_path<M>(
let mut fingerprints = VecDeque::new();
let mut next_fp = fp;
while let Some(source) = generated.get(&next_fp) {
match *source {
match source.parent_fingerprint {
Some(prev_fingerprint) => {
fingerprints.push_front(next_fp);
next_fp = prev_fingerprint;
Expand Down
Loading