From 268bd8bb4db3ad76afc269ae29de10f1a37cf9d3 Mon Sep 17 00:00:00 2001 From: Eliza Weisman Date: Wed, 4 May 2022 12:03:10 -0700 Subject: [PATCH] add a span for the current model's iteration Signed-off-by: Eliza Weisman --- src/model.rs | 25 ++++++++++++++++--------- src/rt/thread.rs | 29 ++++++++++++++++++++--------- 2 files changed, 36 insertions(+), 18 deletions(-) diff --git a/src/model.rs b/src/model.rs index 1623ae62..c7169c38 100644 --- a/src/model.rs +++ b/src/model.rs @@ -133,6 +133,9 @@ impl Builder { where F: Fn() + Sync + Send + 'static, { + let mut i = 1; + let mut _span = tracing::info_span!("iter", message = i).entered(); + let mut execution = Execution::new(self.max_threads, self.max_branches, self.preemption_bound); let mut scheduler = Scheduler::new(self.max_threads); @@ -149,17 +152,15 @@ impl Builder { let f = Arc::new(f); - let mut i = 0; - let start = Instant::now(); - loop { - i += 1; - if i % self.checkpoint_interval == 0 { - info!(""); - info!(" ================== Iteration {} ==================", i); - info!(""); + info!(parent: None, ""); + info!( + parent: None, + " ================== Iteration {} ==================", i + ); + info!(parent: None, ""); if let Some(ref path) = self.checkpoint_file { checkpoint::store_execution_path(&execution.path, path); @@ -193,10 +194,16 @@ impl Builder { execution.check_for_leaks(); + i += 1; + + // Create the next iteration's `tracing` span before trying to step to the next + // execution, as the `Execution` will capture the current span when + // it's reset. + _span = tracing::info_span!(parent: None, "iter", message = i).entered(); if let Some(next) = execution.step() { execution = next; } else { - info!("Completed in {} iterations", i); + info!(parent: None, "Completed in {} iterations", i - 1); return; } } diff --git a/src/rt/thread.rs b/src/rt/thread.rs index d1a4c32d..626cc552 100644 --- a/src/rt/thread.rs +++ b/src/rt/thread.rs @@ -8,8 +8,6 @@ use super::Location; pub(crate) struct Thread { pub id: Id, - pub span: tracing::Span, - /// If the thread is runnable, blocked, or terminated. pub state: State, @@ -35,6 +33,9 @@ pub(crate) struct Thread { pub yield_count: usize, locals: LocalMap, + + /// `tracing` span used to associate diagnostics with the current thread. + span: tracing::Span, } #[derive(Debug)] @@ -53,6 +54,9 @@ pub(crate) struct Set { /// Sequential consistency causality. All sequentially consistent operations /// synchronize with this causality. pub seq_cst_causality: VersionVec, + + /// `tracing` span used as the parent for new thread spans. + iteration_span: tracing::Span, } #[derive(Eq, PartialEq, Hash, Copy, Clone)] @@ -85,10 +89,10 @@ struct LocalKeyId(usize); struct LocalValue(Option>); impl Thread { - fn new(id: Id) -> Thread { + fn new(id: Id, parent_span: &tracing::Span) -> Thread { Thread { id, - span: tracing::info_span!(parent: None, "thread", id = id.id), + span: tracing::info_span!(parent: parent_span.id(), "thread", id = id.id), state: State::Runnable { unparked: false }, critical: false, operation: None, @@ -187,15 +191,18 @@ impl Set { /// The set may contain up to `max_threads` threads. pub(crate) fn new(execution_id: execution::Id, max_threads: usize) -> Set { let mut threads = Vec::with_capacity(max_threads); - + // Capture the current iteration's span to be used as each thread + // span's parent. + let iteration_span = tracing::Span::current(); // Push initial thread - threads.push(Thread::new(Id::new(execution_id, 0))); + threads.push(Thread::new(Id::new(execution_id, 0), &iteration_span)); Set { execution_id, threads, active: Some(0), seq_cst_causality: VersionVec::new(), + iteration_span, } } @@ -211,8 +218,10 @@ impl Set { let id = self.threads.len(); // Push the thread onto the stack - self.threads - .push(Thread::new(Id::new(self.execution_id, id))); + self.threads.push(Thread::new( + Id::new(self.execution_id, id), + &self.iteration_span, + )); Id::new(self.execution_id, id) } @@ -323,8 +332,10 @@ impl Set { } pub(crate) fn clear(&mut self, execution_id: execution::Id) { + self.iteration_span = tracing::Span::current(); self.threads.clear(); - self.threads.push(Thread::new(Id::new(execution_id, 0))); + self.threads + .push(Thread::new(Id::new(execution_id, 0), &self.iteration_span)); self.execution_id = execution_id; self.active = Some(0);