Skip to content

Commit

Permalink
[Cider] First pass at data-race detection and also some control port …
Browse files Browse the repository at this point in the history
…overhauling. (#2305)

This adds a thread-id and vector clock system to Cider enabling some
race-detection checks. The checks are turned off by default, since the
analysis can be expensive, but can be enabled with the
`--check-data-race` flag. The checks are overly conservative right now
for `with` groups under the current semantic model and will produce
false positives in these cases.

I also ended up adjusting the treatment of control ports in this set of
changes. We explicitly consider some control ports rather than special
casing the `@done` ports, however this does not extend to every port by
default. Currently, we treat `@go`, `@done`, `inout`, and ports
explicitly marked `@control` as control. To avoid breaking a bunch of
existing code, we also ignore any attempts to set a zero control port to
`undef` with an assignment. This also requires us to update the
assignment conflict rules so that “implicit” values---those produced by
zeroing a control, or otherwise assigning a value which does not come
from a cell or assignment---are allowed to be overwritten by cells or
assignments. Implicit values may not, however, override any defined
value.
  • Loading branch information
EclecticGriffin authored Oct 16, 2024
1 parent 074df16 commit 586fb25
Show file tree
Hide file tree
Showing 27 changed files with 2,086 additions and 326 deletions.
6 changes: 4 additions & 2 deletions interp/src/debugger/debugger_core.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ pub struct Debugger<C: AsRef<Context> + Clone> {
}

/// A type alias for the debugger using an Rc of the context. Use this in cases
/// where the use of lifetimes would be a hinderance.
/// where the use of lifetimes would be a hindrance.
pub type OwnedDebugger = Debugger<Rc<Context>>;

impl OwnedDebugger {
Expand All @@ -94,7 +94,7 @@ impl OwnedDebugger {
)?;

let debugger: Debugger<Rc<Context>> =
Self::new(Rc::new(ctx), &None, &None)?;
Self::new(Rc::new(ctx), &None, &None, false)?;

Ok((debugger, map))
}
Expand All @@ -106,11 +106,13 @@ impl<C: AsRef<Context> + Clone> Debugger<C> {
program_context: C,
data_file: &Option<std::path::PathBuf>,
wave_file: &Option<std::path::PathBuf>,
check_data_races: bool,
) -> InterpreterResult<Self> {
let mut interpreter = Simulator::build_simulator(
program_context.clone(),
data_file,
wave_file,
check_data_races,
)?;
interpreter.converge()?;

Expand Down
17 changes: 16 additions & 1 deletion interp/src/errors.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,12 @@ use crate::flatten::{
base::{AssignmentWinner, ComponentIdx, GlobalCellIdx, GlobalPortIdx},
prelude::AssignedValue,
},
structures::environment::Environment,
structures::environment::{clock::ClockError, Environment},
};
use baa::{BitVecOps, BitVecValue};
use calyx_ir::Id;
use calyx_utils::{Error as CalyxError, MultiError as CalyxMultiError};
use owo_colors::OwoColorize;
use rustyline::error::ReadlineError;
use thiserror::Error;

Expand Down Expand Up @@ -193,10 +194,16 @@ pub enum InterpreterError {
)]
UndefinedReadAddr(GlobalCellIdx),

#[error("Attempted to undefine a defined port \"{0:?}\"")]
UndefiningDefinedPort(GlobalPortIdx),

/// A wrapper for serialization errors
#[error(transparent)]
SerializationError(#[from] crate::serialization::SerializationError),

#[error(transparent)]
ClockError(#[from] ClockError),

/// A nonspecific error, used for arbitrary messages
#[error("{0}")]
GenericError(String),
Expand Down Expand Up @@ -295,6 +302,14 @@ impl InterpreterError {
InterpreterError::UndefinedWrite(c) => InterpreterError::GenericError(format!("Attempted to write an undefined value to register or memory named \"{}\"", env.get_full_name(c))),
InterpreterError::UndefinedWriteAddr(c) => InterpreterError::GenericError(format!("Attempted to write to an undefined memory address in memory named \"{}\"", env.get_full_name(c))),
InterpreterError::UndefinedReadAddr(c) => InterpreterError::GenericError(format!("Attempted to read from an undefined memory address from memory named \"{}\"", env.get_full_name(c))),
InterpreterError::ClockError(clk) => {
match clk {
ClockError::ReadWrite(c) => InterpreterError::GenericError(format!("Concurrent read & write to the same register/memory {}", env.get_full_name(c).underline())),
ClockError::WriteWrite(c) => InterpreterError::GenericError(format!("Concurrent writes to the same register/memory {}", env.get_full_name(c).underline())),
_ => InterpreterError::ClockError(clk),
}
}
InterpreterError::UndefiningDefinedPort(p) => InterpreterError::GenericError(format!("Attempted to undefine a defined port \"{}\"", env.get_full_name(p))),
e => e,
}
}
Expand Down
62 changes: 60 additions & 2 deletions interp/src/flatten/flat_ir/base.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,10 @@ use std::{

use super::{cell_prototype::CellPrototype, prelude::Identifier};
use crate::{
flatten::structures::index_trait::{
impl_index, impl_index_nonzero, IndexRange, IndexRef,
flatten::structures::{
environment::clock::ClockPair,
index_trait::{impl_index, impl_index_nonzero, IndexRange, IndexRef},
thread::ThreadIdx,
},
serialization::PrintCode,
};
Expand Down Expand Up @@ -424,13 +426,16 @@ impl From<AssignmentIdx> for AssignmentWinner {
pub struct AssignedValue {
val: BitVecValue,
winner: AssignmentWinner,
thread: Option<ThreadIdx>,
clocks: Option<ClockPair>,
}

impl std::fmt::Debug for AssignedValue {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
f.debug_struct("AssignedValue")
.field("val", &self.val.to_bit_str())
.field("winner", &self.winner)
.field("thread", &self.thread)
.finish()
}
}
Expand All @@ -448,9 +453,26 @@ impl AssignedValue {
Self {
val,
winner: winner.into(),
thread: None,
clocks: None,
}
}

pub fn with_thread(mut self, thread: ThreadIdx) -> Self {
self.thread = Some(thread);
self
}

pub fn with_thread_optional(mut self, thread: Option<ThreadIdx>) -> Self {
self.thread = thread;
self
}

pub fn with_clocks(mut self, clock_pair: ClockPair) -> Self {
self.clocks = Some(clock_pair);
self
}

/// Returns true if the two AssignedValues do not have the same winner
pub fn has_conflict_with(&self, other: &Self) -> bool {
self.winner != other.winner
Expand All @@ -472,6 +494,8 @@ impl AssignedValue {
Self {
val: BitVecValue::tru(),
winner: AssignmentWinner::Implicit,
thread: None,
clocks: None,
}
}

Expand All @@ -482,6 +506,8 @@ impl AssignedValue {
Self {
val,
winner: AssignmentWinner::Cell,
thread: None,
clocks: None,
}
}

Expand All @@ -492,6 +518,8 @@ impl AssignedValue {
Self {
val,
winner: AssignmentWinner::Implicit,
thread: None,
clocks: None,
}
}

Expand All @@ -507,6 +535,14 @@ impl AssignedValue {
pub fn cell_b_low() -> Self {
Self::cell_value(BitVecValue::fals())
}

pub fn thread(&self) -> Option<ThreadIdx> {
self.thread
}

pub fn clocks(&self) -> Option<&ClockPair> {
self.clocks.as_ref()
}
}

#[derive(Debug, Clone, Default)]
Expand Down Expand Up @@ -539,6 +575,20 @@ impl PortValue {
self.0.as_ref()
}

pub fn with_thread(mut self, thread: ThreadIdx) -> Self {
if let Some(val) = self.0.as_mut() {
val.thread = Some(thread);
}
self
}

pub fn with_thread_optional(mut self, thread: Option<ThreadIdx>) -> Self {
if let Some(val) = self.0.as_mut() {
val.thread = thread;
}
self
}

/// If the value is defined, returns the value cast to a boolean. Otherwise
/// returns `None`. It will panic if the given value is not one bit wide.
pub fn as_bool(&self) -> Option<bool> {
Expand All @@ -551,12 +601,20 @@ impl PortValue {
self.0.as_ref().map(|x| x.val().to_u64().unwrap())
}

pub fn is_zero(&self) -> Option<bool> {
self.0.as_ref().map(|x| x.val.is_zero())
}

/// Returns a reference to the underlying value if it is defined. Otherwise
/// returns `None`.
pub fn val(&self) -> Option<&BitVecValue> {
self.0.as_ref().map(|x| &x.val)
}

pub fn clocks(&self) -> Option<ClockPair> {
self.0.as_ref().and_then(|x| x.clocks)
}

/// Returns a reference to the underlying [`AssignmentWinner`] if it is
/// defined. Otherwise returns `None`.
pub fn winner(&self) -> Option<&AssignmentWinner> {
Expand Down
51 changes: 48 additions & 3 deletions interp/src/flatten/flat_ir/control/translator.rs
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,43 @@ fn translate_guard(
interp_ctx: &mut InterpretationContext,
map: &PortMapper,
) -> GuardIdx {
flatten_tree(guard, None, &mut interp_ctx.guards, map)
let idx = flatten_tree(guard, None, &mut interp_ctx.guards, map);

// not worth trying to force this search traversal into the flatten trait so
// I'm just gonna opt for this. It's a onetime cost, so I'm not particularly
// worried about it
let mut search_stack = vec![idx];
let mut read_ports = vec![];

while let Some(idx) = search_stack.pop() {
match &interp_ctx.guards[idx] {
Guard::True => {}
Guard::Or(guard_idx, guard_idx1) => {
search_stack.push(*guard_idx);
search_stack.push(*guard_idx1);
}
Guard::And(guard_idx, guard_idx1) => {
search_stack.push(*guard_idx);
search_stack.push(*guard_idx1);
}
Guard::Not(guard_idx) => {
search_stack.push(*guard_idx);
}
Guard::Comp(_port_comp, port_ref, port_ref1) => {
read_ports.push(*port_ref);
read_ports.push(*port_ref1);
}
Guard::Port(port_ref) => {
read_ports.push(*port_ref);
}
}
}

if !read_ports.is_empty() {
interp_ctx.guard_read_map.insert_value(idx, read_ports);
}

idx
}

fn translate_component(
Expand Down Expand Up @@ -287,8 +323,17 @@ fn insert_port(
local_offset.into()
}
ContainmentType::Local => {
let idx_definition =
secondary_ctx.push_local_port(id, port.borrow().width as usize);
let borrow = port.borrow();
let is_control = borrow.has_attribute(calyx_ir::NumAttr::Go)
|| borrow.has_attribute(calyx_ir::NumAttr::Done)
|| borrow.has_attribute(calyx_ir::BoolAttr::Control)
|| (borrow.direction == calyx_ir::Direction::Inout);

let idx_definition = secondary_ctx.push_local_port(
id,
port.borrow().width as usize,
is_control,
);
let local_offset = aux.port_offset_map.insert(idx_definition);
local_offset.into()
}
Expand Down
Loading

0 comments on commit 586fb25

Please sign in to comment.