pct_strategy: run round robin for livelock avoding

Author: Kirillog

runtime/include/pct_strategy.h

@@ -34,8 +34,7 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
   size_t NextThreadId() override {
     auto& threads = this->threads;
     int max = std::numeric_limits<int>::min();
-    int snd_max = std::numeric_limits<int>::min();
-    size_t index_of_max = 0, index_of_snd_max = 0;
+    size_t index_of_max = 0;
     // Have to ignore waiting threads, so can't do it faster than O(n)
     for (size_t i = 0; i < threads.size(); ++i) {
       // Ignore waiting tasks
@@ -51,21 +50,31 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
       }
 
       if (max <= priorities[i]) {
-        index_of_snd_max = index_of_max;
-        snd_max = max;
         max = priorities[i];
         index_of_max = i;
-      } else if (snd_max <= priorities[i]) {
-        snd_max = priorities[i];
-        index_of_snd_max = i;
+      }
+    }
+
+    if (round_robin_stage > 0) {
+      for (size_t attempt = 0; attempt < threads.size(); ++attempt) {
+        auto i = (++last_chosen) % threads.size();
+        if (!threads[i].empty() && threads[i].back()->IsBlocked()) {
+          continue;
+        }
+        index_of_max = i;
+        max = priorities[i];
+        break;
+      }
+      // debug(stderr, "round robin choose: %d\n", index_of_max);
+      if (round_robin_start == index_of_max) {
+        --round_robin_stage;
       }
     }
 
     // TODO: Choose wiser constant
-    if (count_chosen_same == 100 && index_of_max == last_chosen &&
-        snd_max != std::numeric_limits<int>::min()) {
-      priorities[index_of_max] = snd_max - 1;
-      index_of_max = index_of_snd_max;
+    if (count_chosen_same == 1000 && index_of_max == last_chosen) {
+      round_robin_stage = 5;
+      round_robin_start = index_of_max;
     }
 
     if (index_of_max == last_chosen) {
@@ -97,8 +106,7 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
     auto& round_schedule = this->round_schedule;
     auto& threads = this->threads;
     int max = std::numeric_limits<int>::min();
-    int snd_max = std::numeric_limits<int>::min();
-    size_t index_of_max = 0, index_of_snd_max = 0;
+    size_t index_of_max = 0;
     // Have to ignore waiting threads, so can't do it faster than O(n)
     for (size_t i = 0; i < threads.size(); ++i) {
       int task_index = this->GetNextTaskInThread(i);
@@ -113,29 +121,40 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
       }
 
       if (max <= priorities[i]) {
-        index_of_snd_max = index_of_max;
-        snd_max = max;
         max = priorities[i];
         index_of_max = i;
-      } else if (snd_max <= priorities[i]) {
-        snd_max = priorities[i];
-        index_of_snd_max = i;
+      }
+    }
+
+    if (round_robin_stage > 0) {
+      for (size_t attempt = 0; attempt < threads.size(); ++attempt) {
+        auto i = (++last_chosen) % threads.size();
+        int task_index = this->GetNextTaskInThread(i);
+        if (task_index == threads[i].size() ||
+            threads[i][task_index]->IsBlocked()) {
+          continue;
+        }
+        index_of_max = i;
+        max = priorities[i];
+        break;
+      }
+      // debug(stderr, "round robin choose: %d\n", index_of_max);
+      if (round_robin_start == index_of_max) {
+        --round_robin_stage;
       }
     }
 
     // TODO: Choose wiser constant
-    if (count_chosen_same == 100 && index_of_max == last_chosen &&
-        snd_max != std::numeric_limits<int>::min()) {
-      priorities[index_of_max] = snd_max - 1;
-      index_of_max = index_of_snd_max;
+    if (count_chosen_same == 1000 && index_of_max == last_chosen) {
+      round_robin_stage = 5;
+      round_robin_start = index_of_max;
     }
 
     if (index_of_max == last_chosen) {
       ++count_chosen_same;
     } else {
       count_chosen_same = 1;
     }
-
     last_chosen = index_of_max;
     // Picked thread is `index_of_max`
     int next_task_index = this->GetNextTaskInThread(index_of_max);
@@ -179,6 +198,7 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
     k_statistics.push_back(current_schedule_length);
     current_schedule_length = 0;
     count_chosen_same = 0;
+    round_robin_stage = 0;
 
     // current_depth have been increased
     size_t new_k = std::reduce(k_statistics.begin(), k_statistics.end()) /
@@ -211,6 +231,8 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
   // original article)
   size_t count_chosen_same;
   size_t last_chosen;
+  size_t round_robin_start;
+  size_t round_robin_stage{0};
   std::vector<int> priorities;
   std::vector<size_t> priority_change_points;
   std::mt19937 rng;

runtime/include/scheduler.h

@@ -164,7 +164,7 @@ struct BaseStrategyWithThreads : public Strategy {
       size_t tasks_in_thread = thread.size();
       for (size_t i = 0; i < tasks_in_thread; ++i) {
         if (!IsTaskRemoved(thread[i]->GetId())) {
-          thread[i] = thread[i]->Restart(&*state);
+          thread[i] = thread[i]->Restart(state.get());
         }
       }
     }
@@ -220,7 +220,7 @@ struct BaseStrategyWithThreads : public Strategy {
       }
       threads[thread_index].emplace_back(
           this->constructors[verified_constructor].Build(
-              &*this->state, thread_index, this->new_task_id++));
+              this->state.get(), thread_index, this->new_task_id++));
       TaskWithMetaData task{threads[thread_index].back(), true, thread_index};
       return task;
     }
@@ -264,7 +264,7 @@ struct BaseStrategyWithThreads : public Strategy {
                                 return b.GetName() == *releaseTask;
                               });
             auto task =
-                constructor.Build(&*this->state, thread_index, task_index);
+                constructor.Build(this->state.get(), thread_index, task_index);
             auto verified = this->sched_checker.Verify(CreatedTaskMetaData{
                 std::string(task->GetName()), true, thread_index});
             assert(verified && "wrong release task at termination");
@@ -615,7 +615,7 @@ struct TLAScheduler : Scheduler {
       if (frame.is_new) {
         // It was a new task.
         // So restart it from the beginning with the same args.
-        *task = (*task)->Restart(&*state);
+        *task = (*task)->Restart(state.get());
       } else {
         // It was a not new task, hence, we recreated in early.
       }
@@ -732,7 +732,7 @@ struct TLAScheduler : Scheduler {
       for (size_t cons_num = 0; auto cons : constructors) {
         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 */));
 
         auto [is_over, res] = ResumeTask(frame, step, switches, thread, true);
         if (is_over || res.has_value()) {