[Interp] Deferred Conflicting Assignments Checking, Scheduler Code Cleanup, and More Tests

[Nikil-Shyamsunder]

This PR changes how the scheduler and interpreter handle conflicting assignments in multi-threaded protocol execution. Previously (like in the last PR lol) the system checked for conflicts eagerly at the moment each assignment was evaluated. I found an example where this doesn't work. I changed this to a deferred model where conflicts are only checked once at the end of each cycle, after all threads have finished executing. This change fixes incorrect behavior where valid protocol compositions were being rejected, and also improves error reporting by showing the locations of both conflicting assignments.

The Problem with Eager Conflict Checking

To understand why eager conflict checking was problematic, consider the wait_and_add_correct.tx test case. This test runs two transactions concurrently:

wait_and_add(1, 2, 3);
add(4, 5, 9);

The wait_and_add protocol waits for two cycles before setting the adder inputs, while the add protocol sets inputs immediately. Here's the relevant portion of wait_and_add:

fn wait_and_add<DUT: Adder>(in a: u32, in b: u32, out s: u32) {
  step();       // Cycle 0 -> 1
  fork();
  step();       // Cycle 1 -> 2: add(4, 5, 9) runs here after fork
  DUT.a := a;   // Sets a = 1
  DUT.b := b;   // Sets b = 2
  step();       // Cycle 2 -> 3
  assert_eq(s, DUT.s);
  step();
}

And here's the add protocol that gets forked:

fn add<DUT: Adder>(in a: u32, in b: u32, out s: u32) {
  DUT.a := a;   // Sets a = 4
  DUT.b := b;   // Sets b = 5
  step();       // Cycle 2 -> 3
  DUT.a := X;
  DUT.b := X;
  assert_eq(s, DUT.s);
  fork();
  step();
}

The critical issue arises due to how input values are implicitly reapplied at the start of each cycle. When a thread doesn't explicitly assign to an input pin, the system reapplies whatever value that thread last assigned to preserve continuity. In cycle 2, the add thread assigns a = 4 and b = 5. Meanwhile, wait_and_add hasn't assigned anything to a or b yet in its execution, so when we enter cycle 2, the system implicitly reapplies the previous values for wait_and_add's inputs.

With eager conflict checking, this implicit reapplication happened before wait_and_add had a chance to execute its DUT.a := a assignment. The implicit reapplication would store a "don't care" or old value for thread 0, and then when add (thread 1) assigned a = 4, the system would compare these values and potentially flag a conflict, even though wait_and_add was about to overwrite its implicit value with an explicit assignment.

The fix is to defer conflict checking until after all threads have executed their statements for the cycle. By the time I check for conflicts, wait_and_add has executed DUT.a := 1 and add has executed DUT.a := X, so things are good to go.

To implement this, I removed the conflict checking logic from apply_input_value, which is called during assignment evaluation. Instead, I added a new method check_for_conflicts() that iterates through all input pins and examines the per-thread values stored for each once all threads have completed for the cycle.

Finalizing Input Values

After checking for conflicts, I call finalize_inputs_for_cycle() to apply the correct final values to the DUT simulation. This step is necessary because of how DontCare (X) assignments interact with eager value application.

Consider the wait_and_add_correct.tx example again. In cycle 2, after the fork:

• Thread 0 (wait_and_add) executes: DUT.a := 1; DUT.b := 2;
• Thread 1 (add) executes: DUT.a := X; DUT.b := X;

During execution, assignments are applied eagerly to the simulation. But here's the problem: a DontCare assignment doesn't actually do anything to the simulation state (if other threads have assigned a concrete value for that input pin). It just records in the per-thread tracking that this thread no longer cares about this input's value. The simulation itself retains whatever value it had before.

This becomes problematic when you consider what might have happened earlier. At the start of cycle 2, thread 1 had concrete values (a = 4, b = 5) from its execution in cycle 1. These values were eagerly applied to the simulation during the implicit reapplication phase. Now when thread 1 executes DUT.a := X, its per-thread value changes to DontCare, but the simulation still holds a = 4 from that earlier eager application.

At the end of the cycle, the per-thread values are:

• Thread 0: a = 1, b = 2 (concrete values)
• Thread 1: a = X, b = X (DontCare)

No conflict here since only one thread has concrete values. The correct final value for a should be 1 (the only concrete value). But the simulation might still have a = 4 from thread 1's earlier assignment that it later "changed its mind" about.

You might think we could handle this during execution: when we see a DontCare assignment, check if any other thread has a concrete value and use that. But this doesn't work because we don't check for conflicts until the end of the cycle. At the point when thread 1 assigns X, thread 0 might not have executed yet, or thread 0 might have an intermediate value that it will later overwrite. We'd need foresight to know which concrete value will be the "real" final one, and making an arbitrary choice could apply a value that later turns out to conflict. So I think finalizing the input one last time to the sim at the end of all threads execution is the cleanest way to handle this, and is semantically correct (because in the view of any one transaction, the only time an input to the sim would "change" during this finalization stage is if it was DontCare anyways and doesnt matter to that transaction -- otherwise we'd have a conflicting assignment error).

Code Cleanup surrounding Threads

There was some logic regarding the termination of threads and the clearing of the inputs for that thread that was overly complex in the previous PR. I fixed this in a few ways, mainly I moved the thread cleanup logic (clearing thread inputs and handling implicit forks) to occur after finalize_inputs_for_cycle(). This ensures that input values are properly committed to the DUT before any cleanup occurs.

Improved Error Messages

For conflicting assignment errors, I modified the diagnostic system to show both threads' assignment locations. Previously, error deduplication would suppress the second error because both used the same StmtId as the deduplication key. I added a new StmtKeyWithThread(StmtId, usize) variant to the ErrorKey enum, allowing the system to distinguish between errors for different threads even when they reference the same statement. The new emit_diagnostic_stmt_for_thread() function uses this thread-aware key for deduplication.

Testing

The wait_and_add_correct.tx test now correctly passes (returns 0) instead of incorrectly failing with a conflicting assignment error. Similarly, other tests involving concurrent protocols with overlapping but non-conflicting assignments now behave correctly. Tests that genuinely have conflicts, like no_dontcare_conflict, now show error messages for both involved threads rather than just one. Also, added back the pcpi_mul_no_reset example which now gets a nice MaxItersError.

[ngernest]

This looks good to me, great job! Just to confirm I'm understanding correctly: this PR replaces #157, where:

• #157 checked for conflicts eagerly at assignment time
• this PR delays this check until the end of each cycle, when all threads finish executing

And just to check: the assignment semantics you formalized in https://github.com/cucapra/protocols-paper/pull/6/changes reflect the behavior implemented in this PR and not #157, right? I'm fairly certain the "final state equivalence" property you mentioned in the writeup refers to this PR, but I wanted to double check -- thanks!

[ngernest]

I also just added a commit with some extra doc-strings to help me better understand what's going on + a Display instance for the ThreadInputValue type for pretty-printing in logs

[Nikil-Shyamsunder]

This looks good to me, great job! Just to confirm I'm understanding correctly: this PR replaces #157, where:

• [Interp] Assignment Handling Overhaul and Implicit Input Reapplication #157 checked for conflicts eagerly at assignment time
• this PR delays this check until the end of each cycle, when all threads finish executing

And just to check: the assignment semantics you formalized in https://github.com/cucapra/protocols-paper/pull/6/changes reflect the behavior implemented in this PR and not #157, right? I'm fairly certain the "final state equivalence" property you mentioned in the writeup refers to this PR, but I wanted to double check -- thanks!

Technically, I think it applies to both. Most of the "proofs" in that write-up assume that there are no conflicting assignments. How we determine if a conflicting assignment occurs is not relevant under that assumption. Whether you find them statically, dynamically, right when they happen, or never, in this implementation doesn't affect the proof because the proof assumes a "correct/conflict-free" transaction sequence where a "correct" transaction sequence is one free of such conflicting assignment errors.

I think calling the thing i wrote a formalization of the assignment semantics probably is a misnomer on my part.

[Nikil-Shyamsunder]

@ngernest I'd hold off on merging until we can get @ekiwi to review as well for this one.

[ekiwi]

Can we add a comment explaining why we do this?

[ekiwi]

It would be nice to state here what this is testing.

[ekiwi]

This error message could probably be improved by identifying the name of the input and by inverting the causality. I.e., something like: output "s" depends on input "?" which does not have an assigned value.

[ekiwi]

I left some comments that would be worth going through. However, none of them are a blocker for merging this in. Great job, Nikil!