Skip to content

Commit 650ccfd

Browse files
Add support for specifying custom rounds (#23)
Separate macros for test with predefined custom rounds Number of threads could be different from --threads flag Minimization also works for custom rounds If predefined custom rounds do not detect error, regular round generation will start
1 parent ccab07a commit 650ccfd

21 files changed

Lines changed: 522 additions & 73 deletions

codegen/yieldpass.cpp

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,12 @@ struct YieldInserter {
119119
}
120120
}
121121

122-
#ifndef DEBUG
122+
// This change was added to instrument methods recusively for some VK data
123+
// structure, which had a lot of methods inside of it. This change allows to
124+
// insert thread interleavings in the methods without marking them with
125+
// `non_atomic` attribute. This flag is unset by default, because it might cause
126+
// wmm tests to instrument the LTest code, which is leads to errors.
127+
#if defined(LTEST_RECURSIVE_YIELDS)
123128
for (auto &B : F) {
124129
for (auto &I : B) {
125130
if (auto call = dyn_cast<CallInst>(&I)) {

runtime/CMakeLists.txt

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ set (SOURCE_FILES
33
lib.cpp
44
lin_check.cpp
55
logger.cpp
6-
pretty_printer.cpp
76
verifying.cpp
87
generators.cpp
98
minimization.cpp

runtime/include/custom_round.h

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#pragma once
2+
3+
#include <vector>
4+
5+
#include "lib.h"
6+
7+
struct CustomRound {
8+
CustomRound(std::vector<std::vector<TaskBuilder>> threads_)
9+
: threads(threads_) {}
10+
11+
std::vector<std::vector<TaskBuilder>> threads;
12+
};

runtime/include/pct_strategy.h

Lines changed: 21 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -156,6 +156,14 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
156156
return std::nullopt;
157157
}
158158

159+
// Check whether the priority change is required
160+
current_schedule_length++;
161+
for (size_t i = 0; i < priority_change_points.size(); ++i) {
162+
if (current_schedule_length == priority_change_points[i]) {
163+
priorities[index_of_max] = current_depth - i;
164+
}
165+
}
166+
159167
last_chosen = index_of_max;
160168
// Picked thread is `index_of_max`
161169
int next_task_index = this->GetNextTaskInThread(index_of_max);
@@ -166,19 +174,7 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
166174
}
167175

168176
void StartNextRound() override {
169-
this->new_task_id = 0;
170-
// log() << "depth: " << current_depth << "\n";
171-
// Reconstruct target as we start from the beginning.
172-
this->TerminateTasks();
173-
for (auto& thread : this->threads) {
174-
// We don't have to keep references alive
175-
while (thread.size() > 0) {
176-
thread.pop_back();
177-
}
178-
thread = StableVector<Task>();
179-
}
180-
// this->state.Reset();
181-
177+
BaseStrategyWithThreads<TargetObj, Verifier>::StartNextRound();
182178
UpdateStatistics();
183179
}
184180

@@ -187,6 +183,11 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
187183
UpdateStatistics();
188184
}
189185

186+
void SetCustomRound(CustomRound& custom_round) override {
187+
BaseStrategyWithThreads<TargetObj, Verifier>::SetCustomRound(custom_round);
188+
UpdateStatistics();
189+
}
190+
190191
~PctStrategy() { this->TerminateTasks(); }
191192

192193
private:
@@ -209,8 +210,14 @@ struct PctStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
209210
}
210211

211212
void PrepareForDepth(size_t depth, size_t k) {
213+
// Because we have custom rounds, take the
214+
// threads count from the vector size and not
215+
// from the threads_count field, which shows the passed threads count
216+
// argument from the command string
217+
size_t threads_count = this->threads.size();
218+
212219
// Generates priorities
213-
priorities = std::vector<int>(this->threads_count);
220+
priorities = std::vector<int>(threads_count);
214221
for (size_t i = 0; i < priorities.size(); ++i) {
215222
priorities[i] = current_depth + i;
216223
}

runtime/include/pick_strategy.h

Lines changed: 0 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -34,18 +34,6 @@ struct PickStrategy : public BaseStrategyWithThreads<TargetObj, Verifier> {
3434
is_new, current_thread};
3535
}
3636

37-
void StartNextRound() override {
38-
this->new_task_id = 0;
39-
40-
this->TerminateTasks();
41-
for (auto& thread : this->threads) {
42-
// We don't have to keep references alive
43-
while (thread.size() > 0) {
44-
thread.pop_back();
45-
}
46-
}
47-
}
48-
4937
~PickStrategy() { this->TerminateTasks(); }
5038

5139
protected:

runtime/include/pretty_print.h

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ using std::to_string;
1414
using FullHistoryWithThreads = std::vector<std::pair<
1515
int, std::variant<std::reference_wrapper<Task>, CoroutineStatus>>>;
1616
struct PrettyPrinter {
17-
PrettyPrinter(size_t threads_num);
17+
explicit PrettyPrinter() = default;
1818

1919
/*
2020
Prints like this:
@@ -31,7 +31,7 @@ struct PrettyPrinter {
3131
*/
3232
template <typename Out_t>
3333
void PrettyPrint(const std::vector<std::variant<Invoke, Response>>& result,
34-
Out_t& out) {
34+
int threads_num, Out_t& out) {
3535
auto get_thread_num = [](const std::variant<Invoke, Response>& v) {
3636
// Crutch.
3737
if (v.index() == 0) {
@@ -42,7 +42,7 @@ struct PrettyPrinter {
4242

4343
int cell_width = 50; // Up it if necessary. Enough for now.
4444

45-
auto print_separator = [&out, this, cell_width]() {
45+
auto print_separator = [threads_num, &out, this, cell_width]() {
4646
out << "*";
4747
for (int i = 0; i < threads_num; ++i) {
4848
for (int j = 0; j < cell_width; ++j) {
@@ -121,10 +121,11 @@ struct PrettyPrinter {
121121

122122
// Helps to debug full histories.
123123
template <typename Out_t>
124-
void PrettyPrint(FullHistoryWithThreads& result, Out_t& out) {
124+
void PrettyPrint(FullHistoryWithThreads& result, int threads_num,
125+
Out_t& out) {
125126
int cell_width = 20; // Up it if necessary. Enough for now.
126127

127-
auto print_separator = [&out, this, cell_width]() {
128+
auto print_separator = [threads_num, &out, this, cell_width]() {
128129
out << "*";
129130
for (int i = 0; i < threads_num; ++i) {
130131
for (int j = 0; j < cell_width; ++j) {
@@ -178,7 +179,7 @@ struct PrettyPrinter {
178179
index[base] = sz;
179180
}
180181
int length = std::to_string(index[base]).size();
181-
std::cout << index[base];
182+
out << index[base];
182183
assert(spaces - length >= 0);
183184
print_spaces(7 - length);
184185
out << "|";
@@ -247,5 +248,4 @@ struct PrettyPrinter {
247248
out << msg;
248249
}
249250
};
250-
size_t threads_num;
251251
};

runtime/include/random_strategy.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,14 @@ struct RandomStrategy : PickStrategy<TargetObj, Verifier> {
8080
return std::nullopt;
8181
}
8282

83+
void SetCustomRound(CustomRound &custom_round) override {
84+
PickStrategy<TargetObj, Verifier>::SetCustomRound(custom_round);
85+
86+
size_t custom_threads_count = custom_round.threads.size();
87+
weights.resize(custom_threads_count, 1);
88+
pick_weights.clear();
89+
}
90+
8391
private:
8492
std::vector<int> weights;
8593
std::vector<int> pick_weights;

0 commit comments

Comments
 (0)