@@ -20,6 +20,37 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
2020 PrepareForDepth (current_depth, 1 );
2121 }
2222
23+ void AvoidLivelock (size_t & index, size_t & prior) {
24+ auto & threads = this ->threads ;
25+ if (fair_stage > 0 ) [[unlikely]] {
26+ for (size_t attempt = 0 ; attempt < threads.size (); ++attempt) {
27+ auto i = (++last_chosen) % threads.size ();
28+ if (!threads[i].empty () && threads[i].back ()->IsBlocked ()) {
29+ continue ;
30+ }
31+ index = i;
32+ prior = priorities[i];
33+ break ;
34+ }
35+ // debug(stderr, "round robin choose: %d\n", index_of_max);
36+ if (fair_start == index) {
37+ --fair_stage;
38+ }
39+ }
40+
41+ // TODO: Choose wiser constant
42+ if (count_chosen_same == 1000 && index == last_chosen) [[unlikely]] {
43+ fair_stage = 5 ;
44+ fair_start = index;
45+ }
46+
47+ if (index == last_chosen) {
48+ ++count_chosen_same;
49+ } else {
50+ count_chosen_same = 1 ;
51+ }
52+ }
53+
2354 std::optional<size_t > NextThreadId () override {
2455 auto & threads = this ->threads ;
2556 size_t max = std::numeric_limits<size_t >::min ();
@@ -45,33 +76,7 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
4576 }
4677 }
4778
48- if (round_robin_stage > 0 ) [[unlikely]] {
49- for (size_t attempt = 0 ; attempt < threads.size (); ++attempt) {
50- auto i = (++last_chosen) % threads.size ();
51- if (!threads[i].empty () && threads[i].back ()->IsBlocked ()) {
52- continue ;
53- }
54- index_of_max = i;
55- max = priorities[i];
56- break ;
57- }
58- // debug(stderr, "round robin choose: %d\n", index_of_max);
59- if (round_robin_start == index_of_max) {
60- --round_robin_stage;
61- }
62- }
63-
64- // TODO: Choose wiser constant
65- if (count_chosen_same == 1000 && index_of_max == last_chosen) [[unlikely]] {
66- round_robin_stage = 5 ;
67- round_robin_start = index_of_max;
68- }
69-
70- if (index_of_max == last_chosen) {
71- ++count_chosen_same;
72- } else {
73- count_chosen_same = 1 ;
74- }
79+ AvoidLivelock (index_of_max, max);
7580
7681 if (max == std::numeric_limits<size_t >::min ()) [[unlikely]] {
7782 return std::nullopt ;
@@ -117,7 +122,7 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
117122 }
118123 }
119124
120- if (round_robin_stage > 0 ) [[unlikely]] {
125+ if (fair_stage > 0 ) [[unlikely]] {
121126 for (size_t attempt = 0 ; attempt < threads.size (); ++attempt) {
122127 auto i = (++last_chosen) % threads.size ();
123128 int task_index = this ->GetNextTaskInThread (i);
@@ -130,15 +135,15 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
130135 break ;
131136 }
132137 // debug(stderr, "round robin choose: %d\n", index_of_max);
133- if (round_robin_start == index_of_max) {
134- --round_robin_stage ;
138+ if (fair_start == index_of_max) {
139+ --fair_stage ;
135140 }
136141 }
137142
138143 // TODO: Choose wiser constant
139144 if (count_chosen_same == 1000 && index_of_max == last_chosen) [[unlikely]] {
140- round_robin_stage = 5 ;
141- round_robin_start = index_of_max;
145+ fair_stage = 5 ;
146+ fair_start = index_of_max;
142147 }
143148
144149 if (index_of_max == last_chosen) {
@@ -194,7 +199,7 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
194199 k_statistics.push_back (current_schedule_length);
195200 current_schedule_length = 0 ;
196201 count_chosen_same = 0 ;
197- round_robin_stage = 0 ;
202+ fair_stage = 0 ;
198203
199204 // current_depth have been increased
200205 size_t new_k = std::reduce (k_statistics.begin (), k_statistics.end ()) /
@@ -227,8 +232,8 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
227232 // original article)
228233 size_t count_chosen_same;
229234 size_t last_chosen;
230- size_t round_robin_start ;
231- size_t round_robin_stage {0 };
235+ size_t fair_start ;
236+ size_t fair_stage {0 };
232237 std::vector<int > priorities;
233238 std::vector<size_t > priority_change_points;
234239 std::mt19937 rng;
0 commit comments