From ad0ff22ee00c92606e6dd9c66346c458fdbb7dc9 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 15:54:51 -0500 Subject: [PATCH 01/19] Add LoopArgState definition --- monitor/src/interpreter.rs | 18 +++++++++++++--- monitor/src/scheduler.rs | 41 ++++++++++++++++++++++++++++++++---- monitor/src/thread.rs | 6 +++++- monitor/src/types.rs | 21 ++++++++++++++++++ protocols/src/interpreter.rs | 11 +++++----- protocols/src/ir.rs | 9 ++++---- protocols/src/parser.rs | 2 +- protocols/src/serialize.rs | 4 ++-- protocols/src/typecheck.rs | 2 +- 9 files changed, 93 insertions(+), 21 deletions(-) diff --git a/monitor/src/interpreter.rs b/monitor/src/interpreter.rs index 9c565251..d691c934 100644 --- a/monitor/src/interpreter.rs +++ b/monitor/src/interpreter.rs @@ -15,17 +15,25 @@ use crate::{ global_context::GlobalContext, signal_trace::{PortKey, SignalTrace, WaveSignalTrace}, thread::Thread, - types::ProtocolApplication, + types::{LoopArgState, ProtocolApplication}, }; +#[allow(dead_code)] #[derive(Clone)] pub struct Interpreter { pub transaction: Transaction, pub symbol_table: SymbolTable, pub next_stmt_map: NextStmtMap, + + /// Maps protocol arguments (input/output parameters) to their values pub args_mapping: FxHashMap, + + /// Tracks which bits of a `SymbolId` are known pub known_bits: FxHashMap, + /// Tracks the state of arguments for `repeat` loops + pub loop_args: FxHashMap, + /// Constraints on DUT input port values that must hold after stepping. /// These are established by assignments like `D.m_axis_tvalid := 1'b1` /// and verified after each `step()` to ensure the constraint still holds. @@ -91,6 +99,7 @@ impl Interpreter { self.known_bits = thread.known_bits.clone(); self.constraints = thread.constraints.clone(); self.args_to_pins = thread.args_to_pins.clone(); + self.loop_args = thread.loop_args.clone(); } /// Pretty-prints a `Statement` identified by its `StmtId` @@ -157,6 +166,7 @@ impl Interpreter { trace_cycle_count, args_to_pins: FxHashMap::default(), dut_symbol_id, + loop_args: FxHashMap::default(), } } @@ -475,8 +485,10 @@ impl Interpreter { Stmt::While(loop_guard_id, do_block_id) => { self.evaluate_while(loop_guard_id, stmt_id, do_block_id, ctx, trace) } - Stmt::BoundedLoop(_, _) => { - todo!("Bounded loops is not yet implemented in the monitor") + Stmt::RepeatLoop(_, _) => { + // Repeat loops are intercepted in `run_thread_till_next_step` + // in `scheduler.rs`, so this case is unreachable + unreachable!("Repeat loops handled in `scheduler.rs` already") } Stmt::Step | Stmt::Fork => { // The scheduler handles `step`s and `fork`s. diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index 707d3ceb..8baf9b7e 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -1,9 +1,9 @@ -use anyhow::{Context, anyhow}; +use anyhow::{anyhow, Context}; use baa::BitVecOps; use log::info; use protocols::{ errors::{EvaluationError, ExecutionError}, - ir::{Stmt, SymbolId, SymbolTable, Transaction}, + ir::{Expr, Stmt, SymbolId, SymbolTable, Transaction}, serialize::serialize_bitvec, }; use rustc_hash::FxHashSet; @@ -15,7 +15,8 @@ use crate::{ signal_trace::{SignalTrace, WaveSignalTrace}, thread::Thread, types::{ - AugmentedProtocolApplication, AugmentedTrace, CycleResult, SchedulerError, ThreadResult, + AugmentedProtocolApplication, AugmentedTrace, CycleResult, LoopArgState, SchedulerError, + ThreadResult, }, }; @@ -143,7 +144,7 @@ impl Scheduler { current_threads.push_back(thread); thread_id += 1; } - // Technically, initializing the `interpreter` here is necessary + // Technically, initializing the `interpreter` here is unnecessary // since when we pop a thread from the `current` queue, we perform // a context switch and run the `interpreter` on the transaction/symbol_table // corresponding to the thread. However, we do this here nonetheless @@ -673,6 +674,38 @@ impl Scheduler { let mut current_stmt_id = thread.current_stmt_id; loop { + // Intercept repeat loops before evaluating statements + if let Stmt::RepeatLoop(loop_arg_expr_id, loop_body_id) = + thread.transaction[current_stmt_id] + { + let loop_stmt_id = current_stmt_id; + let loop_arg_symbol_id = match thread.transaction[loop_arg_expr_id] { + Expr::Sym(symbol_id) => symbol_id, + _ => { + unreachable!("Arguments to repeat loops are always SymbolIDs") + } + }; + + match thread.loop_args.get(&loop_arg_symbol_id) { + None => { + // First time seeing loop arg, it is `Unknown` + // (i.e. absent from the thread's `loop_args` map) + + // Update the thread's `loop_args` map so that + // the `loop_arg_symbol_id` is now `Speculative(1, ...)` + thread.loop_args.insert( + loop_arg_symbol_id, + LoopArgState::Speculative(1, loop_stmt_id), + ); + + // Execute the loop body + current_stmt_id = loop_body_id; + } + Some(_) => todo!(), + } + + continue; + } match self.interpreter.evaluate_stmt(¤t_stmt_id, ctx, trace) { Ok(Some(next_stmt_id)) => { // Update thread-local maps diff --git a/monitor/src/thread.rs b/monitor/src/thread.rs index 59ddef8e..f617cf22 100644 --- a/monitor/src/thread.rs +++ b/monitor/src/thread.rs @@ -10,7 +10,7 @@ use protocols::{ }; use rustc_hash::FxHashMap; -use crate::global_context::GlobalContext; +use crate::{global_context::GlobalContext, types::LoopArgState}; /// The local context associated with an individual thread, /// storing information such as: @@ -62,6 +62,9 @@ pub struct Thread { /// Maps function parameters to DUT ports pub args_to_pins: FxHashMap, + /// Maps arguments of `repeat` loops to their current state + pub loop_args: FxHashMap, + /// Determines if the thread has called `fork()` yet. Initialized to `false`. /// Since well-formedness dicates that a protocol can only contain /// at most one `fork()`, once this flag is set to `true`, @@ -117,6 +120,7 @@ impl Thread { start_time_step, args_to_pins: FxHashMap::default(), has_forked: false, + loop_args: FxHashMap::default(), } } diff --git a/monitor/src/types.rs b/monitor/src/types.rs index 11b6ad5d..8d818fad 100644 --- a/monitor/src/types.rs +++ b/monitor/src/types.rs @@ -7,6 +7,8 @@ use std::{collections::VecDeque, fmt}; +use protocols::ir::StmtId; + use crate::{scheduler::Scheduler, thread::Thread}; /// Represents a protocol application like `add(1, 2, 3)` which appears @@ -130,3 +132,22 @@ pub enum CycleResult { parent: Box>, }, } + +/// The possible states for an argument to a `repeat` loop. +/// We maintain the following invariants: +/// - `Speculative(n, loopID) `only becomes `Known(n)` after the corresponding +/// scheduler has executed the body of the loop at `loopID` exactly `n` +/// times (note that `n`` can be 0). +/// - Once a `LoopArg` becomes Known, we proceed to the next statement +/// that immediately follows the loop (we don't enter the loop body). +/// - Moreover, once a `LoopArg` remains `Known`, it remains `Known` thereafter. +#[allow(dead_code)] +#[derive(Debug, Clone)] +pub enum LoopArgState { + /// `Speculative(n, loopID)` means the associated thread has already + /// *speculatively* executed the loop at `loopID` for `n` iterations. + /// (The `StmtId` is there to disambiguate between different loop statements, + /// since different loops can use the same loop argument `n`.) + Speculative(u64, StmtId), + Known(u64), +} diff --git a/protocols/src/interpreter.rs b/protocols/src/interpreter.rs index 8203db7f..33c6b653 100644 --- a/protocols/src/interpreter.rs +++ b/protocols/src/interpreter.rs @@ -14,8 +14,8 @@ use log::info; use patronus::expr::ExprRef; use patronus::sim::{InitKind, Interpreter, Simulator}; use patronus::system::Output; -use rand::SeedableRng; use rand::rngs::StdRng; +use rand::SeedableRng; use rustc_hash::FxHashMap; /// Per-thread input value: either a concrete assignment or DontCare @@ -231,9 +231,10 @@ impl<'a> Evaluator<'a> { patronus::system::analysis::cone_of_influence_comb(ctx, sys, out.expr); for input_expr in input_exprs { // Find the protocol symbol corresponding to this input expression - if let Some(input_sym) = input_mapping - .iter() - .find_map(|(k, v)| if *v == input_expr { Some(*k) } else { None }) + if let Some(input_sym) = + input_mapping + .iter() + .find_map(|(k, v)| if *v == input_expr { Some(*k) } else { None }) { // output_dependencies: output -> Vec (inputs this output depends on) if let Some(vec) = output_dependencies.get_mut(out_sym) { @@ -744,7 +745,7 @@ impl<'a> Evaluator<'a> { Stmt::While(loop_guard_id, do_block_id) => { self.evaluate_while(loop_guard_id, stmt_id, do_block_id) } - Stmt::BoundedLoop(num_iters_id, loop_body_id) => { + Stmt::RepeatLoop(num_iters_id, loop_body_id) => { self.evaluate_bounded_loop(num_iters_id, stmt_id, loop_body_id) } Stmt::Step => { diff --git a/protocols/src/ir.rs b/protocols/src/ir.rs index 2cf720a3..9fb63f58 100644 --- a/protocols/src/ir.rs +++ b/protocols/src/ir.rs @@ -6,7 +6,7 @@ // author: Ernest Ng use baa::BitVecValue; -use cranelift_entity::{PrimaryMap, SecondaryMap, entity_impl}; +use cranelift_entity::{entity_impl, PrimaryMap, SecondaryMap}; use itertools::Itertools; use rustc_hash::FxHashMap; use std::ops::Index; @@ -148,7 +148,7 @@ impl Transaction { } // Add a back-edge from the loop body to the current `stmt_id` // (same as how while-loops are represented in the current AST) - Stmt::BoundedLoop(_, body_id) => { + Stmt::RepeatLoop(_, body_id) => { map.extend(self.next_stmt_mapping_helper(*body_id, Some(stmt_id))); } _ => {} @@ -325,8 +325,9 @@ pub enum Stmt { Step, Fork, While(ExprId, StmtId), - // Bounded loop with fixed no. of iterations - BoundedLoop(ExprId, StmtId), + /// Bounded loop with fixed no. of iterations + /// (`ExprId` is the no. of iterations, `StmtId` is the loop body) + RepeatLoop(ExprId, StmtId), IfElse(ExprId, StmtId, StmtId), AssertEq(ExprId, ExprId), } diff --git a/protocols/src/parser.rs b/protocols/src/parser.rs index c12398fb..43289f7e 100644 --- a/protocols/src/parser.rs +++ b/protocols/src/parser.rs @@ -443,7 +443,7 @@ impl ParserContext<'_> { )?; let num_iterations = self.parse_expr(expr_rule.into_inner())?; let body = self.parse_stmt_block(inner_rules)?; - Ok(Stmt::BoundedLoop(num_iterations, body)) + Ok(Stmt::RepeatLoop(num_iterations, body)) } fn parse_assert_eq(&mut self, pair: pest::iterators::Pair) -> Result { diff --git a/protocols/src/serialize.rs b/protocols/src/serialize.rs index 4dfc470b..c5c30842 100644 --- a/protocols/src/serialize.rs +++ b/protocols/src/serialize.rs @@ -176,7 +176,7 @@ pub fn serialize_stmt(tr: &Transaction, st: &SymbolTable, stmt_id: &StmtId) -> S serialize_stmt(tr, st, stmt_id) ) } - Stmt::BoundedLoop(expr_id, stmt_id) => { + Stmt::RepeatLoop(expr_id, stmt_id) => { format!( "repeat {} iterations {{ {} }}", serialize_expr(tr, st, expr_id), @@ -236,7 +236,7 @@ pub fn build_statements( build_statements(out, tr, st, bodyid, index + 1)?; writeln!(out, "{}}}", " ".repeat(index))?; } - Stmt::BoundedLoop(count, bodyid) => { + Stmt::RepeatLoop(count, bodyid) => { writeln!( out, "{}repeat {} iterations {{", diff --git a/protocols/src/typecheck.rs b/protocols/src/typecheck.rs index 67d08adf..aec8da1c 100644 --- a/protocols/src/typecheck.rs +++ b/protocols/src/typecheck.rs @@ -203,7 +203,7 @@ fn check_stmt_types( Err(anyhow!(error_msg)) } } - Stmt::BoundedLoop(count_expr, bodyid) => { + Stmt::RepeatLoop(count_expr, bodyid) => { // Typecheck the no. of iterations (which must be a BitVec type of any width) let num_iterations_type = check_expr_types(tr, st, handler, count_expr)?; if let Type::BitVec(_) = num_iterations_type { From d9686194a96e0c95ac2569c8f6eb2cc0582caed9 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 16:26:12 -0500 Subject: [PATCH 02/19] Handle speculative loop exeuction --- monitor/src/global_scheduler.rs | 34 ++++++++++++-- monitor/src/scheduler.rs | 83 ++++++++++++++++++++++++++++----- monitor/src/types.rs | 34 ++++++++++++-- protocols/src/interpreter.rs | 9 ++-- protocols/src/ir.rs | 2 +- 5 files changed, 137 insertions(+), 25 deletions(-) diff --git a/monitor/src/global_scheduler.rs b/monitor/src/global_scheduler.rs index 7d5a2a6d..8a141a9e 100644 --- a/monitor/src/global_scheduler.rs +++ b/monitor/src/global_scheduler.rs @@ -48,14 +48,16 @@ fn process_group_cycles( match scheduler.process_current_queue(trace, ctx) { Ok(CycleResult::Done) => processed_schedulers.push_back(scheduler), Ok(CycleResult::Fork { parent }) => { - // Iterate over all possible candidate protocols + // When there is an explicit/implicit fork, + // we need to iterate over all possible candidate protocols + // and for each candidate protocol, spawn a scheduler that runs it for (transaction, symbol_table) in &scheduler.possible_transactions { let mut cloned_scheduler = scheduler.clone(); // If there was an explicit fork, we have to add the - // parent thread to the cloned scheduler + // parent thread to the cloned scheduler's `current` queue. if let Some(ref thread) = *parent { - cloned_scheduler.current.push_front(thread.clone()); + cloned_scheduler.current.push_back(thread.clone()); } // Create a new thread for the candidate protocol @@ -75,6 +77,32 @@ fn process_group_cycles( schedulers_to_process.push_back(cloned_scheduler); } } + Ok(CycleResult::RepeatLoopFork { + exited_thread, + speculative_thread, + }) => { + // For forks that arise due to `repeat` loops, + // create 2 schedulers that each execute a different thread: + // - One which executes the `exited_thread`, i.e. the thread + // which exits the loop with the `LoopArg` set to + // `Known(n)` for some `n >= 0` + // - One which executes the `speculative_thread`, i.e. + // the thread which speculatively executes the loop body + // for another iteration, with the `LoopArg` + // set to `Speculative(n + 1)` + + let mut scheduler_with_exited_thread = scheduler.clone(); + scheduler_with_exited_thread + .current + .push_back(*exited_thread); + schedulers_to_process.push_back(scheduler_with_exited_thread); + + let mut scheduler_with_speculative_thread = scheduler.clone(); + scheduler_with_speculative_thread + .current + .push_back(*speculative_thread); + schedulers_to_process.push_back(scheduler_with_speculative_thread); + } Err(SchedulerError::NoTransactionsMatch { struct_name, error_context, diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index 8baf9b7e..2b74b474 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -1,4 +1,4 @@ -use anyhow::{anyhow, Context}; +use anyhow::{Context, anyhow}; use baa::BitVecOps; use log::info; use protocols::{ @@ -198,8 +198,8 @@ impl Scheduler { /// (marking all suspended threads as ready for execution), /// then advances the trace to the next step. /// Notes: - /// - This function is used by `GlobalScheduler` to coordinate - /// execution between multiple schedulers. + /// - This function is used by `GlobalScheduler::process_group_cycles` + /// to coordinate execution between multiple schedulers. /// - When a `fork` creates a `Scheduler` clone, call this function /// on the clone pub fn process_current_queue( @@ -212,7 +212,10 @@ impl Scheduler { self.struct_name ); - // Process each thread (this function returns early when a thread `fork`s) + // Process each thread. Note that + // this function returns early when a thread `fork`s, with the + // new forked-off threads propagated to the caller + // (`GlobalScheduler::process_group_cycles`) while let Some(thread) = self.current.pop_front() { match self.run_thread_till_next_step(thread, trace, ctx)? { ThreadResult::Completed => continue, @@ -226,6 +229,15 @@ impl Scheduler { parent: Box::new(None), }); } + ThreadResult::RepeatLoopFork { + exited_thread, + speculative_thread, + } => { + return Ok(CycleResult::RepeatLoopFork { + exited_thread, + speculative_thread, + }); + } } } @@ -691,20 +703,69 @@ impl Scheduler { // First time seeing loop arg, it is `Unknown` // (i.e. absent from the thread's `loop_args` map) - // Update the thread's `loop_args` map so that - // the `loop_arg_symbol_id` is now `Speculative(1, ...)` + // Create a new thread `exited_thread` that is identical + // to the current thread, but it exits the loop + // with the `LoopArg` set to `Known(0)` + let mut exited_thread = thread.clone(); + exited_thread.thread_id = self.num_threads; + self.num_threads += 1; + exited_thread + .loop_args + .insert(loop_arg_symbol_id, LoopArgState::Known(0)); + + // Update the current thread's `loop_args` map so that + // the `LoopArg` is now `Speculative(1)` thread.loop_args.insert( loop_arg_symbol_id, LoopArgState::Speculative(1, loop_stmt_id), ); - // Execute the loop body - current_stmt_id = loop_body_id; + // Execute the loop body in the current thread + thread.current_stmt_id = loop_body_id; + + // Let the global scheduler deal with both threads + // (The current thread is called the `speculative_thread`, + // since it speculatively executes the loop body again + // with the `LoopArg` set to `Speculative(1)`) + return Ok(ThreadResult::RepeatLoopFork { + exited_thread: Box::new(exited_thread), + speculative_thread: Box::new(thread), + }); } - Some(_) => todo!(), - } + Some(LoopArgState::Speculative(n, _)) => { + // Create a new thread `exited_thread` that is identical + // to the current thread, but it exits the loop + // with the `LoopArg` set to `Known(n)` + let mut exited_thread = thread.clone(); + exited_thread.thread_id = self.num_threads; + self.num_threads += 1; + exited_thread + .loop_args + .insert(loop_arg_symbol_id, LoopArgState::Known(*n)); + + // Update the current thread's `loop_args` map so that + // the `LoopArg` is now `Speculative(n + 1)` + thread.loop_args.insert( + loop_arg_symbol_id, + LoopArgState::Speculative(n + 1, loop_stmt_id), + ); - continue; + // Execute the loop body in the current thread + thread.current_stmt_id = loop_body_id; + + // Let the global scheduler deal with both threads + // (The current thread is called the `speculative_thread`, + // since it speculatively executes the loop body again + // with the `LoopArg` set to `Speculative(1)`) + return Ok(ThreadResult::RepeatLoopFork { + exited_thread: Box::new(exited_thread), + speculative_thread: Box::new(thread), + }); + } + Some(LoopArgState::Known(_)) => { + todo!("Handle case when `LoopArg` is `Known`") + } + } } match self.interpreter.evaluate_stmt(¤t_stmt_id, ctx, trace) { Ok(Some(next_stmt_id)) => { diff --git a/monitor/src/types.rs b/monitor/src/types.rs index 8d818fad..24ab2284 100644 --- a/monitor/src/types.rs +++ b/monitor/src/types.rs @@ -97,8 +97,11 @@ impl From for SchedulerError { } } -/// The result of an individual `Thread`: either it `Completed`, -/// forked explcitly or forked implicitly. +/// The result of an individual `Thread` is one of four options: +/// - it `Completed` (was moved to one of the `next/finished/failed` queues) +/// - it forked explicitly (by calling `fork()`) (`ExplicitFork`) +/// - it forked implicitly at the end of a protocol (`ImplicitFork`) +/// - it forked after encountering a `repeat` loop (`RepeatLoopFork`) #[derive(Debug)] pub enum ThreadResult { /// Thread completed (moved to next/finished/failed queue) @@ -112,11 +115,22 @@ pub enum ThreadResult { /// constructors of this enum. ExplicitFork { parent: Box }, - /// Thread is laready in the `finished queue and forked implicitly + /// Thread is already in the `finished` queue and forked implicitly /// (e.g. this thread is a protocol which ends with `step` without /// ever calling `fork`). The caller of a function which returns /// this constructor is responsible for spawning new protocol ImplicitFork, + + /// A fork that arises when learning the value of arguments to `repeat` loops + RepeatLoopFork { + /// The thread that exited the loop with the loop argument + /// set to `Known(n)` for some `n >= 0` + exited_thread: Box, + + /// The thread that remains in the loop and executed the loop body again, + /// with the loop argument set to `Speculative(n + 1)` + speculative_thread: Box, + }, } /// The result of the *Scheduler* at the end of a cycle @@ -131,13 +145,23 @@ pub enum CycleResult { /// constructors of this enum. parent: Box>, }, + /// A fork that arises when learning the value of arguments to `repeat` loops + RepeatLoopFork { + /// The thread that exited the loop with the loop argument + /// set to `Known(n)` for some `n >= 0` + exited_thread: Box, + + /// The thread that remains in the loop and executed the loop body again, + /// with the loop argument set to `Speculative(n + 1)` + speculative_thread: Box, + }, } /// The possible states for an argument to a `repeat` loop. /// We maintain the following invariants: /// - `Speculative(n, loopID) `only becomes `Known(n)` after the corresponding -/// scheduler has executed the body of the loop at `loopID` exactly `n` -/// times (note that `n`` can be 0). +/// scheduler has executed the body of the loop at `loopID` exactly `n` +/// times (note that `n` can be 0). /// - Once a `LoopArg` becomes Known, we proceed to the next statement /// that immediately follows the loop (we don't enter the loop body). /// - Moreover, once a `LoopArg` remains `Known`, it remains `Known` thereafter. diff --git a/protocols/src/interpreter.rs b/protocols/src/interpreter.rs index 33c6b653..abd5eb33 100644 --- a/protocols/src/interpreter.rs +++ b/protocols/src/interpreter.rs @@ -14,8 +14,8 @@ use log::info; use patronus::expr::ExprRef; use patronus::sim::{InitKind, Interpreter, Simulator}; use patronus::system::Output; -use rand::rngs::StdRng; use rand::SeedableRng; +use rand::rngs::StdRng; use rustc_hash::FxHashMap; /// Per-thread input value: either a concrete assignment or DontCare @@ -231,10 +231,9 @@ impl<'a> Evaluator<'a> { patronus::system::analysis::cone_of_influence_comb(ctx, sys, out.expr); for input_expr in input_exprs { // Find the protocol symbol corresponding to this input expression - if let Some(input_sym) = - input_mapping - .iter() - .find_map(|(k, v)| if *v == input_expr { Some(*k) } else { None }) + if let Some(input_sym) = input_mapping + .iter() + .find_map(|(k, v)| if *v == input_expr { Some(*k) } else { None }) { // output_dependencies: output -> Vec (inputs this output depends on) if let Some(vec) = output_dependencies.get_mut(out_sym) { diff --git a/protocols/src/ir.rs b/protocols/src/ir.rs index 9fb63f58..f6f7527e 100644 --- a/protocols/src/ir.rs +++ b/protocols/src/ir.rs @@ -6,7 +6,7 @@ // author: Ernest Ng use baa::BitVecValue; -use cranelift_entity::{entity_impl, PrimaryMap, SecondaryMap}; +use cranelift_entity::{PrimaryMap, SecondaryMap, entity_impl}; use itertools::Itertools; use rustc_hash::FxHashMap; use std::ops::Index; From e0075a04bec1d11427d9ce87926fac45cf938b20 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 16:30:59 -0500 Subject: [PATCH 03/19] Exit loop when LoopArg becomes Known(n) --- monitor/src/scheduler.rs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index 2b74b474..43df795b 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -1,4 +1,4 @@ -use anyhow::{Context, anyhow}; +use anyhow::{anyhow, Context}; use baa::BitVecOps; use log::info; use protocols::{ @@ -733,6 +733,9 @@ impl Scheduler { }); } Some(LoopArgState::Speculative(n, _)) => { + // Fork two threads: + // one with `Known(n)`, one with `Speculative(n + 1)` + // Create a new thread `exited_thread` that is identical // to the current thread, but it exits the loop // with the `LoopArg` set to `Known(n)` @@ -763,7 +766,14 @@ impl Scheduler { }); } Some(LoopArgState::Known(_)) => { - todo!("Handle case when `LoopArg` is `Known`") + // Exit the loop since the `LoopArg` is already known, + // proceed to the next immediate statement + // (evaluated in the next iteration + // of the outer `loop` in this function) + current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" + ); + continue; } } } From 84589926b723fc7a420ace098f7867461a54d9de Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 16:31:17 -0500 Subject: [PATCH 04/19] Formatting --- monitor/src/scheduler.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index 43df795b..524dd2f9 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -1,4 +1,4 @@ -use anyhow::{anyhow, Context}; +use anyhow::{Context, anyhow}; use baa::BitVecOps; use log::info; use protocols::{ From 0996bdaae678ea57dedd31e7a34b0cb1663a09f1 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 16:41:23 -0500 Subject: [PATCH 05/19] Add loop_arg to args_mapping when forking exit_thread --- monitor/src/scheduler.rs | 49 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 46 insertions(+), 3 deletions(-) diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index 524dd2f9..b2551b40 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -1,5 +1,5 @@ use anyhow::{Context, anyhow}; -use baa::BitVecOps; +use baa::{BitVecOps, BitVecValue}; use log::info; use protocols::{ errors::{EvaluationError, ExecutionError}, @@ -713,6 +713,26 @@ impl Scheduler { .loop_args .insert(loop_arg_symbol_id, LoopArgState::Known(0)); + // Also add the `loop_arg` to the `exited_thread`'s + // `args_mapping` and `known_bits` map. + // (The `loop_arg` is an input + // parameter, so other statements in the protocol + // can still refer to it) + let loop_arg_bitwidth = + thread.symbol_table[loop_arg_symbol_id].tpe().bitwidth(); + exited_thread + .args_mapping + .insert(loop_arg_symbol_id, BitVecValue::zero(loop_arg_bitwidth)); + exited_thread + .known_bits + .insert(loop_arg_symbol_id, BitVecValue::ones(loop_arg_bitwidth)); + + // The exited_thread needs to execute the first statement + // that immediately follow the loop + exited_thread.current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + "Repeat loops can't be the last statement in a protocol since protocols always end with `step`" + ); + // Update the current thread's `loop_args` map so that // the `LoopArg` is now `Speculative(1)` thread.loop_args.insert( @@ -720,7 +740,8 @@ impl Scheduler { LoopArgState::Speculative(1, loop_stmt_id), ); - // Execute the loop body in the current thread + // The current thread executes the + // loop body for another iteration speculatively thread.current_stmt_id = loop_body_id; // Let the global scheduler deal with both threads @@ -746,6 +767,27 @@ impl Scheduler { .loop_args .insert(loop_arg_symbol_id, LoopArgState::Known(*n)); + // Also add the `loop_arg` to the `exited_thread`'s + // `args_mapping` and `known_bits` map. + // (The `loop_arg` is an input + // parameter, so other statements in the protocol + // can still refer to it) + let loop_arg_bitwidth = + thread.symbol_table[loop_arg_symbol_id].tpe().bitwidth(); + exited_thread.args_mapping.insert( + loop_arg_symbol_id, + BitVecValue::from_u64(*n, loop_arg_bitwidth), + ); + exited_thread + .known_bits + .insert(loop_arg_symbol_id, BitVecValue::ones(loop_arg_bitwidth)); + + // The `exited_thread` needs to execute the first statement + // that immediately follows the loop + exited_thread.current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + "Repeat loops can't be the last statement in a protocol since protocols always end with `step`" + ); + // Update the current thread's `loop_args` map so that // the `LoopArg` is now `Speculative(n + 1)` thread.loop_args.insert( @@ -753,7 +795,8 @@ impl Scheduler { LoopArgState::Speculative(n + 1, loop_stmt_id), ); - // Execute the loop body in the current thread + // The current thread executes the + // loop body for another iteration speculatively thread.current_stmt_id = loop_body_id; // Let the global scheduler deal with both threads From da7824d4073af55939761b254569cdc00a00a22d Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 16:59:10 -0500 Subject: [PATCH 06/19] Refactor two cases of the RepeatLoop forking logic into a helper function --- monitor/src/scheduler.rs | 194 +++++++++++++++++++-------------------- 1 file changed, 92 insertions(+), 102 deletions(-) diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index b2551b40..6cd367c2 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -3,7 +3,7 @@ use baa::{BitVecOps, BitVecValue}; use log::info; use protocols::{ errors::{EvaluationError, ExecutionError}, - ir::{Expr, Stmt, SymbolId, SymbolTable, Transaction}, + ir::{Expr, Stmt, StmtId, SymbolId, SymbolTable, Transaction}, serialize::serialize_bitvec, }; use rustc_hash::FxHashSet; @@ -663,6 +663,81 @@ impl Scheduler { Err(error_msg) } + /// Helper function which handles `repeat` loops by forking two threads: + /// - One which exits the loop with the `LoopArg` set to `Known(n)` + /// - One which speculatively executes the loop body for another iteration, + /// with the `LoopArg` set to `Speculative(n + 1)` + /// + /// The arguments to this function are: + /// - The `SymbolId` / `StmtId`s of the `LoopArg`, loop body and the + /// entire loop statement itself + /// - The `current_thread` (which will speculatively execute the loop body + /// for another iteration) + /// - The value `n` that has been currently "guessed" for the `LoopArg` + /// + /// This function returns a `ThreadResult::RepeatLoopFork` containing the + /// two threads. + fn handle_repeat_loops( + &mut self, + loop_arg_symbol_id: SymbolId, + loop_body_id: StmtId, + loop_stmt_id: StmtId, + mut current_thread: Thread, + n: u64, + ) -> ThreadResult { + // Create a new thread `exited_thread` that is identical + // to the current thread, but it exits the loop + // with the `LoopArg` set to `Known(n)` + let mut exited_thread = current_thread.clone(); + exited_thread.thread_id = self.num_threads; + self.num_threads += 1; + exited_thread + .loop_args + .insert(loop_arg_symbol_id, LoopArgState::Known(n)); + + // Also add the `loop_arg` to the `exited_thread`'s + // `args_mapping` and `known_bits` map. + // (The `loop_arg` is an input + // parameter, so other statements in the protocol + // can still refer to it) + let loop_arg_bitwidth = current_thread.symbol_table[loop_arg_symbol_id] + .tpe() + .bitwidth(); + exited_thread.args_mapping.insert( + loop_arg_symbol_id, + BitVecValue::from_u64(n, loop_arg_bitwidth), + ); + exited_thread + .known_bits + .insert(loop_arg_symbol_id, BitVecValue::ones(loop_arg_bitwidth)); + + // The exited_thread needs to execute the first statement + // that immediately follow the loop + exited_thread.current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + "Repeat loops can't be the last statement in a protocol since protocols always end with `step`" + ); + + // Update the current thread's `loop_args` map so that + // the `LoopArg` is now `Speculative(n + 1)` + current_thread.loop_args.insert( + loop_arg_symbol_id, + LoopArgState::Speculative(n + 1, loop_stmt_id), + ); + + // The current thread executes the + // loop body for another iteration speculatively + current_thread.current_stmt_id = loop_body_id; + + // Let the global scheduler deal with both threads + // (The current thread is called the `speculative_thread`, + // since it speculatively executes the loop body again + // with the `LoopArg` set to `Speculative(n + 1)`) + ThreadResult::RepeatLoopFork { + exited_thread: Box::new(exited_thread), + speculative_thread: Box::new(current_thread), + } + } + /// Keeps running a `thread` until: /// - It reaches the next `step()` or `fork()` statement /// - It completes succesfully @@ -698,115 +773,30 @@ impl Scheduler { } }; - match thread.loop_args.get(&loop_arg_symbol_id) { + match thread.loop_args.get(&loop_arg_symbol_id).cloned() { None => { // First time seeing loop arg, it is `Unknown` - // (i.e. absent from the thread's `loop_args` map) - - // Create a new thread `exited_thread` that is identical - // to the current thread, but it exits the loop - // with the `LoopArg` set to `Known(0)` - let mut exited_thread = thread.clone(); - exited_thread.thread_id = self.num_threads; - self.num_threads += 1; - exited_thread - .loop_args - .insert(loop_arg_symbol_id, LoopArgState::Known(0)); - - // Also add the `loop_arg` to the `exited_thread`'s - // `args_mapping` and `known_bits` map. - // (The `loop_arg` is an input - // parameter, so other statements in the protocol - // can still refer to it) - let loop_arg_bitwidth = - thread.symbol_table[loop_arg_symbol_id].tpe().bitwidth(); - exited_thread - .args_mapping - .insert(loop_arg_symbol_id, BitVecValue::zero(loop_arg_bitwidth)); - exited_thread - .known_bits - .insert(loop_arg_symbol_id, BitVecValue::ones(loop_arg_bitwidth)); - - // The exited_thread needs to execute the first statement - // that immediately follow the loop - exited_thread.current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( - "Repeat loops can't be the last statement in a protocol since protocols always end with `step`" - ); - - // Update the current thread's `loop_args` map so that - // the `LoopArg` is now `Speculative(1)` - thread.loop_args.insert( + // (i.e. absent from the thread's `loop_args` map), + // so pass in `n = 0` to the `handle_repeat_loops` + // helper function + return Ok(self.handle_repeat_loops( loop_arg_symbol_id, - LoopArgState::Speculative(1, loop_stmt_id), - ); - - // The current thread executes the - // loop body for another iteration speculatively - thread.current_stmt_id = loop_body_id; - - // Let the global scheduler deal with both threads - // (The current thread is called the `speculative_thread`, - // since it speculatively executes the loop body again - // with the `LoopArg` set to `Speculative(1)`) - return Ok(ThreadResult::RepeatLoopFork { - exited_thread: Box::new(exited_thread), - speculative_thread: Box::new(thread), - }); + loop_body_id, + loop_stmt_id, + thread, + 0, + )); } Some(LoopArgState::Speculative(n, _)) => { // Fork two threads: // one with `Known(n)`, one with `Speculative(n + 1)` - - // Create a new thread `exited_thread` that is identical - // to the current thread, but it exits the loop - // with the `LoopArg` set to `Known(n)` - let mut exited_thread = thread.clone(); - exited_thread.thread_id = self.num_threads; - self.num_threads += 1; - exited_thread - .loop_args - .insert(loop_arg_symbol_id, LoopArgState::Known(*n)); - - // Also add the `loop_arg` to the `exited_thread`'s - // `args_mapping` and `known_bits` map. - // (The `loop_arg` is an input - // parameter, so other statements in the protocol - // can still refer to it) - let loop_arg_bitwidth = - thread.symbol_table[loop_arg_symbol_id].tpe().bitwidth(); - exited_thread.args_mapping.insert( - loop_arg_symbol_id, - BitVecValue::from_u64(*n, loop_arg_bitwidth), - ); - exited_thread - .known_bits - .insert(loop_arg_symbol_id, BitVecValue::ones(loop_arg_bitwidth)); - - // The `exited_thread` needs to execute the first statement - // that immediately follows the loop - exited_thread.current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( - "Repeat loops can't be the last statement in a protocol since protocols always end with `step`" - ); - - // Update the current thread's `loop_args` map so that - // the `LoopArg` is now `Speculative(n + 1)` - thread.loop_args.insert( + return Ok(self.handle_repeat_loops( loop_arg_symbol_id, - LoopArgState::Speculative(n + 1, loop_stmt_id), - ); - - // The current thread executes the - // loop body for another iteration speculatively - thread.current_stmt_id = loop_body_id; - - // Let the global scheduler deal with both threads - // (The current thread is called the `speculative_thread`, - // since it speculatively executes the loop body again - // with the `LoopArg` set to `Speculative(1)`) - return Ok(ThreadResult::RepeatLoopFork { - exited_thread: Box::new(exited_thread), - speculative_thread: Box::new(thread), - }); + loop_body_id, + loop_stmt_id, + thread, + n, + )); } Some(LoopArgState::Known(_)) => { // Exit the loop since the `LoopArg` is already known, From 4ff13e69b9a66947dfe44f6ae8e784bdcec20602 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 17:43:58 -0500 Subject: [PATCH 07/19] Handle case when multiple loops use the same loop arg --- monitor/src/interpreter.rs | 2 +- monitor/src/scheduler.rs | 60 +++++++++++++++++++++++++++++--------- monitor/src/thread.rs | 17 +++++++++-- 3 files changed, 61 insertions(+), 18 deletions(-) diff --git a/monitor/src/interpreter.rs b/monitor/src/interpreter.rs index d691c934..dd5e6068 100644 --- a/monitor/src/interpreter.rs +++ b/monitor/src/interpreter.rs @@ -99,7 +99,7 @@ impl Interpreter { self.known_bits = thread.known_bits.clone(); self.constraints = thread.constraints.clone(); self.args_to_pins = thread.args_to_pins.clone(); - self.loop_args = thread.loop_args.clone(); + self.loop_args = thread.loop_args_state.clone(); } /// Pretty-prints a `Statement` identified by its `StmtId` diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index 6cd367c2..d8ef4a2b 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -692,7 +692,7 @@ impl Scheduler { exited_thread.thread_id = self.num_threads; self.num_threads += 1; exited_thread - .loop_args + .loop_args_state .insert(loop_arg_symbol_id, LoopArgState::Known(n)); // Also add the `loop_arg` to the `exited_thread`'s @@ -719,7 +719,7 @@ impl Scheduler { // Update the current thread's `loop_args` map so that // the `LoopArg` is now `Speculative(n + 1)` - current_thread.loop_args.insert( + current_thread.loop_args_state.insert( loop_arg_symbol_id, LoopArgState::Speculative(n + 1, loop_stmt_id), ); @@ -768,15 +768,57 @@ impl Scheduler { let loop_stmt_id = current_stmt_id; let loop_arg_symbol_id = match thread.transaction[loop_arg_expr_id] { Expr::Sym(symbol_id) => symbol_id, + Expr::Const(_) => { + todo!("Maybe allow constants to appear as arguments to repeat loops??") + } _ => { unreachable!("Arguments to repeat loops are always SymbolIDs") } }; - match thread.loop_args.get(&loop_arg_symbol_id).cloned() { + // Suppose we already know how many iterations a `repeat` loop + // must take. If so, we execute it deterministically. + // This situation occurs if there are multiple `repeat` loops + // in a protocol that use the same `LoopArg`, e.g. + // `repeat n iterations { ... }; ...; repeat n iterations { ... }` + if let Some(num_remaining_iters) = + thread.repeat_loops_remaining_iters.get_mut(&loop_stmt_id) + { + *num_remaining_iters -= 1; + if *num_remaining_iters == 0 { + thread.repeat_loops_remaining_iters.remove(&loop_stmt_id); + current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" + ); + } else { + current_stmt_id = loop_body_id; + } + continue; + } + + // Now we need to handle the case when the value of a `LoopArg` + // is unknown + match thread.loop_args_state.get(&loop_arg_symbol_id).cloned() { + Some(LoopArgState::Known(n)) => { + // Value of `n` has been resolved from a prior loop + // (either with the same `StmtId` or a different `StmtId`) + if n == 0 { + // Exit the loop since the `LoopArg` is already known, + // proceed to the next immediate statement + // (evaluated in the next iteration + // of the outer `loop` in this function) + current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" + ); + } else { + thread.repeat_loops_remaining_iters.insert(loop_stmt_id, n); + current_stmt_id = loop_body_id; + } + continue; + } None => { // First time seeing loop arg, it is `Unknown` - // (i.e. absent from the thread's `loop_args` map), + // (i.e. absent from the thread's `loop_args_state` map), // so pass in `n = 0` to the `handle_repeat_loops` // helper function return Ok(self.handle_repeat_loops( @@ -798,16 +840,6 @@ impl Scheduler { n, )); } - Some(LoopArgState::Known(_)) => { - // Exit the loop since the `LoopArg` is already known, - // proceed to the next immediate statement - // (evaluated in the next iteration - // of the outer `loop` in this function) - current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( - "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" - ); - continue; - } } } match self.interpreter.evaluate_stmt(¤t_stmt_id, ctx, trace) { diff --git a/monitor/src/thread.rs b/monitor/src/thread.rs index f617cf22..315b67ba 100644 --- a/monitor/src/thread.rs +++ b/monitor/src/thread.rs @@ -62,8 +62,18 @@ pub struct Thread { /// Maps function parameters to DUT ports pub args_to_pins: FxHashMap, - /// Maps arguments of `repeat` loops to their current state - pub loop_args: FxHashMap, + /// Maps arguments of `repeat` loops to their current "guessed" state + /// (either `Speculative` or `Known` -- see docs for the `LoopArgState` type) + pub loop_args_state: FxHashMap, + + /// Once the state of a `LoopArg` has been determined, we need to track + /// how many iterations remain to be executed -- this is most useful + /// if we have two loops that use the same `LoopArg`, e.g. + /// `repeat n iterations { ... }; ...; repeat n iterations { ...}`. + /// This map is populated lazily when we encounter each `repeat` loop + /// (see `Scheduler::run_thread_till_next_step`). + /// The `StmtId` key is the statement of the `repeat` loop. + pub repeat_loops_remaining_iters: FxHashMap, /// Determines if the thread has called `fork()` yet. Initialized to `false`. /// Since well-formedness dicates that a protocol can only contain @@ -120,7 +130,8 @@ impl Thread { start_time_step, args_to_pins: FxHashMap::default(), has_forked: false, - loop_args: FxHashMap::default(), + loop_args_state: FxHashMap::default(), + repeat_loops_remaining_iters: FxHashMap::default(), } } From 4af2f9915785e5f3b71be2fc0dba04d52cc60aff Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 17:53:23 -0500 Subject: [PATCH 08/19] Disallow nested repeat loops that use the same loop arg --- monitor/src/scheduler.rs | 49 +++++++++++++++++++++++++--------------- 1 file changed, 31 insertions(+), 18 deletions(-) diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index d8ef4a2b..3e79e9fd 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -799,23 +799,6 @@ impl Scheduler { // Now we need to handle the case when the value of a `LoopArg` // is unknown match thread.loop_args_state.get(&loop_arg_symbol_id).cloned() { - Some(LoopArgState::Known(n)) => { - // Value of `n` has been resolved from a prior loop - // (either with the same `StmtId` or a different `StmtId`) - if n == 0 { - // Exit the loop since the `LoopArg` is already known, - // proceed to the next immediate statement - // (evaluated in the next iteration - // of the outer `loop` in this function) - current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( - "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" - ); - } else { - thread.repeat_loops_remaining_iters.insert(loop_stmt_id, n); - current_stmt_id = loop_body_id; - } - continue; - } None => { // First time seeing loop arg, it is `Unknown` // (i.e. absent from the thread's `loop_args_state` map), @@ -829,7 +812,17 @@ impl Scheduler { 0, )); } - Some(LoopArgState::Speculative(n, _)) => { + Some(LoopArgState::Speculative(n, stored_loop_stmt_id)) => { + // We disallow nested `repeat` loops that use the + // same loop argument, i.e. we forbid + // `repeat n iterations { repeat n iterations { ... } ... }` + if loop_stmt_id != stored_loop_stmt_id { + panic!( + "Nested `repeat` loops that use the same loop argument `{}` are forbidden", + thread.symbol_table[loop_arg_symbol_id].name() + ) + } + // Fork two threads: // one with `Known(n)`, one with `Speculative(n + 1)` return Ok(self.handle_repeat_loops( @@ -840,6 +833,26 @@ impl Scheduler { n, )); } + Some(LoopArgState::Known(n)) => { + // Value of `n` has been resolved from a prior loop + // (either with the same `StmtId` or a different `StmtId`) + if n == 0 { + // Exit the loop since the `LoopArg` is already known, + // proceed to the next immediate statement + // (evaluated in the next iteration + // of the outer `loop` in this function) + current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" + ); + } else { + // Insert it into the thread's `repeat_loops_remaining_iters` + // map, which tracks how many iterations need to be executed + // for this loop + thread.repeat_loops_remaining_iters.insert(loop_stmt_id, n); + current_stmt_id = loop_body_id; + } + continue; + } } } match self.interpreter.evaluate_stmt(¤t_stmt_id, ctx, trace) { From cd0bc93f87815c3bed8de9ec8237f9e64f670987 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 18:05:59 -0500 Subject: [PATCH 09/19] Run Cargo in Quiet mode when running Snapshot Tests --- examples/turnt.toml | 2 +- protocols/tests/turnt.toml | 2 +- turnt.toml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/turnt.toml b/examples/turnt.toml index 8c08bf47..4854c84b 100644 --- a/examples/turnt.toml +++ b/examples/turnt.toml @@ -1,2 +1,2 @@ [envs.interp] -command = "cargo run --package protocols-interp -- --color never --transactions {filename} {args}" +command = "cargo run --quiet --package protocols-interp -- --color never --transactions {filename} {args}" diff --git a/protocols/tests/turnt.toml b/protocols/tests/turnt.toml index 8c08bf47..4854c84b 100644 --- a/protocols/tests/turnt.toml +++ b/protocols/tests/turnt.toml @@ -1,2 +1,2 @@ [envs.interp] -command = "cargo run --package protocols-interp -- --color never --transactions {filename} {args}" +command = "cargo run --quiet --package protocols-interp -- --color never --transactions {filename} {args}" diff --git a/turnt.toml b/turnt.toml index 70a5c157..7c87759f 100644 --- a/turnt.toml +++ b/turnt.toml @@ -1 +1 @@ -command = "cargo run --package protocols-interp -- --color never --transactions {filename} {args}" +command = "cargo run --quiet --package protocols-interp -- --color never --transactions {filename} {args}" From 8c296ef464b258394000418a0959f83662a48b9c Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 18:11:03 -0500 Subject: [PATCH 10/19] Add Cargo aliases --- .cargo/config.toml | 3 +++ .gitignore | 7 +++---- 2 files changed, 6 insertions(+), 4 deletions(-) create mode 100644 .cargo/config.toml diff --git a/.cargo/config.toml b/.cargo/config.toml new file mode 100644 index 00000000..05025a9c --- /dev/null +++ b/.cargo/config.toml @@ -0,0 +1,3 @@ +[alias] +interp = "run --quiet --package protocols-interp --" +monitor = "run --quiet --package protocols-monitor --" diff --git a/.gitignore b/.gitignore index 47672ecb..5cc08d2d 100644 --- a/.gitignore +++ b/.gitignore @@ -4,8 +4,6 @@ Cargo.lock test_run/ *.btor **/.DS_Store -.vscode/* -.surfer/ monitor/target monitor/tests/axi_output.txt *.json @@ -18,6 +16,7 @@ monitor/tests/axi_output.txt # But include the .github directory (CI files) !.github/ !.github/**/* -# And also include .gitignore + .python-version +# And also include .gitignore + .python-version + Cargo config !.gitignore -!.python-version \ No newline at end of file +!.python-version +!.cargo From bca2aa1fd395bc9aea29f890648acefe0fae3b71 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 18:14:41 -0500 Subject: [PATCH 11/19] Update various Turnt.toml files to use Cargo aliases --- examples/turnt.toml | 2 +- monitor/tests/turnt.toml | 2 +- protocols/tests/turnt.toml | 2 +- turnt.toml | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/examples/turnt.toml b/examples/turnt.toml index 4854c84b..68a576a6 100644 --- a/examples/turnt.toml +++ b/examples/turnt.toml @@ -1,2 +1,2 @@ [envs.interp] -command = "cargo run --quiet --package protocols-interp -- --color never --transactions {filename} {args}" +command = "cargo interp --color never --transactions {filename} {args}" diff --git a/monitor/tests/turnt.toml b/monitor/tests/turnt.toml index 6b85ef21..ebe5dde3 100644 --- a/monitor/tests/turnt.toml +++ b/monitor/tests/turnt.toml @@ -1,7 +1,7 @@ # We run Cargo in quiet mode to prevent build messages from # appearing in the output for Turnt tests [envs.monitor] -command = "cargo run --quiet --package protocols-monitor -- -p {filename} {args}" +command = "cargo monitor -p {filename} {args}" output.out = "-" output.err = "2" diff --git a/protocols/tests/turnt.toml b/protocols/tests/turnt.toml index 4854c84b..68a576a6 100644 --- a/protocols/tests/turnt.toml +++ b/protocols/tests/turnt.toml @@ -1,2 +1,2 @@ [envs.interp] -command = "cargo run --quiet --package protocols-interp -- --color never --transactions {filename} {args}" +command = "cargo interp --color never --transactions {filename} {args}" diff --git a/turnt.toml b/turnt.toml index 7c87759f..895f5f9c 100644 --- a/turnt.toml +++ b/turnt.toml @@ -1 +1 @@ -command = "cargo run --quiet --package protocols-interp -- --color never --transactions {filename} {args}" +command = "cargo interp --color never --transactions {filename} {args}" From 7a70e62f4f4065a664dab2066ebf1b2a0bf6cc38 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 23:44:36 -0500 Subject: [PATCH 12/19] Add adder_d1 repeat loop tests --- monitor/tests/adders/busy_wait.out | 0 monitor/tests/adders/busy_wait.prof | 0 monitor/tests/adders/busy_wait.prot | 29 +++++++++++++++++++++ monitor/tests/adders/loop_with_assigns.out | 0 monitor/tests/adders/loop_with_assigns.prof | 0 monitor/tests/adders/loop_with_assigns.prot | 22 ++++++++++++++++ monitor/tests/adders/nested_busy_wait.out | 0 monitor/tests/adders/nested_busy_wait.prof | 0 monitor/tests/adders/nested_busy_wait.prot | 28 ++++++++++++++++++++ 9 files changed, 79 insertions(+) create mode 100644 monitor/tests/adders/busy_wait.out create mode 100644 monitor/tests/adders/busy_wait.prof create mode 100644 monitor/tests/adders/busy_wait.prot create mode 100644 monitor/tests/adders/loop_with_assigns.out create mode 100644 monitor/tests/adders/loop_with_assigns.prof create mode 100644 monitor/tests/adders/loop_with_assigns.prot create mode 100644 monitor/tests/adders/nested_busy_wait.out create mode 100644 monitor/tests/adders/nested_busy_wait.prof create mode 100644 monitor/tests/adders/nested_busy_wait.prot diff --git a/monitor/tests/adders/busy_wait.out b/monitor/tests/adders/busy_wait.out new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/busy_wait.prof b/monitor/tests/adders/busy_wait.prof new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/busy_wait.prot b/monitor/tests/adders/busy_wait.prot new file mode 100644 index 00000000..08c6fa3e --- /dev/null +++ b/monitor/tests/adders/busy_wait.prot @@ -0,0 +1,29 @@ +// Maps to a Verilog design +struct Adder { + in a: u32, + in b: u32, + out s: u32, +} + +// Uses a bounded loop that busy-waits for `num_iters` cycles. +// Since concrete assignments to DUT input ports persist, +// calling `step()` multiple times in the loop with the same inputs +// should still produce the correct result on the adder. (This allows us to +// reuse the same Verilog file as the other `adder_d1` tests.) +prot add_busy_wait(in a: u32, in b: u32, in num_iters: u8, out s: u32) { + DUT.a := a; + DUT.b := b; + // We want `assert_eq(s, DUT.s)` to hold for every iteration of this loop, + // so we cannot put `DUT.a := X; DUT.b := X` in the loop body, since + // that would cause the `assert_eq` to fail on later iterations of the loop + repeat num_iters iterations { + step(); + assert_eq(s, DUT.s); + } + DUT.a := X; + DUT.b := X; + // Ensure `s = a + b` still holds when we exit the loop + assert_eq(s, DUT.s); + fork(); + step(); +} diff --git a/monitor/tests/adders/loop_with_assigns.out b/monitor/tests/adders/loop_with_assigns.out new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/loop_with_assigns.prof b/monitor/tests/adders/loop_with_assigns.prof new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/loop_with_assigns.prot b/monitor/tests/adders/loop_with_assigns.prot new file mode 100644 index 00000000..589267e3 --- /dev/null +++ b/monitor/tests/adders/loop_with_assigns.prot @@ -0,0 +1,22 @@ +struct Adder { + in a: u32, + in b: u32, + out s: u32, +} + +// Each iteration of the loop performs the full add protocol: +// assign inputs -> step -> release inputs -> assert output +// This tests that assignments, DontCare releases, and assertions +// all work correctly inside a bounded loop body. +prot loop_add(in a: u32, in b: u32, in num_iters: u8, out s: u32) { + repeat num_iters iterations { + DUT.a := a; + DUT.b := b; + step(); + DUT.a := X; + DUT.b := X; + assert_eq(s, DUT.s); + } + fork(); + step(); +} diff --git a/monitor/tests/adders/nested_busy_wait.out b/monitor/tests/adders/nested_busy_wait.out new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/nested_busy_wait.prof b/monitor/tests/adders/nested_busy_wait.prof new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/nested_busy_wait.prot b/monitor/tests/adders/nested_busy_wait.prot new file mode 100644 index 00000000..fbb465f9 --- /dev/null +++ b/monitor/tests/adders/nested_busy_wait.prot @@ -0,0 +1,28 @@ +struct Adder { + in a: u32, + in b: u32, + out s: u32, +} + +// Nested bounded loops: the outer loop runs `outer_iters` times, +// and the inner loop runs `inner_iters` times per outer iteration, +// for a total of `outer_iters * inner_iters` steps. +// Since inputs are sticky on the adder, the final result is +// the same regardless of how many steps we take. +prot nested_busy_wait(in a: u32, in b: u32, in outer_iters: u8, in inner_iters: u8, out s: u32) { + DUT.a := a; + DUT.b := b; + repeat outer_iters iterations { + repeat inner_iters iterations { + step(); + assert_eq(s, DUT.s); + } + step(); + assert_eq(s, DUT.s); + } + DUT.a := X; + DUT.b := X; + assert_eq(s, DUT.s); + fork(); + step(); +} From 2c7009d40a87605fa1a39b424f590c752443df2f Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 23:52:13 -0500 Subject: [PATCH 13/19] Add adder_d1 loop waveform files --- monitor/tests/adders/busy_wait.fst | Bin 0 -> 611 bytes monitor/tests/adders/loop_with_assigns.fst | Bin 0 -> 606 bytes monitor/tests/adders/nested_busy_wait.fst | Bin 0 -> 618 bytes 3 files changed, 0 insertions(+), 0 deletions(-) create mode 100644 monitor/tests/adders/busy_wait.fst create mode 100644 monitor/tests/adders/loop_with_assigns.fst create mode 100644 monitor/tests/adders/nested_busy_wait.fst diff --git a/monitor/tests/adders/busy_wait.fst b/monitor/tests/adders/busy_wait.fst new file mode 100644 index 0000000000000000000000000000000000000000..4349baaf766ddf5508878b65b32932a012c597e5 GIT binary patch literal 611 zcmZQz00Tx(2n{D$GQ&l>x%RUJjb>yBNGvJJ&nqofD6T9nNzGNr%qvMP zDkw??l4xcOPc9qOTc%K2yX7B4VoFMUiXl70L;;3G1_cHIh9owI3&}az42(c_F;L_` zGgP$Bg4xVWK#G%@mx&kZ MA{Is literal 0 HcmV?d00001 diff --git a/monitor/tests/adders/loop_with_assigns.fst b/monitor/tests/adders/loop_with_assigns.fst new file mode 100644 index 0000000000000000000000000000000000000000..b3babd9d06b55bd3a8a98cf42ac0318cae8283b4 GIT binary patch literal 606 zcmZQz00Tx(2n{D$GQ&l>x%RUJjb>yBNGvJJ&nqofD6T9nNzGNr%qvMP zDkw??l4xcOPc9qOTc%K2yX7B4VoFMUiXl70L;;3G1_cHIh9owI3&}az42(c_F;L_` zGgP$Jjb>yBNGvJJ&nqofD6T9nNzGNr%qvMP zDkw??l4xcOPc9qOTc%K2yX7B4VoFMUiXl70L;;3G1_cHIh9owI3&}az42(c_F;L_` zGgP$nE-)zqwwYM~NXaqt bGVwwk!cq~JoZV#F^e literal 0 HcmV?d00001 From c8a42e05f7f771878a2572621c4fccad49acf66e Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Fri, 20 Feb 2026 23:52:22 -0500 Subject: [PATCH 14/19] Add Turnt args to adder_d1 loop tests --- monitor/tests/adders/busy_wait.err | 0 monitor/tests/adders/busy_wait.out | 28 +++++++++++++++++++++ monitor/tests/adders/busy_wait.prot | 4 +-- monitor/tests/adders/loop_with_assigns.prot | 3 ++- monitor/tests/adders/nested_busy_wait.prot | 3 ++- 5 files changed, 34 insertions(+), 4 deletions(-) create mode 100644 monitor/tests/adders/busy_wait.err diff --git a/monitor/tests/adders/busy_wait.err b/monitor/tests/adders/busy_wait.err new file mode 100644 index 00000000..e69de29b diff --git a/monitor/tests/adders/busy_wait.out b/monitor/tests/adders/busy_wait.out index e69de29b..649dcd68 100644 --- a/monitor/tests/adders/busy_wait.out +++ b/monitor/tests/adders/busy_wait.out @@ -0,0 +1,28 @@ +// trace 0 +trace { + add_busy_wait(1, 2, 0, 0); +} + +// trace 1 +trace { + add_busy_wait(4, 5, 3, 3); +} + +// trace 2 +trace { + add_busy_wait(1, 2, 1, 3); + add_busy_wait(4, 5, 2, 9); +} + +// trace 3 +trace { + add_busy_wait(4, 5, 2, 3); + add_busy_wait(4, 5, 1, 9); +} + +// trace 4 +trace { + add_busy_wait(1, 2, 1, 3); + add_busy_wait(4, 5, 1, 9); + add_busy_wait(4, 5, 1, 9); +} diff --git a/monitor/tests/adders/busy_wait.prot b/monitor/tests/adders/busy_wait.prot index 08c6fa3e..289df726 100644 --- a/monitor/tests/adders/busy_wait.prot +++ b/monitor/tests/adders/busy_wait.prot @@ -1,4 +1,4 @@ -// Maps to a Verilog design +// ARGS: --wave adders/busy_wait.fst --instances add_d1:Adder struct Adder { in a: u32, in b: u32, @@ -10,7 +10,7 @@ struct Adder { // calling `step()` multiple times in the loop with the same inputs // should still produce the correct result on the adder. (This allows us to // reuse the same Verilog file as the other `adder_d1` tests.) -prot add_busy_wait(in a: u32, in b: u32, in num_iters: u8, out s: u32) { +prot add_busy_wait(in a: u32, in b: u32, in num_iters: u64, out s: u32) { DUT.a := a; DUT.b := b; // We want `assert_eq(s, DUT.s)` to hold for every iteration of this loop, diff --git a/monitor/tests/adders/loop_with_assigns.prot b/monitor/tests/adders/loop_with_assigns.prot index 589267e3..c933237f 100644 --- a/monitor/tests/adders/loop_with_assigns.prot +++ b/monitor/tests/adders/loop_with_assigns.prot @@ -1,3 +1,4 @@ +// ARGS: --wave adders/loop_with_assigns.fst --instances add_d1:Adder struct Adder { in a: u32, in b: u32, @@ -8,7 +9,7 @@ struct Adder { // assign inputs -> step -> release inputs -> assert output // This tests that assignments, DontCare releases, and assertions // all work correctly inside a bounded loop body. -prot loop_add(in a: u32, in b: u32, in num_iters: u8, out s: u32) { +prot loop_add(in a: u32, in b: u32, in num_iters: u64, out s: u32) { repeat num_iters iterations { DUT.a := a; DUT.b := b; diff --git a/monitor/tests/adders/nested_busy_wait.prot b/monitor/tests/adders/nested_busy_wait.prot index fbb465f9..2c0e4a15 100644 --- a/monitor/tests/adders/nested_busy_wait.prot +++ b/monitor/tests/adders/nested_busy_wait.prot @@ -1,3 +1,4 @@ +// ARGS: --wave adders/nested_busy_wait.fst --instances add_d1:Adder struct Adder { in a: u32, in b: u32, @@ -9,7 +10,7 @@ struct Adder { // for a total of `outer_iters * inner_iters` steps. // Since inputs are sticky on the adder, the final result is // the same regardless of how many steps we take. -prot nested_busy_wait(in a: u32, in b: u32, in outer_iters: u8, in inner_iters: u8, out s: u32) { +prot nested_busy_wait(in a: u32, in b: u32, in outer_iters: u64, in inner_iters: u64, out s: u32) { DUT.a := a; DUT.b := b; repeat outer_iters iterations { From c261d2a85984c3c215251125266261ddbc1334e3 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sat, 21 Feb 2026 14:30:55 -0500 Subject: [PATCH 15/19] Make Interpreter::to_protocol_application return an option --- monitor/src/interpreter.rs | 23 +++++++++++++---------- monitor/src/scheduler.rs | 17 +++++++++++++++-- 2 files changed, 28 insertions(+), 12 deletions(-) diff --git a/monitor/src/interpreter.rs b/monitor/src/interpreter.rs index dd5e6068..915ed271 100644 --- a/monitor/src/interpreter.rs +++ b/monitor/src/interpreter.rs @@ -51,7 +51,7 @@ pub struct Interpreter { } impl Interpreter { - /// Builds a `ProtocolApplication` from the current interpreter state. + /// Attempts to builds a `ProtocolApplication` from the current interpreter state. /// `struct_name` is left as `None` — the caller (Scheduler) is responsible /// for setting it, since the Interpreter doesn't know the struct name. pub fn to_protocol_application( @@ -59,33 +59,36 @@ impl Interpreter { struct_name: Option, ctx: &GlobalContext, trace: &WaveSignalTrace, - ) -> ProtocolApplication { + ) -> Option { let mut serialized_args = vec![]; for arg in &self.transaction.args { let symbol_id = arg.symbol(); - let name = self.symbol_table[symbol_id].full_name(&self.symbol_table); - let value = self.args_mapping.get(&symbol_id).unwrap_or_else(|| { + let value_opt = self.args_mapping.get(&symbol_id); + if let Some(value) = value_opt { + serialized_args.push(serialize_bitvec(value, ctx.display_hex)); + } else { + let name = self.symbol_table[symbol_id].full_name(&self.symbol_table); let time_str = if ctx.show_waveform_time { trace.format_time(trace.time_step(), ctx.time_unit) } else { format!("cycle {}", self.trace_cycle_count) }; - panic!( + info!( "Transaction `{}`, {}: Unable to find value for {} ({}) in args_mapping, which is {{ {} }}", self.transaction.name, time_str, name, symbol_id, serialize_args_mapping(&self.args_mapping, &self.symbol_table, ctx.display_hex) - ) - }); - serialized_args.push(serialize_bitvec(value, ctx.display_hex)); + ); + return None; + } } - ProtocolApplication { + Some(ProtocolApplication { struct_name, protocol_name: self.transaction.name.clone(), serialized_args, - } + }) } /// Performs a context switch in the `Interpreter` by setting its diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index 3e79e9fd..72822263 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -973,10 +973,22 @@ impl Scheduler { None }; let is_idle = self.interpreter.transaction.is_idle; - let protocol_application = + + let prot_app_opt = self.interpreter .to_protocol_application(struct_name, ctx, trace); + if prot_app_opt.is_none() { + info!( + "Unable to construct protocol application for thread {} (`{}`), marking thread as failed", + thread.global_thread_id(ctx), + self.format_transaction_name(ctx, thread.transaction.name.clone()) + ); + self.failed.push_back(thread.clone()); + self.print_scheduler_state(trace, ctx); + return Ok(ThreadResult::Completed); + } + if is_idle { info!( "Transaction `{}` is marked as idle", @@ -988,7 +1000,8 @@ impl Scheduler { // output buffer self.output_buffer.push(AugmentedProtocolApplication { end_cycle_count: self.cycle_count, - protocol_application, + protocol_application: prot_app_opt + .expect("Expected Some(ProtocolApplication)"), start_time_step: thread.start_time_step, end_time_step, thread_id: thread.global_thread_id(ctx), From 68d44bad95ac5165811e451c06927be6cbc47715 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sat, 21 Feb 2026 14:31:08 -0500 Subject: [PATCH 16/19] Add expected output for two adder_d1 tests with loops --- monitor/tests/adders/busy_wait.out | 27 ++-------------------- monitor/tests/adders/loop_with_assigns.out | 5 ++++ 2 files changed, 7 insertions(+), 25 deletions(-) diff --git a/monitor/tests/adders/busy_wait.out b/monitor/tests/adders/busy_wait.out index 649dcd68..95a94f09 100644 --- a/monitor/tests/adders/busy_wait.out +++ b/monitor/tests/adders/busy_wait.out @@ -1,28 +1,5 @@ // trace 0 trace { - add_busy_wait(1, 2, 0, 0); -} - -// trace 1 -trace { - add_busy_wait(4, 5, 3, 3); -} - -// trace 2 -trace { - add_busy_wait(1, 2, 1, 3); - add_busy_wait(4, 5, 2, 9); -} - -// trace 3 -trace { - add_busy_wait(4, 5, 2, 3); - add_busy_wait(4, 5, 1, 9); -} - -// trace 4 -trace { - add_busy_wait(1, 2, 1, 3); - add_busy_wait(4, 5, 1, 9); - add_busy_wait(4, 5, 1, 9); + add_busy_wait(1, 2, 1, 3); + add_busy_wait(4, 5, 3, 9); } diff --git a/monitor/tests/adders/loop_with_assigns.out b/monitor/tests/adders/loop_with_assigns.out index e69de29b..21c26b8a 100644 --- a/monitor/tests/adders/loop_with_assigns.out +++ b/monitor/tests/adders/loop_with_assigns.out @@ -0,0 +1,5 @@ +// trace 0 +trace { + loop_add(1, 2, 3, 3); + loop_add(10, 20, 1, 30); +} \ No newline at end of file From d903d7a62b9267351637a4da58cfce79c7f0ec1d Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sat, 21 Feb 2026 14:33:12 -0500 Subject: [PATCH 17/19] Optimize Interpreter::to_protocol_application --- monitor/src/interpreter.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/monitor/src/interpreter.rs b/monitor/src/interpreter.rs index 915ed271..bf95722a 100644 --- a/monitor/src/interpreter.rs +++ b/monitor/src/interpreter.rs @@ -54,6 +54,10 @@ impl Interpreter { /// Attempts to builds a `ProtocolApplication` from the current interpreter state. /// `struct_name` is left as `None` — the caller (Scheduler) is responsible /// for setting it, since the Interpreter doesn't know the struct name. + /// If this return function returns `None` (e.g. because an argument + /// wasn't present in `args_mapping`), the caller + /// (`Scheduler::run_thread_till_next_step`) treats the corresponding thread + /// as having failed. pub fn to_protocol_application( &self, struct_name: Option, @@ -63,8 +67,7 @@ impl Interpreter { let mut serialized_args = vec![]; for arg in &self.transaction.args { let symbol_id = arg.symbol(); - let value_opt = self.args_mapping.get(&symbol_id); - if let Some(value) = value_opt { + if let Some(value) = self.args_mapping.get(&symbol_id) { serialized_args.push(serialize_bitvec(value, ctx.display_hex)); } else { let name = self.symbol_table[symbol_id].full_name(&self.symbol_table); From 16670829112c883e6262c15fec34fa6b65e3ca88 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sat, 21 Feb 2026 15:33:16 -0500 Subject: [PATCH 18/19] Intercept fork before handling other statements --- monitor/src/scheduler.rs | 251 ++++++++++++++++++++------------------- 1 file changed, 129 insertions(+), 122 deletions(-) diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index 72822263..8dfab492 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -714,8 +714,8 @@ impl Scheduler { // The exited_thread needs to execute the first statement // that immediately follow the loop exited_thread.current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( - "Repeat loops can't be the last statement in a protocol since protocols always end with `step`" - ); + "Repeat loops can't be the last statement in a protocol since protocols always end with `step`" + ); // Update the current thread's `loop_args` map so that // the `LoopArg` is now `Speculative(n + 1)` @@ -761,99 +761,146 @@ impl Scheduler { let mut current_stmt_id = thread.current_stmt_id; loop { - // Intercept repeat loops before evaluating statements - if let Stmt::RepeatLoop(loop_arg_expr_id, loop_body_id) = - thread.transaction[current_stmt_id] - { - let loop_stmt_id = current_stmt_id; - let loop_arg_symbol_id = match thread.transaction[loop_arg_expr_id] { - Expr::Sym(symbol_id) => symbol_id, - Expr::Const(_) => { - todo!("Maybe allow constants to appear as arguments to repeat loops??") - } - _ => { - unreachable!("Arguments to repeat loops are always SymbolIDs") - } - }; - - // Suppose we already know how many iterations a `repeat` loop - // must take. If so, we execute it deterministically. - // This situation occurs if there are multiple `repeat` loops - // in a protocol that use the same `LoopArg`, e.g. - // `repeat n iterations { ... }; ...; repeat n iterations { ... }` - if let Some(num_remaining_iters) = - thread.repeat_loops_remaining_iters.get_mut(&loop_stmt_id) - { - *num_remaining_iters -= 1; - if *num_remaining_iters == 0 { - thread.repeat_loops_remaining_iters.remove(&loop_stmt_id); - current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( - "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" + match thread.transaction[current_stmt_id] { + // Intercept `fork()` when it appears as the current statement + // (this happens when an `exited_thread` produced by + // the `handle_repeat_loops` helper function + // has `current_stmt_id`` pointing to `fork()`) + Stmt::Fork => { + thread.has_forked = true; + + // Check if another thread from the same start cycle has already forked + // in the current cycle for this scheduler. + // If so, skip the fork to avoid creating duplicate threads. + let already_forked = self.forked_start_cycles.contains(&thread.start_cycle); + let next_stmt_id = self.interpreter.next_stmt_map[¤t_stmt_id] + .expect("fork() is never the last statement in a protocol"); + + if already_forked { + info!( + "Thread {} called `fork()`, but another thread from the same start cycle (cycle {}) already forked in this cycle. Skipping fork to avoid duplicates.", + thread.global_thread_id(ctx), + thread.start_cycle ); + // Continue from the fork statement onwards + current_stmt_id = next_stmt_id; } else { - current_stmt_id = loop_body_id; + // Here, instead of creating a new thread for + // each possible protocol, we indicate to the + // caller that the current thread forked + + // Indicate that the thread's `start_cycle` + // called `fork` in the current cycle + self.forked_start_cycles.insert(thread.start_cycle); + + // Advance to next statement + thread.current_stmt_id = next_stmt_id; + + // Save the parent thread's state before we exit this function + thread.args_mapping = self.interpreter.args_mapping.clone(); + thread.known_bits = self.interpreter.known_bits.clone(); + thread.constraints = self.interpreter.constraints.clone(); + thread.args_to_pins = self.interpreter.args_to_pins.clone(); + + // Indicate to the caller that this thread forked + return Ok(ThreadResult::ExplicitFork { + parent: Box::new(thread), + }); } continue; } - - // Now we need to handle the case when the value of a `LoopArg` - // is unknown - match thread.loop_args_state.get(&loop_arg_symbol_id).cloned() { - None => { - // First time seeing loop arg, it is `Unknown` - // (i.e. absent from the thread's `loop_args_state` map), - // so pass in `n = 0` to the `handle_repeat_loops` - // helper function - return Ok(self.handle_repeat_loops( - loop_arg_symbol_id, - loop_body_id, - loop_stmt_id, - thread, - 0, - )); - } - Some(LoopArgState::Speculative(n, stored_loop_stmt_id)) => { - // We disallow nested `repeat` loops that use the - // same loop argument, i.e. we forbid - // `repeat n iterations { repeat n iterations { ... } ... }` - if loop_stmt_id != stored_loop_stmt_id { - panic!( - "Nested `repeat` loops that use the same loop argument `{}` are forbidden", - thread.symbol_table[loop_arg_symbol_id].name() - ) + Stmt::RepeatLoop(loop_arg_expr_id, loop_body_id) => { + let loop_stmt_id = current_stmt_id; + let loop_arg_symbol_id = match thread.transaction[loop_arg_expr_id] { + Expr::Sym(symbol_id) => symbol_id, + Expr::Const(_) => { + todo!("Maybe allow constants to appear as arguments to repeat loops??") } + _ => { + unreachable!("Arguments to repeat loops are always SymbolIDs") + } + }; - // Fork two threads: - // one with `Known(n)`, one with `Speculative(n + 1)` - return Ok(self.handle_repeat_loops( - loop_arg_symbol_id, - loop_body_id, - loop_stmt_id, - thread, - n, - )); - } - Some(LoopArgState::Known(n)) => { - // Value of `n` has been resolved from a prior loop - // (either with the same `StmtId` or a different `StmtId`) - if n == 0 { - // Exit the loop since the `LoopArg` is already known, - // proceed to the next immediate statement - // (evaluated in the next iteration - // of the outer `loop` in this function) + // Suppose we already know how many iterations a `repeat` loop + // must take. If so, we execute it deterministically. + // This situation occurs if there are multiple `repeat` loops + // in a protocol that use the same `LoopArg`, e.g. + // `repeat n iterations { ... }; ...; repeat n iterations { ... }` + if let Some(num_remaining_iters) = + thread.repeat_loops_remaining_iters.get_mut(&loop_stmt_id) + { + *num_remaining_iters -= 1; + if *num_remaining_iters == 0 { + thread.repeat_loops_remaining_iters.remove(&loop_stmt_id); current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( - "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" - ); + "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" + ); } else { - // Insert it into the thread's `repeat_loops_remaining_iters` - // map, which tracks how many iterations need to be executed - // for this loop - thread.repeat_loops_remaining_iters.insert(loop_stmt_id, n); current_stmt_id = loop_body_id; } continue; } + + // Now we need to handle the case when the value of a `LoopArg` + // is unknown + match thread.loop_args_state.get(&loop_arg_symbol_id).cloned() { + None => { + // First time seeing loop arg, it is `Unknown` + // (i.e. absent from the thread's `loop_args_state` map), + // so pass in `n = 0` to the `handle_repeat_loops` + // helper function + return Ok(self.handle_repeat_loops( + loop_arg_symbol_id, + loop_body_id, + loop_stmt_id, + thread, + 0, + )); + } + Some(LoopArgState::Speculative(n, stored_loop_stmt_id)) => { + // We disallow nested `repeat` loops that use the + // same loop argument, i.e. we forbid + // `repeat n iterations { repeat n iterations { ... } ... }` + if loop_stmt_id != stored_loop_stmt_id { + panic!( + "Nested `repeat` loops that use the same loop argument `{}` are forbidden", + thread.symbol_table[loop_arg_symbol_id].name() + ) + } + + // Fork two threads: + // one with `Known(n)`, one with `Speculative(n + 1)` + return Ok(self.handle_repeat_loops( + loop_arg_symbol_id, + loop_body_id, + loop_stmt_id, + thread, + n, + )); + } + Some(LoopArgState::Known(n)) => { + // Value of `n` has been resolved from a prior loop + // (either with the same `StmtId` or a different `StmtId`) + if n == 0 { + // Exit the loop since the `LoopArg` is already known, + // proceed to the next immediate statement + // (evaluated in the next iteration + // of the outer `loop` in this function) + current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" + ); + } else { + // Insert it into the thread's `repeat_loops_remaining_iters` + // map, which tracks how many iterations need to be executed + // for this loop + thread.repeat_loops_remaining_iters.insert(loop_stmt_id, n); + current_stmt_id = loop_body_id; + } + continue; + } + } } + _ => (), } match self.interpreter.evaluate_stmt(¤t_stmt_id, ctx, trace) { Ok(Some(next_stmt_id)) => { @@ -881,47 +928,7 @@ impl Scheduler { self.print_scheduler_state(trace, ctx); return Ok(ThreadResult::Completed); } - Stmt::Fork => { - thread.has_forked = true; - - // Check if another thread from the same start cycle has already forked - // in the current cycle for this scheduler. - // If so, skip the fork to avoid creating duplicate threads. - let already_forked = - self.forked_start_cycles.contains(&thread.start_cycle); - - if already_forked { - info!( - "Thread {} called `fork()`, but another thread from the same start cycle (cycle {}) already forked in this cycle. Skipping fork to avoid duplicates.", - thread.global_thread_id(ctx), - thread.start_cycle - ); - // Continue from the fork statement onwards - current_stmt_id = next_stmt_id; - } else { - // Here, instead of creating a new thread for - // each possible protocol, we indicate to the - // caller that the current thread forked - - // Indicate that the thread's `start_cycle` - // called `fork` in the current cycle - self.forked_start_cycles.insert(thread.start_cycle); - - // Advance to next statement - thread.current_stmt_id = next_stmt_id; - - // Save the parent thread's state before we exit this function - thread.args_mapping = self.interpreter.args_mapping.clone(); - thread.known_bits = self.interpreter.known_bits.clone(); - thread.constraints = self.interpreter.constraints.clone(); - thread.args_to_pins = self.interpreter.args_to_pins.clone(); - - // Indicate to the caller that this thread forked - return Ok(ThreadResult::ExplicitFork { - parent: Box::new(thread), - }); - } - } + Stmt::Fork => unreachable!("Handled above already"), _ => { // Default case: update `current_stmt_id` // to point to `next_stmt_id` From 943d665bb81496a36e66a91a7785045cf7f394a1 Mon Sep 17 00:00:00 2001 From: Ernest Ng Date: Sat, 21 Feb 2026 16:13:51 -0500 Subject: [PATCH 19/19] Revert "Intercept fork before handling other statements" This reverts commit 16670829112c883e6262c15fec34fa6b65e3ca88. --- monitor/src/scheduler.rs | 251 +++++++++++++++++++-------------------- 1 file changed, 122 insertions(+), 129 deletions(-) diff --git a/monitor/src/scheduler.rs b/monitor/src/scheduler.rs index 8dfab492..72822263 100644 --- a/monitor/src/scheduler.rs +++ b/monitor/src/scheduler.rs @@ -714,8 +714,8 @@ impl Scheduler { // The exited_thread needs to execute the first statement // that immediately follow the loop exited_thread.current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( - "Repeat loops can't be the last statement in a protocol since protocols always end with `step`" - ); + "Repeat loops can't be the last statement in a protocol since protocols always end with `step`" + ); // Update the current thread's `loop_args` map so that // the `LoopArg` is now `Speculative(n + 1)` @@ -761,146 +761,99 @@ impl Scheduler { let mut current_stmt_id = thread.current_stmt_id; loop { - match thread.transaction[current_stmt_id] { - // Intercept `fork()` when it appears as the current statement - // (this happens when an `exited_thread` produced by - // the `handle_repeat_loops` helper function - // has `current_stmt_id`` pointing to `fork()`) - Stmt::Fork => { - thread.has_forked = true; - - // Check if another thread from the same start cycle has already forked - // in the current cycle for this scheduler. - // If so, skip the fork to avoid creating duplicate threads. - let already_forked = self.forked_start_cycles.contains(&thread.start_cycle); - let next_stmt_id = self.interpreter.next_stmt_map[¤t_stmt_id] - .expect("fork() is never the last statement in a protocol"); - - if already_forked { - info!( - "Thread {} called `fork()`, but another thread from the same start cycle (cycle {}) already forked in this cycle. Skipping fork to avoid duplicates.", - thread.global_thread_id(ctx), - thread.start_cycle + // Intercept repeat loops before evaluating statements + if let Stmt::RepeatLoop(loop_arg_expr_id, loop_body_id) = + thread.transaction[current_stmt_id] + { + let loop_stmt_id = current_stmt_id; + let loop_arg_symbol_id = match thread.transaction[loop_arg_expr_id] { + Expr::Sym(symbol_id) => symbol_id, + Expr::Const(_) => { + todo!("Maybe allow constants to appear as arguments to repeat loops??") + } + _ => { + unreachable!("Arguments to repeat loops are always SymbolIDs") + } + }; + + // Suppose we already know how many iterations a `repeat` loop + // must take. If so, we execute it deterministically. + // This situation occurs if there are multiple `repeat` loops + // in a protocol that use the same `LoopArg`, e.g. + // `repeat n iterations { ... }; ...; repeat n iterations { ... }` + if let Some(num_remaining_iters) = + thread.repeat_loops_remaining_iters.get_mut(&loop_stmt_id) + { + *num_remaining_iters -= 1; + if *num_remaining_iters == 0 { + thread.repeat_loops_remaining_iters.remove(&loop_stmt_id); + current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" ); - // Continue from the fork statement onwards - current_stmt_id = next_stmt_id; } else { - // Here, instead of creating a new thread for - // each possible protocol, we indicate to the - // caller that the current thread forked - - // Indicate that the thread's `start_cycle` - // called `fork` in the current cycle - self.forked_start_cycles.insert(thread.start_cycle); - - // Advance to next statement - thread.current_stmt_id = next_stmt_id; - - // Save the parent thread's state before we exit this function - thread.args_mapping = self.interpreter.args_mapping.clone(); - thread.known_bits = self.interpreter.known_bits.clone(); - thread.constraints = self.interpreter.constraints.clone(); - thread.args_to_pins = self.interpreter.args_to_pins.clone(); - - // Indicate to the caller that this thread forked - return Ok(ThreadResult::ExplicitFork { - parent: Box::new(thread), - }); + current_stmt_id = loop_body_id; } continue; } - Stmt::RepeatLoop(loop_arg_expr_id, loop_body_id) => { - let loop_stmt_id = current_stmt_id; - let loop_arg_symbol_id = match thread.transaction[loop_arg_expr_id] { - Expr::Sym(symbol_id) => symbol_id, - Expr::Const(_) => { - todo!("Maybe allow constants to appear as arguments to repeat loops??") - } - _ => { - unreachable!("Arguments to repeat loops are always SymbolIDs") - } - }; - // Suppose we already know how many iterations a `repeat` loop - // must take. If so, we execute it deterministically. - // This situation occurs if there are multiple `repeat` loops - // in a protocol that use the same `LoopArg`, e.g. - // `repeat n iterations { ... }; ...; repeat n iterations { ... }` - if let Some(num_remaining_iters) = - thread.repeat_loops_remaining_iters.get_mut(&loop_stmt_id) - { - *num_remaining_iters -= 1; - if *num_remaining_iters == 0 { - thread.repeat_loops_remaining_iters.remove(&loop_stmt_id); - current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( - "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" - ); - } else { - current_stmt_id = loop_body_id; - } - continue; + // Now we need to handle the case when the value of a `LoopArg` + // is unknown + match thread.loop_args_state.get(&loop_arg_symbol_id).cloned() { + None => { + // First time seeing loop arg, it is `Unknown` + // (i.e. absent from the thread's `loop_args_state` map), + // so pass in `n = 0` to the `handle_repeat_loops` + // helper function + return Ok(self.handle_repeat_loops( + loop_arg_symbol_id, + loop_body_id, + loop_stmt_id, + thread, + 0, + )); } - - // Now we need to handle the case when the value of a `LoopArg` - // is unknown - match thread.loop_args_state.get(&loop_arg_symbol_id).cloned() { - None => { - // First time seeing loop arg, it is `Unknown` - // (i.e. absent from the thread's `loop_args_state` map), - // so pass in `n = 0` to the `handle_repeat_loops` - // helper function - return Ok(self.handle_repeat_loops( - loop_arg_symbol_id, - loop_body_id, - loop_stmt_id, - thread, - 0, - )); + Some(LoopArgState::Speculative(n, stored_loop_stmt_id)) => { + // We disallow nested `repeat` loops that use the + // same loop argument, i.e. we forbid + // `repeat n iterations { repeat n iterations { ... } ... }` + if loop_stmt_id != stored_loop_stmt_id { + panic!( + "Nested `repeat` loops that use the same loop argument `{}` are forbidden", + thread.symbol_table[loop_arg_symbol_id].name() + ) } - Some(LoopArgState::Speculative(n, stored_loop_stmt_id)) => { - // We disallow nested `repeat` loops that use the - // same loop argument, i.e. we forbid - // `repeat n iterations { repeat n iterations { ... } ... }` - if loop_stmt_id != stored_loop_stmt_id { - panic!( - "Nested `repeat` loops that use the same loop argument `{}` are forbidden", - thread.symbol_table[loop_arg_symbol_id].name() - ) - } - // Fork two threads: - // one with `Known(n)`, one with `Speculative(n + 1)` - return Ok(self.handle_repeat_loops( - loop_arg_symbol_id, - loop_body_id, - loop_stmt_id, - thread, - n, - )); - } - Some(LoopArgState::Known(n)) => { - // Value of `n` has been resolved from a prior loop - // (either with the same `StmtId` or a different `StmtId`) - if n == 0 { - // Exit the loop since the `LoopArg` is already known, - // proceed to the next immediate statement - // (evaluated in the next iteration - // of the outer `loop` in this function) - current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( + // Fork two threads: + // one with `Known(n)`, one with `Speculative(n + 1)` + return Ok(self.handle_repeat_loops( + loop_arg_symbol_id, + loop_body_id, + loop_stmt_id, + thread, + n, + )); + } + Some(LoopArgState::Known(n)) => { + // Value of `n` has been resolved from a prior loop + // (either with the same `StmtId` or a different `StmtId`) + if n == 0 { + // Exit the loop since the `LoopArg` is already known, + // proceed to the next immediate statement + // (evaluated in the next iteration + // of the outer `loop` in this function) + current_stmt_id = self.interpreter.next_stmt_map[&loop_stmt_id].expect( "Repeat loops can't be the last statement in a protocol since protocols always end with `step()`" ); - } else { - // Insert it into the thread's `repeat_loops_remaining_iters` - // map, which tracks how many iterations need to be executed - // for this loop - thread.repeat_loops_remaining_iters.insert(loop_stmt_id, n); - current_stmt_id = loop_body_id; - } - continue; + } else { + // Insert it into the thread's `repeat_loops_remaining_iters` + // map, which tracks how many iterations need to be executed + // for this loop + thread.repeat_loops_remaining_iters.insert(loop_stmt_id, n); + current_stmt_id = loop_body_id; } + continue; } } - _ => (), } match self.interpreter.evaluate_stmt(¤t_stmt_id, ctx, trace) { Ok(Some(next_stmt_id)) => { @@ -928,7 +881,47 @@ impl Scheduler { self.print_scheduler_state(trace, ctx); return Ok(ThreadResult::Completed); } - Stmt::Fork => unreachable!("Handled above already"), + Stmt::Fork => { + thread.has_forked = true; + + // Check if another thread from the same start cycle has already forked + // in the current cycle for this scheduler. + // If so, skip the fork to avoid creating duplicate threads. + let already_forked = + self.forked_start_cycles.contains(&thread.start_cycle); + + if already_forked { + info!( + "Thread {} called `fork()`, but another thread from the same start cycle (cycle {}) already forked in this cycle. Skipping fork to avoid duplicates.", + thread.global_thread_id(ctx), + thread.start_cycle + ); + // Continue from the fork statement onwards + current_stmt_id = next_stmt_id; + } else { + // Here, instead of creating a new thread for + // each possible protocol, we indicate to the + // caller that the current thread forked + + // Indicate that the thread's `start_cycle` + // called `fork` in the current cycle + self.forked_start_cycles.insert(thread.start_cycle); + + // Advance to next statement + thread.current_stmt_id = next_stmt_id; + + // Save the parent thread's state before we exit this function + thread.args_mapping = self.interpreter.args_mapping.clone(); + thread.known_bits = self.interpreter.known_bits.clone(); + thread.constraints = self.interpreter.constraints.clone(); + thread.args_to_pins = self.interpreter.args_to_pins.clone(); + + // Indicate to the caller that this thread forked + return Ok(ThreadResult::ExplicitFork { + parent: Box::new(thread), + }); + } + } _ => { // Default case: update `current_stmt_id` // to point to `next_stmt_id`