From 8410bcc3808a93b3f1abec506bedf8fb1a75e0e7 Mon Sep 17 00:00:00 2001
From: Dmitrii Art <artuhovdmitrii@gmail.com>
Date: Thu, 15 Jan 2026 20:51:00 +0000
Subject: [PATCH 01/11] Add custom rounds implementation

---
 runtime/CMakeLists.txt            |  1 -
 runtime/include/custom_round.h    | 12 +++++
 runtime/include/pretty_print.h    | 12 ++---
 runtime/include/scheduler.h       | 79 ++++++++++++++++++++++++++-----
 runtime/include/scheduler_fwd.h   |  4 +-
 runtime/include/verifying.h       | 60 ++++++++++++++++-------
 runtime/include/verifying_macro.h | 53 +++++++++++++++++++++
 runtime/pretty_printer.cpp        |  3 --
 8 files changed, 184 insertions(+), 40 deletions(-)
 create mode 100644 runtime/include/custom_round.h
 delete mode 100644 runtime/pretty_printer.cpp

diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt
index 565ccc47..c152d769 100644
--- a/runtime/CMakeLists.txt
+++ b/runtime/CMakeLists.txt
@@ -3,7 +3,6 @@ set (SOURCE_FILES
         lib.cpp
         lin_check.cpp
         logger.cpp
-        pretty_printer.cpp
         verifying.cpp 
         generators.cpp
         minimization.cpp
diff --git a/runtime/include/custom_round.h b/runtime/include/custom_round.h
new file mode 100644
index 00000000..23bbaf58
--- /dev/null
+++ b/runtime/include/custom_round.h
@@ -0,0 +1,12 @@
+#pragma once
+
+#include <vector>
+
+#include "lib.h"
+
+struct CustomRound {
+  CustomRound(std::vector<std::vector<TaskBuilder>> threads_)
+      : threads(threads_) {}
+
+  std::vector<std::vector<TaskBuilder>> threads;
+};
\ No newline at end of file
diff --git a/runtime/include/pretty_print.h b/runtime/include/pretty_print.h
index 9504fa59..1e81c398 100644
--- a/runtime/include/pretty_print.h
+++ b/runtime/include/pretty_print.h
@@ -14,7 +14,7 @@ using std::to_string;
 using FullHistoryWithThreads = std::vector<std::pair<
     int, std::variant<std::reference_wrapper<Task>, CoroutineStatus>>>;
 struct PrettyPrinter {
-  PrettyPrinter(size_t threads_num);
+  explicit PrettyPrinter() = default;
 
   /*
       Prints like this:
@@ -31,7 +31,7 @@ struct PrettyPrinter {
   */
   template <typename Out_t>
   void PrettyPrint(const std::vector<std::variant<Invoke, Response>>& result,
-                   Out_t& out) {
+                   int threads_num, Out_t& out) {
     auto get_thread_num = [](const std::variant<Invoke, Response>& v) {
       // Crutch.
       if (v.index() == 0) {
@@ -42,7 +42,7 @@ struct PrettyPrinter {
 
     int cell_width = 50;  // Up it if necessary. Enough for now.
 
-    auto print_separator = [&out, this, cell_width]() {
+    auto print_separator = [threads_num, &out, this, cell_width]() {
       out << "*";
       for (int i = 0; i < threads_num; ++i) {
         for (int j = 0; j < cell_width; ++j) {
@@ -121,10 +121,11 @@ struct PrettyPrinter {
 
   // Helps to debug full histories.
   template <typename Out_t>
-  void PrettyPrint(FullHistoryWithThreads& result, Out_t& out) {
+  void PrettyPrint(FullHistoryWithThreads& result, int threads_num,
+                   Out_t& out) {
     int cell_width = 20;  // Up it if necessary. Enough for now.
 
-    auto print_separator = [&out, this, cell_width]() {
+    auto print_separator = [threads_num, &out, this, cell_width]() {
       out << "*";
       for (int i = 0; i < threads_num; ++i) {
         for (int j = 0; j < cell_width; ++j) {
@@ -247,5 +248,4 @@ struct PrettyPrinter {
       out << msg;
     }
   };
-  size_t threads_num;
 };
diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h
index 86420377..5ffe24e8 100644
--- a/runtime/include/scheduler.h
+++ b/runtime/include/scheduler.h
@@ -9,6 +9,7 @@
 #include <string_view>
 #include <utility>
 
+#include "custom_round.h"
 #include "lib.h"
 #include "lincheck.h"
 #include "logger.h"
@@ -78,6 +79,11 @@ struct Strategy {
   // Resets the state of all created tasks in the strategy.
   virtual void ResetCurrentRound() = 0;
 
+  // Sets custom round provided by the user for execution.
+  // The round should be executed via `Scheduler::ExploreRound` method
+  // instead of `Scheduler::GenerateAndRunRound`.
+  virtual void SetCustomRound(CustomRound& custom_round) = 0;
+
   // Returns the number of non-removed tasks
   virtual int GetValidTasksCount() const = 0;
 
@@ -165,6 +171,26 @@ struct BaseStrategyWithThreads : public Strategy {
     }
   }
 
+  void SetCustomRound(CustomRound& custom_round) override {
+    size_t custom_threads_count = custom_round.threads.size();
+
+    // custom round threads count might differ from the generated rounds
+    this->threads.resize(custom_threads_count);
+    this->round_schedule.resize(custom_threads_count, -1);
+
+    for (size_t current_thread = 0; current_thread < custom_threads_count;
+         ++current_thread) {
+      auto& builders = custom_round.threads[current_thread];
+      StableVector<Task> thread_tasks;
+      for (auto& task_builder : builders) {
+        auto task =
+            task_builder.Build(state.get(), current_thread, new_task_id++);
+        thread_tasks.emplace_back(task);
+      }
+      this->threads[current_thread] = std::move(thread_tasks);
+    }
+  }
+
   int GetValidTasksCount() const override {
     int non_removed_tasks = 0;
     for (auto& thread : threads) {
@@ -320,11 +346,13 @@ struct StrategyScheduler : public SchedulerWithReplay {
   // max_switches represents the maximal count of switches. After this count
   // scheduler will end execution of the Run function
   StrategyScheduler(Strategy& sched_class, ModelChecker& checker,
+                    std::vector<CustomRound> custom_rounds,
                     PrettyPrinter& pretty_printer, size_t max_tasks,
                     size_t max_rounds, bool minimize, size_t exploration_runs,
                     size_t minimization_runs)
       : strategy(sched_class),
         checker(checker),
+        custom_rounds(std::move(custom_rounds)),
         pretty_printer(pretty_printer),
         max_tasks(max_tasks),
         max_rounds(max_rounds),
@@ -336,28 +364,41 @@ struct StrategyScheduler : public SchedulerWithReplay {
   // history is a history with all events, where each element in the vector is a
   // Resume operation on the corresponding task
   Scheduler::Result Run() override {
-    for (size_t i = 0; i < max_rounds; ++i) {
-      log() << "run round: " << i << "\n";
-      auto histories = RunRound();
+    for (size_t j = 0; j < custom_rounds.size() + max_rounds; ++j) {
+      bool is_running_custom_scenarios = (j < custom_rounds.size());
+      Result histories;
+
+      if (is_running_custom_scenarios) {
+        log() << "explore custom round: " << j << "\n";
+        debug(stderr, "explore custom round: %zu\n", j);
+        strategy.SetCustomRound(custom_rounds[j]);
+        histories = ExploreRound(exploration_runs, true);
+      } else {
+        size_t i = j - custom_rounds.size();
+        log() << "run round: " << i << "\n";
+        debug(stderr, "run round: %zu\n", i);
+        histories = RunRound();
+      }
 
       if (histories.has_value()) {
         auto& [full_history, sequential_history, reason] = histories.value();
+        int threads_num = GetStartegyThreadsCount();
 
         if (should_minimize_history) {
           log() << "Full nonlinear scenario: \n";
-          pretty_printer.PrettyPrint(sequential_history, log());
+          pretty_printer.PrettyPrint(sequential_history, threads_num, log());
 
           log() << "Minimizing same interleaving...\n";
           Minimize(histories.value(), SameInterleavingMinimizor());
           log() << "Minimized to:\n";
-          pretty_printer.PrettyPrint(sequential_history, log());
+          pretty_printer.PrettyPrint(sequential_history, threads_num, log());
 
           log() << "Minimizing with rescheduling (exploration runs: "
                 << exploration_runs << ")...\n";
           Minimize(histories.value(),
                    StrategyExplorationMinimizor(exploration_runs));
           log() << "Minimized to:\n";
-          pretty_printer.PrettyPrint(sequential_history, log());
+          pretty_printer.PrettyPrint(sequential_history, threads_num, log());
 
           log() << "Minimizing with smart minimizor (exploration runs: "
                 << exploration_runs
@@ -377,6 +418,10 @@ struct StrategyScheduler : public SchedulerWithReplay {
     return std::nullopt;
   }
 
+  int GetStartegyThreadsCount() const override {
+    return strategy.GetThreadsCount();
+  }
+
  protected:
   // Runs a round with some interleaving while generating it
   Result RunRound() override {
@@ -412,7 +457,8 @@ struct StrategyScheduler : public SchedulerWithReplay {
       }
     }
 
-    pretty_printer.PrettyPrint(sequential_history, log());
+    pretty_printer.PrettyPrint(sequential_history, GetStartegyThreadsCount(),
+                               log());
 
     if (deadlock_detected) {
       return NonLinearizableHistory(full_history, sequential_history,
@@ -429,7 +475,7 @@ struct StrategyScheduler : public SchedulerWithReplay {
   }
 
   // Runs different interleavings of the current round
-  Result ExploreRound(int runs) override {
+  Result ExploreRound(int runs, bool log_each_interleaving) override {
     for (int i = 0; i < runs; ++i) {
       // log() << "Run " << i + 1 << "/" << runs << "\n";
       strategy.ResetCurrentRound();
@@ -463,6 +509,12 @@ struct StrategyScheduler : public SchedulerWithReplay {
         }
       }
 
+      if (log_each_interleaving) {
+        pretty_printer.PrettyPrint(sequential_history,
+                                   GetStartegyThreadsCount(), log());
+        log() << "\n";
+      }
+
       if (deadlock_detected) {
         return NonLinearizableHistory(full_history, sequential_history,
                                       NonLinearizableHistory::Reason::DEADLOCK);
@@ -470,7 +522,8 @@ struct StrategyScheduler : public SchedulerWithReplay {
 
       if (!checker.Check(sequential_history)) {
         // log() << "New nonlinearized scenario:\n";
-        // pretty_printer.PrettyPrint(sequential_history, log());
+        // pretty_printer.PrettyPrint(sequential_history,
+        //                            GetStartegyThreadsCount(), log());
         return NonLinearizableHistory(
             full_history, sequential_history,
             NonLinearizableHistory::Reason::NON_LINEARIZABLE_HISTORY);
@@ -554,6 +607,7 @@ struct StrategyScheduler : public SchedulerWithReplay {
  private:
   Strategy& strategy;
   ModelChecker& checker;
+  std::vector<CustomRound> custom_rounds;
   PrettyPrinter& pretty_printer;
   size_t max_tasks;
   size_t max_rounds;
@@ -724,7 +778,8 @@ struct TLAScheduler : Scheduler {
       }
     } else {
       log() << "run round: " << finished_rounds << "\n";
-      pretty_printer.PrettyPrint(full_history, log());
+      pretty_printer.PrettyPrint(full_history, GetStartegyThreadsCount(),
+                                 log());
       log() << "===============================================\n\n";
       log().flush();
       // Stop, check if the the generated history is linearizable.
@@ -813,7 +868,7 @@ struct TLAScheduler : Scheduler {
           }
           frame.is_new = true;
           auto size_before = tasks.size();
-          tasks.emplace_back(cons.Build(&state, i, -1/* TODO: fix task id for tla, because it is Scheduler and not Strategy class for some reason */));
+          tasks.emplace_back(cons.Build(state.get(), i, -1/* TODO: fix task id for tla, because it is Scheduler and not Strategy class for some reason */));
           started_tasks++;
           auto [is_over, res] = ResumeTask(frame, step, switches, thread, true);
           if (is_over || res.has_value()) {
@@ -834,6 +889,8 @@ struct TLAScheduler : Scheduler {
     return {false, {}};
   }
 
+  int GetStartegyThreadsCount() const override { return threads.size(); }
+
   PrettyPrinter& pretty_printer;
   size_t max_tasks;
   size_t max_rounds;
diff --git a/runtime/include/scheduler_fwd.h b/runtime/include/scheduler_fwd.h
index 5e0900f1..0b51f7f2 100644
--- a/runtime/include/scheduler_fwd.h
+++ b/runtime/include/scheduler_fwd.h
@@ -23,6 +23,8 @@ struct Scheduler {
 
   virtual Result Run() = 0;
 
+  virtual int GetStartegyThreadsCount() const = 0;
+
   virtual ~Scheduler() = default;
 };
 
@@ -35,7 +37,7 @@ struct SchedulerWithReplay : Scheduler {
 
   virtual Result RunRound() = 0;
 
-  virtual Result ExploreRound(int runs) = 0;
+  virtual Result ExploreRound(int runs, bool log_each_interleaving = false) = 0;
 
   virtual Result ReplayRound(const std::vector<int>& tasks_ordering) = 0;
 
diff --git a/runtime/include/verifying.h b/runtime/include/verifying.h
index 10a9c3d4..b7eb394f 100644
--- a/runtime/include/verifying.h
+++ b/runtime/include/verifying.h
@@ -6,6 +6,7 @@
 #include <type_traits>
 
 #include "blocking_primitives.h"
+#include "custom_round.h"
 #include "lib.h"
 #include "lincheck_recursive.h"
 #include "logger.h"
@@ -112,11 +113,14 @@ std::unique_ptr<Strategy> MakeStrategy(Opts &opts, std::vector<TaskBuilder> l) {
 template <StrategyTaskVerifier Verifier>
 struct StrategySchedulerWrapper : StrategyScheduler<Verifier> {
   StrategySchedulerWrapper(std::unique_ptr<Strategy> strategy,
-                           ModelChecker &checker, PrettyPrinter &pretty_printer,
-                           size_t max_tasks, size_t max_rounds, bool minimize,
+                           ModelChecker &checker,
+                           std::vector<CustomRound> custom_rounds,
+                           PrettyPrinter &pretty_printer, size_t max_tasks,
+                           size_t max_rounds, bool minimize,
                            size_t exploration_runs, size_t minimization_runs)
       : strategy(std::move(strategy)),
-        StrategyScheduler<Verifier>(*strategy.get(), checker, pretty_printer,
+        StrategyScheduler<Verifier>(*strategy.get(), checker,
+                                    std::move(custom_rounds), pretty_printer,
                                     max_tasks, max_rounds, minimize,
                                     exploration_runs, minimization_runs) {};
 
@@ -127,6 +131,7 @@ struct StrategySchedulerWrapper : StrategyScheduler<Verifier> {
 template <typename TargetObj, StrategyTaskVerifier Verifier>
 std::unique_ptr<Scheduler> MakeScheduler(ModelChecker &checker, Opts &opts,
                                          const std::vector<TaskBuilder> &l,
+                                         std::vector<CustomRound> custom_rounds,
                                          PrettyPrinter &pretty_printer,
                                          const std::function<void()> &cancel) {
   std::cout << "strategy = ";
@@ -136,8 +141,9 @@ std::unique_ptr<Scheduler> MakeScheduler(ModelChecker &checker, Opts &opts,
     case RND: {
       auto strategy = MakeStrategy<TargetObj, Verifier>(opts, std::move(l));
       auto scheduler = std::make_unique<StrategySchedulerWrapper<Verifier>>(
-          std::move(strategy), checker, pretty_printer, opts.tasks, opts.rounds,
-          opts.minimize, opts.exploration_runs, opts.minimization_runs);
+          std::move(strategy), checker, std::move(custom_rounds),
+          pretty_printer, opts.tasks, opts.rounds, opts.minimize,
+          opts.exploration_runs, opts.minimization_runs);
       return scheduler;
     }
     case TLA: {
@@ -159,12 +165,14 @@ inline int TrapRun(std::unique_ptr<Scheduler> &&scheduler,
   if (result.has_value()) {
     if (result->reason == Scheduler::NonLinearizableHistory::Reason::DEADLOCK) {
       std::cout << "deadlock detected:\n";
-      pretty_printer.PrettyPrint(result->seq, std::cout);
+      pretty_printer.PrettyPrint(
+          result->seq, scheduler->GetStartegyThreadsCount(), std::cout);
       return 4;  // see https://tldp.org/LDP/abs/html/exitcodes.html
     } else if (result->reason == Scheduler::NonLinearizableHistory::Reason::
                                      NON_LINEARIZABLE_HISTORY) {
       std::cout << "non linearized:\n";
-      pretty_printer.PrettyPrint(result->seq, std::cout);
+      pretty_printer.PrettyPrint(
+          result->seq, scheduler->GetStartegyThreadsCount(), std::cout);
       return 3;
     } else {
       std::abort();
@@ -177,7 +185,7 @@ inline int TrapRun(std::unique_ptr<Scheduler> &&scheduler,
 
 template <class Spec,
           StrategyTaskVerifier Verifier = DefaultStrategyTaskVerifier>
-int Run(int argc, char *argv[]) {
+int Run(int argc, char *argv[], std::vector<CustomRound> custom_rounds = {}) {
   if constexpr (!std::is_same_v<typename Spec::options_override_t,
                                 ltest::NoOverride>) {
     SetOpts(Spec::options_override_t::GetOptions());
@@ -198,7 +206,7 @@ int Run(int argc, char *argv[]) {
   }
   std::cout << "targets  = " << task_builders.size() << "\n";
 
-  PrettyPrinter pretty_printer{opts.threads};
+  PrettyPrinter pretty_printer;
 
   using lchecker_t =
       LinearizabilityCheckerRecursive<typename Spec::linear_spec_t,
@@ -208,8 +216,8 @@ int Run(int argc, char *argv[]) {
                      typename Spec::linear_spec_t{}};
 
   auto scheduler = MakeScheduler<typename Spec::target_obj_t, Verifier>(
-      checker, opts, std::move(task_builders), pretty_printer,
-      &Spec::cancel_t::Cancel);
+      checker, opts, std::move(task_builders), std::move(custom_rounds),
+      pretty_printer, &Spec::cancel_t::Cancel);
   std::cout << "\n\n";
   std::cout.flush();
   return TrapRun(std::move(scheduler), pretty_printer);
@@ -217,12 +225,28 @@ int Run(int argc, char *argv[]) {
 
 }  // namespace ltest
 
-#define LTEST_ENTRYPOINT_CONSTRAINT(spec_obj_t, strategy_verifier) \
-  int main(int argc, char *argv[]) {                               \
-    return ltest::Run<spec_obj_t, strategy_verifier>(argc, argv);  \
+// `...` is used instead of named argument in order to allow
+// user to specify custom rounds without wrapping them into
+// parenthesis `()` manually
+#define LTEST_ENTRYPOINT(spec_obj_t, ...)                                    \
+  int main(int argc, char *argv[]) {                                         \
+    std::vector<CustomRound> custom_rounds;                                  \
+    __VA_OPT__(std::vector<std::vector<std::vector<TaskBuilder>>> builders = \
+                   {__VA_ARGS__};                                            \
+               for (auto &v : builders) {                                    \
+                 custom_rounds.emplace_back(std::move(v));                   \
+               })                                                            \
+    return ltest::Run<spec_obj_t>(argc, argv, std::move(custom_rounds));     \
   }
 
-#define LTEST_ENTRYPOINT(spec_obj_t)           \
-  int main(int argc, char *argv[]) {           \
-    return ltest::Run<spec_obj_t>(argc, argv); \
-  }\
+#define LTEST_ENTRYPOINT_CONSTRAINT(spec_obj_t, strategy_verifier, ...)      \
+  int main(int argc, char *argv[]) {                                         \
+    std::vector<CustomRound> custom_rounds;                                  \
+    __VA_OPT__(std::vector<std::vector<std::vector<TaskBuilder>>> builders = \
+                   {__VA_ARGS__};                                            \
+               for (auto &v : builders) {                                    \
+                 custom_rounds.emplace_back(std::move(v));                   \
+               })                                                            \
+    return ltest::Run<spec_obj_t, strategy_verifier>(                        \
+        argc, argv, std::move(custom_rounds));                               \
+  }
\ No newline at end of file
diff --git a/runtime/include/verifying_macro.h b/runtime/include/verifying_macro.h
index 466f2d7b..a9f21f7b 100644
--- a/runtime/include/verifying_macro.h
+++ b/runtime/include/verifying_macro.h
@@ -78,6 +78,26 @@ struct TargetMethod {
   }
 };
 
+template <typename Ret, typename Target, typename... Args>
+struct MethodInvocation {
+  using Method = std::function<ValueWrapper(Target *, Args...)>;
+
+  inline static TaskBuilder GetTaskBuilder(std::string_view method_name,
+                                           std::tuple<Args...> params,
+                                           Method method) {
+    auto builder =
+        [method_name, params = std::move(params), method = std::move(method)](
+            void *this_ptr, size_t unused_thread_num, int task_id) -> Task {
+      auto args = std::shared_ptr<void>(new std::tuple(params));
+      auto coro = Coro<Target, Args...>::New(method, this_ptr, args,
+                                             &ltest::toStringArgs<Args...>,
+                                             method_name, task_id);
+      return coro;
+    };
+    return TaskBuilder(std::string(method_name), builder);
+  }
+};
+
 template <typename Target, typename... Args>
 struct TargetMethod<void, Target, Args...> {
   using Method = std::function<void(Target *, Args...)>;
@@ -102,6 +122,31 @@ struct TargetMethod<void, Target, Args...> {
   }
 };
 
+template <typename Target, typename... Args>
+struct MethodInvocation<void, Target, Args...> {
+  using Method = std::function<void(Target *, Args...)>;
+
+  inline static TaskBuilder GetTaskBuilder(std::string_view method_name,
+                                           std::tuple<Args...> params,
+                                           Method method) {
+    auto builder =
+        [method_name, params = std::move(params), method = std::move(method)](
+            void *this_ptr, size_t unused_thread_num, int task_id) -> Task {
+      // auto wrapper = Wrapper<Target, decltype(method), Args...>{method};
+      auto wrapper = [f = std::move(method)](void *this_ptr, Args &&...args) {
+        f(reinterpret_cast<Target *>(this_ptr), std::forward<Args>(args)...);
+        return void_v;
+      };
+      auto args = std::shared_ptr<void>(new std::tuple(params));
+      auto coro = Coro<Target, Args...>::New(wrapper, this_ptr, args,
+                                             &ltest::toStringArgs<Args...>,
+                                             method_name, task_id);
+      return coro;
+    };
+    return TaskBuilder(std::string(method_name), builder);
+  }
+};
+
 }  // namespace ltest
 
 #define declare_task_name(symbol) \
@@ -111,3 +156,11 @@ struct TargetMethod<void, Target, Args...> {
   declare_task_name(symbol);                               \
   ltest::TargetMethod<ret, cls __VA_OPT__(, ) __VA_ARGS__> \
       symbol##_ltest_method_cls{symbol##_task_name, gen, &cls::symbol};
+
+#define stringify_detail(x) #x
+#define stringify(x) stringify_detail(x)
+#define method_invocation(params, ret, cls, symbol, ...)                      \
+  ltest::MethodInvocation<                                                    \
+      ret, cls __VA_OPT__(, ) __VA_ARGS__>::GetTaskBuilder(stringify(symbol), \
+                                                           params,            \
+                                                           &cls::symbol)
\ No newline at end of file
diff --git a/runtime/pretty_printer.cpp b/runtime/pretty_printer.cpp
deleted file mode 100644
index 36cffdbe..00000000
--- a/runtime/pretty_printer.cpp
+++ /dev/null
@@ -1,3 +0,0 @@
-#include "include/pretty_print.h"
-
-PrettyPrinter::PrettyPrinter(size_t threads_num) : threads_num{threads_num} {}

From 54ddcf2da67dd9ad6f66e8ee4eda52bef5865fea Mon Sep 17 00:00:00 2001
From: Dmitrii Art <artuhovdmitrii@gmail.com>
Date: Thu, 15 Jan 2026 21:02:50 +0000
Subject: [PATCH 02/11] Add a test with custom round

---
 verifying/targets/CMakeLists.txt              |  7 +++
 .../nonlinear_queue_with_custom_rounds.cpp    | 45 +++++++++++++++++++
 2 files changed, 52 insertions(+)
 create mode 100644 verifying/targets/nonlinear_queue_with_custom_rounds.cpp

diff --git a/verifying/targets/CMakeLists.txt b/verifying/targets/CMakeLists.txt
index fa5e8a79..130ddfc4 100644
--- a/verifying/targets/CMakeLists.txt
+++ b/verifying/targets/CMakeLists.txt
@@ -6,6 +6,7 @@ set (SOURCE_TARGET_LIST
     nonlinear_set.cpp
     nonlinear_ms_queue.cpp
     nonlinear_treiber_stack.cpp
+    nonlinear_queue_with_custom_rounds.cpp
 )
 
 set (SOURCE_TARGET_WITHOUT_PLUGIN_LIST
@@ -75,6 +76,12 @@ add_integration_test("nonlinear_queue_pct" "verify" TRUE
     nonlinear_queue --rounds 10000 --strategy pct
 )
 
+# TODO: test should fail, but for some reason after commit '15f64f0 - feat: add more tests for blocking data structures&refactor blocking support'
+# it takes too much time to find bugs, I wasn't able to wait until custom round detects a bug 
+add_integration_test("nonlinear_queue_with_custom_rounds_pct" "verify" FALSE 
+    nonlinear_queue_with_custom_rounds --rounds 0 --exploration_runs 1000 --strategy pct
+)
+
 add_integration_test("unique_args" "verify" FALSE 
     unique_args
 )
diff --git a/verifying/targets/nonlinear_queue_with_custom_rounds.cpp b/verifying/targets/nonlinear_queue_with_custom_rounds.cpp
new file mode 100644
index 00000000..c3dc5862
--- /dev/null
+++ b/verifying/targets/nonlinear_queue_with_custom_rounds.cpp
@@ -0,0 +1,45 @@
+#include <atomic>
+#include <cstring>
+
+#include "../specs/queue.h"
+#include "runtime/include/verifying.h"
+#include "runtime/include/verifying_macro.h"
+
+const int N = 100;
+
+// Implementation copy-pasted from `nonlinear_queue.cpp`
+struct Queue {
+  Queue() {}
+
+  non_atomic void Push(int v) {
+    int pos = head.fetch_add(1);
+    a[pos] = v;
+  }
+
+  non_atomic int Pop() {
+    int last = head.load();
+    for (int i = 0; i < last; ++i) {
+      int e = a[i].load();
+      if (e != 0 && a[i].compare_exchange_strong(e, 0)) {
+        return e;
+      }
+    }
+    return 0;
+  }
+
+  std::atomic<int> a[N];
+  std::atomic<int> head{};
+};
+
+// Specify target structure and it's sequential specification.
+using spec_t =
+    ltest::Spec<Queue, spec::Queue<>, spec::QueueHash, spec::QueueEquals>;
+
+LTEST_ENTRYPOINT(spec_t,
+                 {{
+                      method_invocation(std::tuple(1), void, Queue, Push, int),
+                      method_invocation(std::tuple(2), void, Queue, Push, int),
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                  },
+                  {method_invocation(std::tuple(3), void, Queue, Push, int),
+                   method_invocation(std::tuple(), int, Queue, Pop)}});
\ No newline at end of file

From eed414443f6f2d682cc774c98a55e142bdeed739 Mon Sep 17 00:00:00 2001
From: Dmitrii Art <artuhovdmitrii@gmail.com>
Date: Fri, 16 Jan 2026 10:55:12 +0000
Subject: [PATCH 03/11] Increase CI timeout

---
 .github/workflows/run-tests.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/run-tests.yaml b/.github/workflows/run-tests.yaml
index c84e6f70..dfbc3630 100644
--- a/.github/workflows/run-tests.yaml
+++ b/.github/workflows/run-tests.yaml
@@ -31,7 +31,7 @@ jobs:
     container: 
       image: silkeh/clang:19
       options: --user root
-    timeout-minutes: 20
+    timeout-minutes: 30
     steps:
       - name: Install deps
         run: |

From b92fdefd773f1f0d9a6ef8320ed028a3bc8e3e9e Mon Sep 17 00:00:00 2001
From: Dmitrii Art <artuhovdmitrii@gmail.com>
Date: Fri, 16 Jan 2026 11:09:44 +0000
Subject: [PATCH 04/11] Fix bug in pretty printer which used std::cout instead
 of out from args

---
 runtime/include/pretty_print.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/runtime/include/pretty_print.h b/runtime/include/pretty_print.h
index 1e81c398..baf9fc8c 100644
--- a/runtime/include/pretty_print.h
+++ b/runtime/include/pretty_print.h
@@ -179,7 +179,7 @@ struct PrettyPrinter {
           index[base] = sz;
         }
         int length = std::to_string(index[base]).size();
-        std::cout << index[base];
+        out << index[base];
         assert(spaces - length >= 0);
         print_spaces(7 - length);
         out << "|";

From 9920f75a002854d492e5198ab6dac2ca1e599ff4 Mon Sep 17 00:00:00 2001
From: Dmitrii Artiukhov <artuhovdmitrii@gmail.com>
Date: Thu, 22 Jan 2026 23:48:11 +0000
Subject: [PATCH 05/11] Unify `StartNextRound` method between startegies and
 override `SetCustomRound` for random startegy additionally

---
 runtime/include/pct_strategy.h                | 14 +---------
 runtime/include/pick_strategy.h               | 12 --------
 runtime/include/random_strategy.h             |  8 ++++++
 runtime/include/scheduler.h                   | 28 +++++++++++++++++++
 runtime/include/strategy_verifier.h           |  2 ++
 .../verifiers/buffered_channel_verifier.h     | 12 ++++++--
 verifying/blocking/verifiers/mutex_verifier.h |  2 ++
 .../verifiers/shared_mutex_verifier.h         |  2 ++
 8 files changed, 52 insertions(+), 28 deletions(-)

diff --git a/runtime/include/pct_strategy.h b/runtime/include/pct_strategy.h
index 02569b88..06e6a7ff 100644
--- a/runtime/include/pct_strategy.h
+++ b/runtime/include/pct_strategy.h
@@ -166,19 +166,7 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
   }
 
   void StartNextRound() override {
-    this->new_task_id = 0;
-    //    log() << "depth: " << current_depth << "\n";
-    // Reconstruct target as we start from the beginning.
-    this->TerminateTasks();
-    for (auto& thread : this->threads) {
-      // We don't have to keep references alive
-      while (thread.size() > 0) {
-        thread.pop_back();
-      }
-      thread = StableVector<Task>();
-    }
-    // this->state.Reset();
-
+    BaseStrategyWithThreads<TargetObj, Verifier>::StartNextRound();
     UpdateStatistics();
   }
 
diff --git a/runtime/include/pick_strategy.h b/runtime/include/pick_strategy.h
index 8a21045a..d3a8aba5 100644
--- a/runtime/include/pick_strategy.h
+++ b/runtime/include/pick_strategy.h
@@ -34,18 +34,6 @@ struct PickStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
                             is_new, current_thread};
   }
 
-  void StartNextRound() override {
-    this->new_task_id = 0;
-
-    this->TerminateTasks();
-    for (auto& thread : this->threads) {
-      // We don't have to keep references alive
-      while (thread.size() > 0) {
-        thread.pop_back();
-      }
-    }
-  }
-
   ~PickStrategy() { this->TerminateTasks(); }
 
  protected:
diff --git a/runtime/include/random_strategy.h b/runtime/include/random_strategy.h
index 9f144f7f..f2f52d77 100644
--- a/runtime/include/random_strategy.h
+++ b/runtime/include/random_strategy.h
@@ -80,6 +80,14 @@ struct RandomStrategy : PickStrategy<TargetObj, Verifier> {
     return std::nullopt;
   }
 
+  void SetCustomRound(CustomRound &custom_round) override {
+    PickStrategy<TargetObj, Verifier>::SetCustomRound(custom_round);
+
+    size_t custom_threads_count = custom_round.threads.size();
+    weights.resize(custom_threads_count, 1);
+    pick_weights.clear();
+  }
+
  private:
   std::vector<int> weights;
   std::vector<int> pick_weights;
diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h
index 5ffe24e8..4033d047 100644
--- a/runtime/include/scheduler.h
+++ b/runtime/include/scheduler.h
@@ -36,6 +36,7 @@ concept StrategyTaskVerifier = requires(T a) {
   } -> std::same_as<bool>;
   { a.OnFinished(std::declval<Task&>(), size_t()) } -> std::same_as<void>;
   { a.ReleaseTask(size_t()) } -> std::same_as<std::optional<std::string>>;
+  { a.Reset() } -> std::same_as<void>;
 };
 
 // Strategy is the general strategy interface which decides which task
@@ -159,6 +160,31 @@ struct BaseStrategyWithThreads : public Strategy {
     return threads;
   }
 
+  void StartNextRound() override {
+    this->new_task_id = 0;
+    // also resets the state
+    this->TerminateTasks();
+
+    // this could happen if we run custom scenarios
+    // (which could have arbitrary number of threads)
+    if (this->threads.size() != this->threads_count) {
+      this->threads.clear();
+      for (size_t i = 0; i < this->threads_count; ++i) {
+        this->threads.emplace_back();
+      }
+    } else {
+      // more optimal allocations-wise implementation
+      for (auto& thread : this->threads) {
+        // We don't have to keep references alive
+        while (thread.size() > 0) {
+          thread.pop_back();
+        }
+      }
+    }
+
+    this->round_schedule.resize(this->threads_count, -1);
+  }
+
   void ResetCurrentRound() override {
     TerminateTasks();
     for (auto& thread : threads) {
@@ -177,6 +203,8 @@ struct BaseStrategyWithThreads : public Strategy {
     // custom round threads count might differ from the generated rounds
     this->threads.resize(custom_threads_count);
     this->round_schedule.resize(custom_threads_count, -1);
+    this->sched_checker.Reset();
+    this->state = std::make_unique<TargetObj>();
 
     for (size_t current_thread = 0; current_thread < custom_threads_count;
          ++current_thread) {
diff --git a/runtime/include/strategy_verifier.h b/runtime/include/strategy_verifier.h
index 75edf5ae..22f2ef2c 100644
--- a/runtime/include/strategy_verifier.h
+++ b/runtime/include/strategy_verifier.h
@@ -9,4 +9,6 @@ struct DefaultStrategyTaskVerifier {
   inline std::optional<std::string> ReleaseTask(size_t thread_id) {
     return std::nullopt;
   }
+
+  inline void Reset() {}
 };
diff --git a/verifying/blocking/verifiers/buffered_channel_verifier.h b/verifying/blocking/verifiers/buffered_channel_verifier.h
index 0bb894c5..ec6c5b50 100644
--- a/verifying/blocking/verifiers/buffered_channel_verifier.h
+++ b/verifying/blocking/verifiers/buffered_channel_verifier.h
@@ -46,8 +46,14 @@ struct BufferedChannelVerifier {
     return std::nullopt;
   }
 
-  size_t senders_;
-  size_t receivers_;
-  size_t size_;
+  void Reset() {
+    senders_ = 0;
+    receivers_ = 0;
+    size_ = 0;
+  }
+
+  size_t senders_ = 0;
+  size_t receivers_ = 0;
+  size_t size_ = 0;
 };
 }  // namespace spec
\ No newline at end of file
diff --git a/verifying/blocking/verifiers/mutex_verifier.h b/verifying/blocking/verifiers/mutex_verifier.h
index 30f12cc6..949caf06 100644
--- a/verifying/blocking/verifiers/mutex_verifier.h
+++ b/verifying/blocking/verifiers/mutex_verifier.h
@@ -36,6 +36,8 @@ struct MutexVerifier {
     return std::nullopt;
   }
 
+  void Reset() { status.clear(); }
+
   // NOTE(kmitkin): we cannot just store number of thread that holds mutex
   //                because Lock can finish before Unlock!
   std::unordered_map<size_t, size_t> status;
diff --git a/verifying/blocking/verifiers/shared_mutex_verifier.h b/verifying/blocking/verifiers/shared_mutex_verifier.h
index 628fdbf0..928d48af 100644
--- a/verifying/blocking/verifiers/shared_mutex_verifier.h
+++ b/verifying/blocking/verifiers/shared_mutex_verifier.h
@@ -54,6 +54,8 @@ struct SharedMutexVerifier {
     return std::nullopt;
   }
 
+  void Reset() { status.clear(); }
+
   std::unordered_map<size_t, size_t> status;
 };
 }  // namespace spec

From 9717f81a10429cdfb4ea36e4a83af80c3664e4bd Mon Sep 17 00:00:00 2001
From: Dmitrii Artiukhov <artuhovdmitrii@gmail.com>
Date: Sat, 21 Feb 2026 18:41:40 +0000
Subject: [PATCH 06/11] Update pct startegy to work the same way both for round
 generation and exploration (replay)

---
 runtime/include/pct_strategy.h | 21 ++++++++++++++++++++-
 runtime/include/scheduler.h    |  5 ++++-
 2 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/runtime/include/pct_strategy.h b/runtime/include/pct_strategy.h
index 06e6a7ff..251b4f4c 100644
--- a/runtime/include/pct_strategy.h
+++ b/runtime/include/pct_strategy.h
@@ -156,6 +156,14 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
       return std::nullopt;
     }
 
+    // Check whether the priority change is required
+    current_schedule_length++;
+    for (size_t i = 0; i < priority_change_points.size(); ++i) {
+      if (current_schedule_length == priority_change_points[i]) {
+        priorities[index_of_max] = current_depth - i;
+      }
+    }
+
     last_chosen = index_of_max;
     // Picked thread is `index_of_max`
     int next_task_index = this->GetNextTaskInThread(index_of_max);
@@ -175,6 +183,11 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
     UpdateStatistics();
   }
 
+  void SetCustomRound(CustomRound& custom_round) override {
+    BaseStrategyWithThreads<TargetObj, Verifier>::SetCustomRound(custom_round);
+    UpdateStatistics();
+  }
+
   ~PctStrategy() { this->TerminateTasks(); }
 
  private:
@@ -197,8 +210,14 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
   }
 
   void PrepareForDepth(size_t depth, size_t k) {
+    // Because we have custom rounds, take the
+    // threads count from the vector size and not
+    // from the threads_count field, which shows the passed threads count
+    // argument from the command string
+    size_t threads_count = this->threads.size();
+
     // Generates priorities
-    priorities = std::vector<int>(this->threads_count);
+    priorities = std::vector<int>(threads_count);
     for (size_t i = 0; i < priorities.size(); ++i) {
       priorities[i] = current_depth + i;
     }
diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h
index 4033d047..93e11733 100644
--- a/runtime/include/scheduler.h
+++ b/runtime/include/scheduler.h
@@ -359,7 +359,10 @@ struct BaseStrategyWithThreads : public Strategy {
   // references can't be invalidated before the end of the round,
   // so we have to contains all tasks in queues(queue doesn't invalidate the
   // references)
-  size_t threads_count;
+  size_t threads_count;  // number of threads specified in the command string
+                         // (in case if custom rounds are run, their threads
+                         // count might be different from this value which is
+                         // used for generated rounds only)
   std::vector<StableVector<Task>> threads;
   std::vector<TaskBuilder> constructors;
   std::uniform_int_distribution<std::mt19937::result_type>

From 0ae710d8708fecde989aebc7a49c054a45e15bd2 Mon Sep 17 00:00:00 2001
From: Dmitrii Artiukhov <artuhovdmitrii@gmail.com>
Date: Sun, 8 Feb 2026 10:40:39 +0000
Subject: [PATCH 07/11] Make recursive instrumentation under a specifi flag
 `LTEST_RECURSIVE_YIELDS`, which is unset by default

---
 codegen/yieldpass.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/codegen/yieldpass.cpp b/codegen/yieldpass.cpp
index 2b495f39..78c5cb31 100644
--- a/codegen/yieldpass.cpp
+++ b/codegen/yieldpass.cpp
@@ -119,7 +119,12 @@ struct YieldInserter {
       }
     }
 
-#ifndef DEBUG
+// This change was added to instrument methods recusively for some VK data
+// structure, which had a lot of methods inside of it. This change allows to
+// insert thread interleavings in the methods without marking them with
+// `non_atomic` attribute. This flag is unset by default, because it might cause
+// wmm tests to instrument the LTest code, which is leads to errors.
+#if defined(LTEST_RECURSIVE_YIELDS)
     for (auto &B : F) {
       for (auto &I : B) {
         if (auto call = dyn_cast<CallInst>(&I)) {

From 1fc7f8382b42b1d68711a59fc637a3ef6ef5b54c Mon Sep 17 00:00:00 2001
From: Dmitrii Artiukhov <artuhovdmitrii@gmail.com>
Date: Sat, 21 Feb 2026 19:19:34 +0000
Subject: [PATCH 08/11] Update param description, adding a note about custom
 rounds (that they run before any generated rounds)

---
 runtime/verifying.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/runtime/verifying.cpp b/runtime/verifying.cpp
index 85f52ed2..3769218e 100644
--- a/runtime/verifying.cpp
+++ b/runtime/verifying.cpp
@@ -67,7 +67,11 @@ StrategyType FromLiteral(std::string &&a) {
 DEFINE_int32(threads, 2, "Number of threads");
 DEFINE_int32(tasks, 15, "Number of tasks");
 DEFINE_int32(switches, 100000000, "Number of switches");
-DEFINE_int32(rounds, 5, "Number of rounds");
+DEFINE_int32(
+    rounds, 5,
+    "Number of rounds. When custom rounds are added, this value will show the "
+    "number of generated rounds to run after all custom ones. This can be "
+    "set to zero in case if you want to run only custom rounds");
 DEFINE_bool(minimize, false, "Minimize nonlinear scenario");
 DEFINE_int32(exploration_runs, 15,
              "Number of attempts to find nonlinearized round during each "

From f881c5a2e4a07cac6527b88776607518fdd810a7 Mon Sep 17 00:00:00 2001
From: Dmitrii Artiukhov <artuhovdmitrii@gmail.com>
Date: Sat, 21 Feb 2026 20:21:57 +0000
Subject: [PATCH 09/11] Add more tests for custom rounds

---
 verifying/targets/CMakeLists.txt              | 23 ++++--
 ... => nonlinear_queue_with_custom_round.cpp} |  0
 ...near_queue_with_multiple_custom_rounds.cpp | 76 +++++++++++++++++++
 3 files changed, 94 insertions(+), 5 deletions(-)
 rename verifying/targets/{nonlinear_queue_with_custom_rounds.cpp => nonlinear_queue_with_custom_round.cpp} (100%)
 create mode 100644 verifying/targets/nonlinear_queue_with_multiple_custom_rounds.cpp

diff --git a/verifying/targets/CMakeLists.txt b/verifying/targets/CMakeLists.txt
index 130ddfc4..e83d7dc6 100644
--- a/verifying/targets/CMakeLists.txt
+++ b/verifying/targets/CMakeLists.txt
@@ -6,7 +6,8 @@ set (SOURCE_TARGET_LIST
     nonlinear_set.cpp
     nonlinear_ms_queue.cpp
     nonlinear_treiber_stack.cpp
-    nonlinear_queue_with_custom_rounds.cpp
+    nonlinear_queue_with_custom_round.cpp
+    nonlinear_queue_with_multiple_custom_rounds.cpp
 )
 
 set (SOURCE_TARGET_WITHOUT_PLUGIN_LIST
@@ -76,10 +77,22 @@ add_integration_test("nonlinear_queue_pct" "verify" TRUE
     nonlinear_queue --rounds 10000 --strategy pct
 )
 
-# TODO: test should fail, but for some reason after commit '15f64f0 - feat: add more tests for blocking data structures&refactor blocking support'
-# it takes too much time to find bugs, I wasn't able to wait until custom round detects a bug 
-add_integration_test("nonlinear_queue_with_custom_rounds_pct" "verify" FALSE 
-    nonlinear_queue_with_custom_rounds --rounds 0 --exploration_runs 1000 --strategy pct
+add_integration_test("nonlinear_queue_with_custom_round_pct" "verify" TRUE 
+    nonlinear_queue_with_custom_round --rounds 0 --exploration_runs 1000 --strategy pct
+)
+
+add_integration_test("nonlinear_queue_with_custom_round_random" "verify" TRUE 
+    nonlinear_queue_with_custom_round --rounds 0 --exploration_runs 100000 --strategy random
+)
+
+# Runs custom rounds 5 times each, and then generates 1 round with random tasks.
+# Note: the number of tasks (--tasks 2) is small so that the nonlinearized scenario is not generated accidentally.
+add_integration_test("nonlinear_queue_with_multiple_custom_rounds_pct" "verify" FALSE 
+    nonlinear_queue_with_multiple_custom_rounds --rounds 1 --verbose --exploration_runs 5 --strategy pct --tasks 2
+)
+
+add_integration_test("nonlinear_queue_with_multiple_custom_rounds_random" "verify" FALSE 
+    nonlinear_queue_with_multiple_custom_rounds --rounds 1 --verbose --exploration_runs 5 --strategy random --tasks 2
 )
 
 add_integration_test("unique_args" "verify" FALSE 
diff --git a/verifying/targets/nonlinear_queue_with_custom_rounds.cpp b/verifying/targets/nonlinear_queue_with_custom_round.cpp
similarity index 100%
rename from verifying/targets/nonlinear_queue_with_custom_rounds.cpp
rename to verifying/targets/nonlinear_queue_with_custom_round.cpp
diff --git a/verifying/targets/nonlinear_queue_with_multiple_custom_rounds.cpp b/verifying/targets/nonlinear_queue_with_multiple_custom_rounds.cpp
new file mode 100644
index 00000000..213ccdcf
--- /dev/null
+++ b/verifying/targets/nonlinear_queue_with_multiple_custom_rounds.cpp
@@ -0,0 +1,76 @@
+#include <atomic>
+#include <cstring>
+
+#include "../specs/queue.h"
+#include "runtime/include/verifying.h"
+#include "runtime/include/verifying_macro.h"
+
+const int N = 100;
+
+// Implementation copy-pasted from `nonlinear_queue.cpp`
+struct Queue {
+  Queue() {}
+
+  non_atomic void Push(int v) {
+    int pos = head.fetch_add(1);
+    a[pos] = v;
+  }
+
+  non_atomic int Pop() {
+    int last = head.load();
+    for (int i = 0; i < last; ++i) {
+      int e = a[i].load();
+      if (e != 0 && a[i].compare_exchange_strong(e, 0)) {
+        return e;
+      }
+    }
+    return 0;
+  }
+
+  std::atomic<int> a[N];
+  std::atomic<int> head{};
+};
+
+// Specify target structure and it's sequential specification.
+using spec_t =
+    ltest::Spec<Queue, spec::Queue<>, spec::QueueHash, spec::QueueEquals>;
+
+LTEST_ENTRYPOINT(spec_t,
+                 // custom round 1
+                 {{
+                      method_invocation(std::tuple(1), void, Queue, Push, int),
+                      method_invocation(std::tuple(2), void, Queue, Push, int),
+                  },
+                  {
+                      method_invocation(std::tuple(3), void, Queue, Push, int),
+                      method_invocation(std::tuple(4), void, Queue, Push, int),
+                  }},
+                 // custom round 2
+                 {{
+                      method_invocation(std::tuple(1), void, Queue, Push, int),
+                  },
+                  {
+                      method_invocation(std::tuple(2), void, Queue, Push, int),
+                  },
+                  {
+                      method_invocation(std::tuple(3), void, Queue, Push, int),
+                  },
+                  {
+                      method_invocation(std::tuple(4), void, Queue, Push, int),
+                  }},
+                 // custom round 3
+                 {
+                     {method_invocation(std::tuple(1), void, Queue, Push, int),
+                      method_invocation(std::tuple(), int, Queue, Pop)},
+                 });
+
+// Then some generated rounds will be executed after all custom rounds.
+
+// Arguments generator.
+auto generateInt(size_t unused_param) {
+  return ltest::generators::makeSingleArg(rand() % 10 + 1);
+}
+
+// Targets.
+target_method(generateInt, void, Queue, Push, int);
+target_method(ltest::generators::genEmpty, int, Queue, Pop);
\ No newline at end of file

From 2bab17981b0d7b7dbeebc2d3e6b4344409f70761 Mon Sep 17 00:00:00 2001
From: Dmitrii Artiukhov <artuhovdmitrii@gmail.com>
Date: Sat, 21 Feb 2026 20:22:52 +0000
Subject: [PATCH 10/11] Decrease tests timeout back to 20 mins instead of 30

---
 .github/workflows/run-tests.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/run-tests.yaml b/.github/workflows/run-tests.yaml
index dfbc3630..c84e6f70 100644
--- a/.github/workflows/run-tests.yaml
+++ b/.github/workflows/run-tests.yaml
@@ -31,7 +31,7 @@ jobs:
     container: 
       image: silkeh/clang:19
       options: --user root
-    timeout-minutes: 30
+    timeout-minutes: 20
     steps:
       - name: Install deps
         run: |

From 2517ffa40042cfd9054bd6a1b4ee31c574b8c14f Mon Sep 17 00:00:00 2001
From: Dmitrii Artiukhov <artuhovdmitrii@gmail.com>
Date: Sat, 21 Feb 2026 20:46:03 +0000
Subject: [PATCH 11/11] Add test with custom scenario minimization

---
 verifying/targets/CMakeLists.txt              |   9 ++
 ...onlinear_queue_with_large_custom_round.cpp | 100 ++++++++++++++++++
 2 files changed, 109 insertions(+)
 create mode 100644 verifying/targets/nonlinear_queue_with_large_custom_round.cpp

diff --git a/verifying/targets/CMakeLists.txt b/verifying/targets/CMakeLists.txt
index e83d7dc6..090d21cd 100644
--- a/verifying/targets/CMakeLists.txt
+++ b/verifying/targets/CMakeLists.txt
@@ -8,6 +8,7 @@ set (SOURCE_TARGET_LIST
     nonlinear_treiber_stack.cpp
     nonlinear_queue_with_custom_round.cpp
     nonlinear_queue_with_multiple_custom_rounds.cpp
+    nonlinear_queue_with_large_custom_round.cpp
 )
 
 set (SOURCE_TARGET_WITHOUT_PLUGIN_LIST
@@ -85,6 +86,14 @@ add_integration_test("nonlinear_queue_with_custom_round_random" "verify" TRUE
     nonlinear_queue_with_custom_round --rounds 0 --exploration_runs 100000 --strategy random
 )
 
+add_integration_test("nonlinear_queue_with_large_custom_round_pct" "verify" TRUE 
+    nonlinear_queue_with_large_custom_round --rounds 0 --exploration_runs 1000 --strategy pct --minimize
+)
+
+add_integration_test("nonlinear_queue_with_large_custom_round_random" "verify" TRUE 
+    nonlinear_queue_with_large_custom_round --rounds 0 --exploration_runs 10000 --strategy random --minimize
+)
+
 # Runs custom rounds 5 times each, and then generates 1 round with random tasks.
 # Note: the number of tasks (--tasks 2) is small so that the nonlinearized scenario is not generated accidentally.
 add_integration_test("nonlinear_queue_with_multiple_custom_rounds_pct" "verify" FALSE 
diff --git a/verifying/targets/nonlinear_queue_with_large_custom_round.cpp b/verifying/targets/nonlinear_queue_with_large_custom_round.cpp
new file mode 100644
index 00000000..7a6d58ac
--- /dev/null
+++ b/verifying/targets/nonlinear_queue_with_large_custom_round.cpp
@@ -0,0 +1,100 @@
+/**
+ * Nonlinear queue with a single large custom round that is non-linearizable.
+ * The round has many groups and operations to stress concurrent Push/Pop
+ * interleaving and expose the bug (Pop scanning from 0 can return wrong order).
+ *
+ * Tests: run with --strategy pct (exploration_runs 1000) or --strategy random
+ * (exploration_runs 100000), both with --minimize.
+ */
+#include <atomic>
+#include <cstring>
+
+#include "../specs/queue.h"
+#include "runtime/include/verifying.h"
+#include "runtime/include/verifying_macro.h"
+
+const int N = 100;
+
+// Implementation copy-pasted from `nonlinear_queue.cpp`
+struct Queue {
+  Queue() {}
+
+  non_atomic void Push(int v) {
+    int pos = head.fetch_add(1);
+    a[pos] = v;
+  }
+
+  non_atomic int Pop() {
+    int last = head.load();
+    for (int i = 0; i < last; ++i) {
+      int e = a[i].load();
+      if (e != 0 && a[i].compare_exchange_strong(e, 0)) {
+        return e;
+      }
+    }
+    return 0;
+  }
+
+  std::atomic<int> a[N];
+  std::atomic<int> head{};
+};
+
+// Specify target structure and it's sequential specification.
+using spec_t =
+    ltest::Spec<Queue, spec::Queue<>, spec::QueueHash, spec::QueueEquals>;
+
+// Single large custom round: many groups with concurrent Push/Pop.
+// Non-linearizable because Pop scans from index 0 and concurrent operations can
+// produce wrong ordering.
+LTEST_ENTRYPOINT(spec_t,
+                 {{
+                      method_invocation(std::tuple(1), void, Queue, Push, int),
+                      method_invocation(std::tuple(2), void, Queue, Push, int),
+                      method_invocation(std::tuple(3), void, Queue, Push, int),
+                      method_invocation(std::tuple(4), void, Queue, Push, int),
+                  },
+                  {
+                      method_invocation(std::tuple(5), void, Queue, Push, int),
+                      method_invocation(std::tuple(6), void, Queue, Push, int),
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                  },
+                  {
+                      method_invocation(std::tuple(7), void, Queue, Push, int),
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                  },
+                  {
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                      method_invocation(std::tuple(8), void, Queue, Push, int),
+                      method_invocation(std::tuple(9), void, Queue, Push, int),
+                  },
+                  {
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                      method_invocation(std::tuple(10), void, Queue, Push, int),
+                  },
+                  {
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                  },
+                  {
+                      method_invocation(std::tuple(11), void, Queue, Push, int),
+                      method_invocation(std::tuple(12), void, Queue, Push, int),
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                  },
+                  {
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                      method_invocation(std::tuple(), int, Queue, Pop),
+                  }});
+
+// Arguments generator.
+auto generateInt(size_t unused_param) {
+  return ltest::generators::makeSingleArg(rand() % 10 + 1);
+}
+
+// Targets.
+target_method(generateInt, void, Queue, Push, int);
+target_method(ltest::generators::genEmpty, int, Queue, Pop);