Closed bensimner closed 3 years ago
I am wary of putting extra events into ExecutionInfo, how are you stopping them from reaching the SMT solver? A clean way to go might be to do something like:
#[derive(Debug)]
pub struct ExecutionInfo<'ev, B> {
/// A vector containing all the events in a candidate execution that the axiomatic concurrency model can use
pub events: Vec<AxEvent<'ev, B>>,
/// A vector containing extra events that can appear in the graph, but won't be given to Z3
pub extra_events: Vec<ExtraEvent<'ev, B>>,
/// A vector of po-ordered instruction opcodes for each thread
pub thread_opcodes: Vec<Vec<B>>,
/// The final write for each register in each thread (if written at all)
pub final_writes: HashMap<(Name, ThreadId), &'ev Val<B>>,
}
Could have ExtraEvent be a separate type as above or just be AxEvent if that's easiest
New Graph drawing code and smt/graph event generation for translations