Skip to content

Commit

Permalink
address review comments
Browse files Browse the repository at this point in the history
  • Loading branch information
@Schaeff
Schaeff committed Jan 15, 2025
1 parent 638ab7e commit feec718
Show file tree
Hide file tree
Showing 2 changed files with 65 additions and 37 deletions.
96 changes: 62 additions & 34 deletions backend/src/mock/bus_checker.rs
View file
Original file line number Diff line number Diff line change
@@ -1,23 +1,25 @@
use std::{cmp::Ordering, collections::BTreeMap, fmt};

use itertools::Itertools;
use powdr_ast::{
analyzed::{Analyzed, Identity, PhantomBusInteractionIdentity},
parsed::visitor::Children,
};
use powdr_executor_utils::expression_evaluator::ExpressionEvaluator;
use powdr_number::FieldElement;
use rayon::iter::{IntoParallelIterator, ParallelIterator};

use super::{localize, machine::Machine, unique_referenced_namespaces};

pub struct BusChecker<'a, F> {
connections: &'a [BusConnection<F>],
connections: &'a [BusInteraction<F>],
machines: &'a BTreeMap<String, Machine<'a, F>>,
}

pub struct Error<F> {
tuple: Vec<F>,
sends: BTreeMap<BusConnection<F>, usize>,
receives: BTreeMap<BusConnection<F>, usize>,
sends: BTreeMap<BusInteraction<F>, usize>,
receives: BTreeMap<BusInteraction<F>, usize>,
}

impl<F: fmt::Display> fmt::Display for Error<F> {
Expand All @@ -26,15 +28,10 @@ impl<F: fmt::Display> fmt::Display for Error<F> {
f,
"Bus interaction {} failed for tuple {}:",
self.tuple[0],
self.tuple
.iter()
.skip(1)
.map(|v| v.to_string())
.collect::<Vec<_>>()
.join(", ")
self.tuple.iter().skip(1).map(|v| v.to_string()).join(", ")
)?;
for (
BusConnection {
BusInteraction {
machine,
interaction,
},
Expand All @@ -46,7 +43,7 @@ impl<F: fmt::Display> fmt::Display for Error<F> {
writeln!(f, " in {machine}",)?;
}
for (
BusConnection {
BusInteraction {
machine,
interaction,
},
Expand All @@ -62,12 +59,12 @@ impl<F: fmt::Display> fmt::Display for Error<F> {
}

#[derive(PartialEq, PartialOrd, Eq, Ord, Clone)]
pub struct BusConnection<F> {
pub struct BusInteraction<F> {
pub machine: String,
pub interaction: PhantomBusInteractionIdentity<F>,
}

impl<F: FieldElement> BusConnection<F> {
impl<F: FieldElement> BusInteraction<F> {
/// Extracts all bus connections from the global PIL.
pub fn get_all(
global_pil: &Analyzed<F>,
Expand All @@ -85,10 +82,10 @@ impl<F: FieldElement> BusConnection<F> {
}
})
.map(|interaction| {
// Localize the interaction assuming a single namespace is accessed. TODO: This may break due to the latch.
// Localize the interaction assuming a single namespace is accessed.
let machine = unique_referenced_namespaces(&interaction).unwrap();
let interaction = localize(interaction, global_pil, &machine_to_pil[&machine]);
BusConnection {
BusInteraction {
machine,
interaction,
}
Expand All @@ -99,7 +96,7 @@ impl<F: FieldElement> BusConnection<F> {

impl<'a, F: FieldElement> BusChecker<'a, F> {
pub fn new(
connections: &'a [BusConnection<F>],
connections: &'a [BusInteraction<F>],
machines: &'a BTreeMap<String, Machine<'a, F>>,
) -> Self {
Self {
Expand All @@ -109,19 +106,19 @@ impl<'a, F: FieldElement> BusChecker<'a, F> {
}

pub fn check(&self) -> Result<(), Vec<Error<F>>> {
type BusState<'a, F> = BTreeMap<
Vec<F>,
(
BTreeMap<&'a BusConnection<F>, usize>,
BTreeMap<&'a BusConnection<F>, usize>,
),
>;
#[derive(Default)]
struct TupleState<'a, F> {
sends: BTreeMap<&'a BusInteraction<F>, usize>,
receives: BTreeMap<&'a BusInteraction<F>, usize>,
}

type BusState<'a, F> = BTreeMap<Vec<F>, TupleState<'a, F>>;

let bus_state: BusState<F> = self
.machines
.iter()
.into_par_iter()
.flat_map(|(name, machine)| {
(0..machine.size).flat_map(|row_id| {
(0..machine.size).into_par_iter().flat_map(|row_id| {
// create an evaluator for this row
let mut evaluator = ExpressionEvaluator::new(
machine.values.row(row_id),
Expand All @@ -148,40 +145,71 @@ impl<'a, F: FieldElement> BusChecker<'a, F> {

(bus_connection, tuple, multiplicity)
})
.collect::<Vec<_>>()
})
})
// fold the interactions from a row into a state
.fold(
Default::default(),
|mut counts, (bus_connection, tuple, multiplicity)| {
// update the counts
let (s, r) = counts.entry(tuple).or_default();

BusState::default,
|mut state, (bus_connection, tuple, multiplicity)| {
let abs = multiplicity.unsigned_abs() as usize;

match multiplicity.cmp(&0) {
// if the multiplicity is zero, we don't need to do anything
Ordering::Equal => {}
// if the multiplicity is positive, we send
Ordering::Greater => {
s.entry(bus_connection)
let TupleState { sends, .. } = state.entry(tuple).or_default();
sends
.entry(bus_connection)
.and_modify(|sends| *sends += abs)
.or_insert(abs);
}
// if the multiplicity is negative, we receive
Ordering::Less => {
r.entry(bus_connection)
let TupleState { receives, .. } = state.entry(tuple).or_default();
receives
.entry(bus_connection)
.and_modify(|receives| *receives += abs)
.or_insert(abs);
}
}

counts
state
},
)
// combine all the states to one
.reduce(
BusState::default,
|mut a, b| {
for (tuple, TupleState { sends, receives }) in b {
let TupleState {
sends: sends_a,
receives: receives_a,
} = a.entry(tuple).or_default();

for (bus_connection, count) in sends {
sends_a
.entry(bus_connection)
.and_modify(|sends| *sends += count)
.or_insert(count);
}

for (bus_connection, count) in receives {
receives_a
.entry(bus_connection)
.and_modify(|receives| *receives += count)
.or_insert(count);
}
}

a
},
);

let mut errors = vec![];

for (tuple, (sends, receives)) in bus_state {
for (tuple, TupleState { sends, receives }) in bus_state {
let send_count = sends.values().sum::<usize>();
let receive_count = receives.values().sum::<usize>();
if send_count != receive_count {
Expand Down
6 changes: 3 additions & 3 deletions backend/src/mock/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ use std::{
sync::Arc,
};

use bus_checker::{BusChecker, BusConnection};
use bus_checker::{BusChecker, BusInteraction};
use connection_constraint_checker::{Connection, ConnectionConstraintChecker};
use machine::Machine;
use polynomial_constraint_checker::PolynomialConstraintChecker;
Expand Down Expand Up @@ -50,7 +50,7 @@ impl<F: FieldElement> BackendFactory<F> for MockBackendFactory {
}
let machine_to_pil = powdr_backend_utils::split_pil(&pil);
let connections = Connection::get_all(&pil, &machine_to_pil);
let bus_connections = BusConnection::get_all(&pil, &machine_to_pil);
let bus_connections = BusInteraction::get_all(&pil, &machine_to_pil);

Ok(Box::new(MockBackend {
machine_to_pil,
Expand All @@ -69,7 +69,7 @@ pub(crate) struct MockBackend<F> {
machine_to_pil: BTreeMap<String, Analyzed<F>>,
fixed: Arc<Vec<(String, VariablySizedColumn<F>)>>,
connections: Vec<Connection<F>>,
bus_connections: Vec<BusConnection<F>>,
bus_connections: Vec<BusInteraction<F>>,
}

impl<F: FieldElement> Backend<F> for MockBackend<F> {
Expand Down

0 comments on commit feec718

Please sign in to comment.