Add support for specifying custom rounds

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)) {

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

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;
+};

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);
@@ -166,19 +174,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();
   }
 
@@ -187,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:
@@ -209,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;
     }

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:

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) {
@@ -178,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 << "|";
@@ -247,5 +248,4 @@ struct PrettyPrinter {
       out << msg;
     }
   };
-  size_t threads_num;
 };

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;