From f4ab4bef62bad3adc7a950017daeb733388e91b6 Mon Sep 17 00:00:00 2001
From: Josh Varga <joshvarga@google.com>
Date: Tue, 8 Sep 2026 15:25:11 -0700
Subject: [PATCH] Use ordered_nodes instead of nodes in mutual exclusion pass.

This ensures deterministic iteration order when processing nodes in the mutual exclusion pass.

PiperOrigin-RevId: 978144817
---
 xls/scheduling/BUILD                         |  1 +
 xls/scheduling/mutual_exclusion_pass.cc      |  4 +-
 xls/scheduling/mutual_exclusion_pass_test.cc | 40 ++++++++++++++++++++
 3 files changed, 43 insertions(+), 2 deletions(-)

diff --git a/xls/scheduling/BUILD b/xls/scheduling/BUILD
index fe6aa8f39e..90c3daf11a 100644
--- a/xls/scheduling/BUILD
+++ b/xls/scheduling/BUILD
@@ -726,6 +726,7 @@ cc_test(
         "//xls/passes:dce_pass",
         "//xls/passes:optimization_pass",
         "//xls/passes:pass_base",
+        "//xls/solvers:solver",
         "@abseil-cpp//absl/status",
         "@abseil-cpp//absl/status:statusor",
         "@abseil-cpp//absl/strings",
diff --git a/xls/scheduling/mutual_exclusion_pass.cc b/xls/scheduling/mutual_exclusion_pass.cc
index e160931c1f..f0c7bdda83 100644
--- a/xls/scheduling/mutual_exclusion_pass.cc
+++ b/xls/scheduling/mutual_exclusion_pass.cc
@@ -416,12 +416,12 @@ absl::StatusOr<std::vector<absl::flat_hash_set<Node*>>> ComputeMergeClasses(
            scm.at(x) == scm.at(y);
   };
 
-  for (Node* x : nodes) {
+  for (Node* x : ordered_nodes) {
     if (!(p->GetPredicate(x).has_value())) {
       continue;
     }
     Node* px = p->GetPredicate(x).value();
-    for (Node* y : nodes) {
+    for (Node* y : ordered_nodes) {
       if (!(p->GetPredicate(y).has_value())) {
         continue;
       }
diff --git a/xls/scheduling/mutual_exclusion_pass_test.cc b/xls/scheduling/mutual_exclusion_pass_test.cc
index 50cb70cff0..60d69f616d 100644
--- a/xls/scheduling/mutual_exclusion_pass_test.cc
+++ b/xls/scheduling/mutual_exclusion_pass_test.cc
@@ -18,6 +18,7 @@
 #include <memory>
 #include <optional>
 #include <string_view>
+#include <variant>
 
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
@@ -43,6 +44,7 @@
 #include "xls/passes/pass_base.h"
 #include "xls/scheduling/scheduling_options.h"
 #include "xls/scheduling/scheduling_pass.h"
+#include "xls/solvers/solver.h"
 
 namespace xls {
 namespace {
@@ -625,6 +627,44 @@ TEST_P(MutualExclusionPassTest, MassiveNumberOfChannelsNoChange) {
   EXPECT_EQ(NumberOfOp(proc, Op::kSend), kNumChannels);
 }
 
+TEST_P(MutualExclusionPassTest, NonOrderRequestsCauseNonDeterministicResults) {
+  auto p = std::make_unique<Package>("p");
+  FunctionBuilder fb("f", p.get());
+  BValue c = fb.Param("c", p->GetBitsType(1));
+  BValue x = fb.Param("x", p->GetBitsType(16));
+  BValue y = fb.Param("y", p->GetBitsType(16));
+
+  BValue mul = fb.UMul(x, y);
+  BValue hard = fb.Eq(mul, fb.Literal(UBits(0x5555, 16)));
+  BValue c_is_1 = fb.Eq(c, fb.Literal(UBits(1, 1)));
+  BValue pa = fb.And(c_is_1, hard);
+  BValue pb = fb.Eq(c, fb.Literal(UBits(0, 1)));
+
+  XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.Build());
+  XLS_ASSERT_OK_AND_ASSIGN(auto solver,
+                           solvers::CreateSolver(solvers::SolverKind::kZ3));
+
+  // At rlimit = 484, proving mutual exclusion in order (pa, pb) succeeds within
+  // the deterministic resource limit (taking 483 steps), but in reverse order
+  // (pb, pa) it exhausts the resource limit (requiring 485 steps).
+  solvers::SolverLimit limit;
+  limit.deterministic_limit = 484;
+
+  auto i1 = solver->CreateSolverInstance(f, /*allow_unsupported=*/true).value();
+  i1->SetLimit(limit);
+  auto res1 =
+      i1->TryProve(pa.node(), solvers::Predicate::IsExclusiveWith(pb.node()));
+  ASSERT_THAT(res1, absl_testing::IsOk());
+  EXPECT_TRUE(std::holds_alternative<solvers::ProvenTrue>(*res1));
+
+  auto i2 = solver->CreateSolverInstance(f, /*allow_unsupported=*/true).value();
+  i2->SetLimit(limit);
+  auto res2 =
+      i2->TryProve(pb.node(), solvers::Predicate::IsExclusiveWith(pa.node()));
+  EXPECT_THAT(res2.status(),
+              absl_testing::StatusIs(absl::StatusCode::kDeadlineExceeded));
+}
+
 INSTANTIATE_TEST_SUITE_P(MutualExclusionPassTestSuite, MutualExclusionPassTest,
                          testing::Values(false, true));