From ee0a991c92188145b70324503834b04bff96ae08 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Wed, 11 Dec 2024 00:43:41 +0000 Subject: [PATCH 01/47] Add task ids --- .gitignore | 1 + runtime/include/scheduler.h | 2 +- runtime/scheduler.cpp | 112 ++++++++++++++++++++++++++++++++++++ 3 files changed, 114 insertions(+), 1 deletion(-) create mode 100644 runtime/scheduler.cpp diff --git a/.gitignore b/.gitignore index 5094ec8e..56dd3bfa 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,6 @@ __pycache__ build +build-cmake venv .vscode .devcontainer/** diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index aa6008b2..7b13be8f 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -494,7 +494,7 @@ struct TLAScheduler : Scheduler { Scheduler::Result Run() override { auto [_, res] = RunStep(0, 0); - return res; + return res; } ~TLAScheduler() { TerminateTasks(); } diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp new file mode 100644 index 00000000..c8692705 --- /dev/null +++ b/runtime/scheduler.cpp @@ -0,0 +1,112 @@ +#include "include/scheduler.h" + +#include "include/logger.h" +#include "include/pretty_print.h" + +StrategyScheduler::StrategyScheduler(Strategy &sched_class, + ModelChecker &checker, + PrettyPrinter &pretty_printer, + size_t max_tasks, size_t max_rounds) + : strategy(sched_class), + checker(checker), + pretty_printer(pretty_printer), + max_tasks(max_tasks), + max_rounds(max_rounds) {} + +Scheduler::Result StrategyScheduler::runRound() { + // History of invoke and response events which is required for the checker + std::vector> sequential_history; + // Full history of the current execution in the Run function + std::vector> full_history; + + for (size_t finished_tasks = 0; finished_tasks < max_tasks;) { + auto [next_task, is_new, thread_id] = strategy.Next(); + + // fill the sequential history + if (is_new) { + sequential_history.emplace_back(Invoke(next_task, thread_id)); + } + full_history.emplace_back(next_task); + + next_task->Resume(); + if (next_task->IsReturned()) { + finished_tasks++; + + auto result = next_task->GetRetVal(); + sequential_history.emplace_back(Response(next_task, result, thread_id)); + } + } + + pretty_printer.PrettyPrint(sequential_history, log()); + + if (!checker.Check(sequential_history)) { + return std::make_pair(full_history, sequential_history); + } + + return std::nullopt; +} + +// TODO: refactor +// StrategyScheduler::Result StrategyScheduler::replayRound(FullHistory tasks_order) { +// // History of invoke and response events which is required for the checker +// SeqHistory sequential_history; + +// for (std::reference_wrapper next_task : tasks_order) { + +// } +// } + +Scheduler::Result StrategyScheduler::Run() { + for (size_t i = 0; i < max_rounds; ++i) { + log() << "run round: " << i << "\n"; + auto seq_history = runRound(); + if (seq_history.has_value()) { + + log() << "found failing sequential history:\n"; + auto& seq = seq_history.value().second; + for (auto history_point : seq) { + if (std::holds_alternative(history_point)) { + Invoke& inv = std::get(history_point); + log() << "i(" << inv.thread_id << ", '" << inv.GetTask()->GetName() << "'), "; + } + else { + Response& resp = std::get(history_point); + log() << "r(" << resp.thread_id << ", '" << resp.GetTask()->GetName() << "'): " << resp.result << ", "; + } + } + log() << "\n"; + + // TODO: add minimization here + return seq_history; + } + log() << "===============================================\n\n"; + log().flush(); + strategy.StartNextRound(); + } + + return std::nullopt; +} + +// Scheduler::Result StrategyScheduler::minimizeHistory(Result nonlinear_history) { +// if (!nonlinear_history.has_value()) return nonlinear_history; + +// auto& full_history = nonlinear_history.value().first; +// auto& sequential_history = nonlinear_history.value().second; + +// log() << "Minimizing history:\n"; +// pretty_printer.PrettyPrint(sequential_history, log()); + +// int task_idx_rm = 0; // task index in the sequential_history which we try to remove + +// while (task_idx_rm < sequential_history.size()) { +// while (std::holds_alternative(sequential_history[task_idx_rm])) { +// task_idx_rm++; +// } + +// const Task& removed_task = std::get(sequential_history[task_idx_rm]).GetTask(); +// log() << "Try remove task: (" << task_idx_rm << ") " << removed_task->GetName() << "\n"; + +// // create a new `std::vector threads_order`, in which `removed_task` will be excluded + +// } +// } From 71a07194defedd45f25576ef3879c067015e5ffc Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Wed, 11 Dec 2024 02:06:49 +0000 Subject: [PATCH 02/47] Add round replay --- runtime/include/pick_strategy.h | 21 ++++++++ runtime/scheduler.cpp | 88 +++++++++++++++++++++++++++------ 2 files changed, 94 insertions(+), 15 deletions(-) diff --git a/runtime/include/pick_strategy.h b/runtime/include/pick_strategy.h index 71530642..19cff7f0 100644 --- a/runtime/include/pick_strategy.h +++ b/runtime/include/pick_strategy.h @@ -76,6 +76,27 @@ struct PickStrategy : public BaseStrategyWithThreads { is_new, current_thread}; } + // TODO: same iplementation for pct + std::optional> GetTask(int task_id) override { + // TODO: can this be optimized? + int thread_id = 0; + for (auto& thread : this->threads) { + size_t tasks = thread.size(); + + for (size_t i = 0; i < tasks; ++i) { + Task& task = thread[i]; + if (task->GetId() == task_id) { + std::tuple result = { task, thread_id }; + return result; + // return std::make_tuple(task, thread_id); + } + } + + thread_id++; + } + return std::nullopt; + } + void StartNextRound() override { this->new_task_id = 0; diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp index c8692705..1e99c473 100644 --- a/runtime/scheduler.cpp +++ b/runtime/scheduler.cpp @@ -46,38 +46,96 @@ Scheduler::Result StrategyScheduler::runRound() { return std::nullopt; } -// TODO: refactor -// StrategyScheduler::Result StrategyScheduler::replayRound(FullHistory tasks_order) { -// // History of invoke and response events which is required for the checker -// SeqHistory sequential_history; +StrategyScheduler::Result StrategyScheduler::replayRound(const std::vector& tasks_ordering) { + strategy.ResetCurrentRound(); -// for (std::reference_wrapper next_task : tasks_order) { - -// } -// } + // History of invoke and response events which is required for the checker + FullHistory full_history; + SeqHistory sequential_history; + // TODO: `IsRunning` field might be added to `Task` instead + std::unordered_set started_tasks; + + for (int next_task_id : tasks_ordering) { + bool is_new = started_tasks.contains(next_task_id) ? false : started_tasks.insert(next_task_id).second; + auto task_info = strategy.GetTask(next_task_id); + + if (!task_info.has_value()) { + std::cerr << "No task with id " << next_task_id << " exists in round" << std::endl; + throw std::runtime_error("Invalid task id"); + } + + auto [next_task, thread_id] = task_info.value(); + if (is_new) { + sequential_history.emplace_back(Invoke(next_task, thread_id)); + } + full_history.emplace_back(next_task); + + log() << "Resume task: id=" << next_task_id << ", " << next_task->GetName() << ", thread-id=" << thread_id << "\n"; + + next_task->Resume(); + if (next_task->IsReturned()) { + auto result = next_task->GetRetVal(); + sequential_history.emplace_back(Response(next_task, result, thread_id)); + } + } + + log() << "Replayed round: tasks ordering = "; + for (size_t i = 0; i < tasks_ordering.size(); ++i) { + int task_id = tasks_ordering[i]; + log() << task_id; + if (i != tasks_ordering.size() - 1) log() << ","; + log() << " "; + } + log() << "\n"; + + pretty_printer.PrettyPrint(sequential_history, log()); + + if (!checker.Check(sequential_history)) { + return std::make_pair(full_history, sequential_history); + } + + return std::nullopt; +} + +std::vector StrategyScheduler::getTasksOrdering(const FullHistory& full_history) const { + std::vector tasks_ordering; + tasks_ordering.reserve(full_history.size()); + + for (auto& task : full_history) { + tasks_ordering.emplace_back(task.get()->GetId()); + } + + return tasks_ordering; +} Scheduler::Result StrategyScheduler::Run() { for (size_t i = 0; i < max_rounds; ++i) { log() << "run round: " << i << "\n"; - auto seq_history = runRound(); - if (seq_history.has_value()) { + auto histories = runRound(); + if (histories.has_value()) { log() << "found failing sequential history:\n"; - auto& seq = seq_history.value().second; - for (auto history_point : seq) { + auto& [full_history, sequential_history] = histories.value(); + + // Print the sequential history for debugging + for (auto history_point : sequential_history) { if (std::holds_alternative(history_point)) { Invoke& inv = std::get(history_point); log() << "i(" << inv.thread_id << ", '" << inv.GetTask()->GetName() << "'), "; } else { - Response& resp = std::get(history_point); - log() << "r(" << resp.thread_id << ", '" << resp.GetTask()->GetName() << "'): " << resp.result << ", "; + Response& response = std::get(history_point); + log() << "r(" << response.thread_id << ", '" << response.GetTask()->GetName() << "'): " << response.result << ", "; } } log() << "\n"; // TODO: add minimization here - return seq_history; + log() << "Replaying round for test\n"; + std::vector tasks_ordering = getTasksOrdering(full_history); + auto res = replayRound(tasks_ordering); + + return histories; } log() << "===============================================\n\n"; log().flush(); From 2dfa7b7a73e9cb206e7d1776e2bb9f881f616491 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Wed, 11 Dec 2024 03:18:23 +0000 Subject: [PATCH 03/47] Implement dumb minimization --- runtime/include/lib.h | 2 + runtime/scheduler.cpp | 103 ++++++++++++++++++++++++++++++++++++------ 2 files changed, 90 insertions(+), 15 deletions(-) diff --git a/runtime/include/lib.h b/runtime/include/lib.h index 26142d75..492eac82 100644 --- a/runtime/include/lib.h +++ b/runtime/include/lib.h @@ -96,6 +96,8 @@ struct CoroBase : public std::enable_shared_from_this { } return is_blocked; } + // Sets IsRemoved state. + void SetRemoved(bool is_removed); // Checks if the coroutine is parked. bool IsParked() const; diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp index 1e99c473..3b0e095a 100644 --- a/runtime/scheduler.cpp +++ b/runtime/scheduler.cpp @@ -1,5 +1,6 @@ -#include "include/scheduler.h" +#include +#include "include/scheduler.h" #include "include/logger.h" #include "include/pretty_print.h" @@ -70,7 +71,9 @@ StrategyScheduler::Result StrategyScheduler::replayRound(const std::vector& } full_history.emplace_back(next_task); - log() << "Resume task: id=" << next_task_id << ", " << next_task->GetName() << ", thread-id=" << thread_id << "\n"; + // log() << "Resume task: id=" << next_task_id << ", " << next_task->GetName() << ", thread-id=" << thread_id << "\n"; + + if (next_task->IsReturned()) continue; next_task->Resume(); if (next_task->IsReturned()) { @@ -79,14 +82,14 @@ StrategyScheduler::Result StrategyScheduler::replayRound(const std::vector& } } - log() << "Replayed round: tasks ordering = "; - for (size_t i = 0; i < tasks_ordering.size(); ++i) { - int task_id = tasks_ordering[i]; - log() << task_id; - if (i != tasks_ordering.size() - 1) log() << ","; - log() << " "; - } - log() << "\n"; + // log() << "Replayed round: tasks ordering = "; + // for (size_t i = 0; i < tasks_ordering.size(); ++i) { + // int task_id = tasks_ordering[i]; + // log() << task_id; + // if (i != tasks_ordering.size() - 1) log() << ","; + // log() << " "; + // } + // log() << "\n"; pretty_printer.PrettyPrint(sequential_history, log()); @@ -97,17 +100,80 @@ StrategyScheduler::Result StrategyScheduler::replayRound(const std::vector& return std::nullopt; } -std::vector StrategyScheduler::getTasksOrdering(const FullHistory& full_history) const { +std::vector StrategyScheduler::getTasksOrdering(const FullHistory& full_history, const std::unordered_set exclude_task_ids) const { std::vector tasks_ordering; - tasks_ordering.reserve(full_history.size()); for (auto& task : full_history) { + if (exclude_task_ids.contains(task.get()->GetId())) continue; tasks_ordering.emplace_back(task.get()->GetId()); } return tasks_ordering; } +void StrategyScheduler::minimize( + std::pair& nonlinear_history +) { + std::unordered_set removed_tasks; + std::vector> tasks; + + for (const HistoryEvent& event : nonlinear_history.second) { + if (std::holds_alternative(event)) { + tasks.push_back(std::get(event).GetTask()); + } + } + + // remove single task + for (auto& task : tasks) { + int task_id = task.get()->GetId(); + + log() << "Try to remove task with id: " << task_id << "\n"; + std::vector new_ordering = getTasksOrdering(nonlinear_history.first, { task_id }); + auto new_histories = replayRound(new_ordering); + + if (new_histories.has_value()) { + nonlinear_history.first.swap(new_histories.value().first); + nonlinear_history.second.swap(new_histories.value().second); + removed_tasks.insert(task_id); + task.get()->SetRemoved(true); + } + } + + // remove two tasks (for operations with semantics of add/remove) + for (auto& task_i : tasks) { + if (task_i.get()->IsRemoved()) continue; + + for (auto& task_j : tasks) { + if (task_j.get()->IsRemoved()) continue; + + int task_i_id = task_i.get()->GetId(); + int task_j_id = task_j.get()->GetId(); + + if (task_i_id == task_j_id) continue; + + log() << "Try to remove task with id: " << task_i_id << " and " << task_j_id << "\n"; + std::vector new_ordering = getTasksOrdering(nonlinear_history.first, { task_i_id, task_j_id }); + auto new_histories = replayRound(new_ordering); + + if (new_histories.has_value()) { + nonlinear_history.first.swap(new_histories.value().first); + nonlinear_history.second.swap(new_histories.value().second); + + removed_tasks.insert(task_i_id); + removed_tasks.insert(task_j_id); + + task_i.get()->SetRemoved(true); + task_j.get()->SetRemoved(true); + } + } + } + + // replay round one last time to get returned coroutine states + replayRound(getTasksOrdering(nonlinear_history.first, {})); + + log() << "Finished minimization\n"; +} + Scheduler::Result StrategyScheduler::Run() { for (size_t i = 0; i < max_rounds; ++i) { log() << "run round: " << i << "\n"; @@ -131,11 +197,18 @@ Scheduler::Result StrategyScheduler::Run() { log() << "\n"; // TODO: add minimization here - log() << "Replaying round for test\n"; - std::vector tasks_ordering = getTasksOrdering(full_history); - auto res = replayRound(tasks_ordering); + log() << "Full nonlinear scenario: \n"; + pretty_printer.PrettyPrint(sequential_history, log()); + + log() << "Minimizing...\n"; + minimize(histories.value()); return histories; + + // log() << "Replaying round for test\n"; + // std::vector tasks_ordering = getTasksOrdering(full_history); + // auto res = replayRound(tasks_ordering); + // return histories; } log() << "===============================================\n\n"; log().flush(); From 899487e23aa2fb518b5be829c65d946be4c23271 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Wed, 11 Dec 2024 03:29:42 +0000 Subject: [PATCH 04/47] Cleanup code --- runtime/scheduler.cpp | 65 ++++--------------------------------------- 1 file changed, 5 insertions(+), 60 deletions(-) diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp index 3b0e095a..6098b9e1 100644 --- a/runtime/scheduler.cpp +++ b/runtime/scheduler.cpp @@ -82,16 +82,7 @@ StrategyScheduler::Result StrategyScheduler::replayRound(const std::vector& } } - // log() << "Replayed round: tasks ordering = "; - // for (size_t i = 0; i < tasks_ordering.size(); ++i) { - // int task_id = tasks_ordering[i]; - // log() << task_id; - // if (i != tasks_ordering.size() - 1) log() << ","; - // log() << " "; - // } - // log() << "\n"; - - pretty_printer.PrettyPrint(sequential_history, log()); + //pretty_printer.PrettyPrint(sequential_history, log()); if (!checker.Check(sequential_history)) { return std::make_pair(full_history, sequential_history); @@ -127,7 +118,7 @@ void StrategyScheduler::minimize( for (auto& task : tasks) { int task_id = task.get()->GetId(); - log() << "Try to remove task with id: " << task_id << "\n"; + // log() << "Try to remove task with id: " << task_id << "\n"; std::vector new_ordering = getTasksOrdering(nonlinear_history.first, { task_id }); auto new_histories = replayRound(new_ordering); @@ -151,7 +142,7 @@ void StrategyScheduler::minimize( if (task_i_id == task_j_id) continue; - log() << "Try to remove task with id: " << task_i_id << " and " << task_j_id << "\n"; + // log() << "Try to remove task with id: " << task_i_id << " and " << task_j_id << "\n"; std::vector new_ordering = getTasksOrdering(nonlinear_history.first, { task_i_id, task_j_id }); auto new_histories = replayRound(new_ordering); @@ -168,10 +159,8 @@ void StrategyScheduler::minimize( } } - // replay round one last time to get returned coroutine states + // replay round one last time to put coroutines in `returned` state replayRound(getTasksOrdering(nonlinear_history.first, {})); - - log() << "Finished minimization\n"; } Scheduler::Result StrategyScheduler::Run() { @@ -180,23 +169,8 @@ Scheduler::Result StrategyScheduler::Run() { auto histories = runRound(); if (histories.has_value()) { - log() << "found failing sequential history:\n"; auto& [full_history, sequential_history] = histories.value(); - // Print the sequential history for debugging - for (auto history_point : sequential_history) { - if (std::holds_alternative(history_point)) { - Invoke& inv = std::get(history_point); - log() << "i(" << inv.thread_id << ", '" << inv.GetTask()->GetName() << "'), "; - } - else { - Response& response = std::get(history_point); - log() << "r(" << response.thread_id << ", '" << response.GetTask()->GetName() << "'): " << response.result << ", "; - } - } - log() << "\n"; - - // TODO: add minimization here log() << "Full nonlinear scenario: \n"; pretty_printer.PrettyPrint(sequential_history, log()); @@ -204,11 +178,6 @@ Scheduler::Result StrategyScheduler::Run() { minimize(histories.value()); return histories; - - // log() << "Replaying round for test\n"; - // std::vector tasks_ordering = getTasksOrdering(full_history); - // auto res = replayRound(tasks_ordering); - // return histories; } log() << "===============================================\n\n"; log().flush(); @@ -216,28 +185,4 @@ Scheduler::Result StrategyScheduler::Run() { } return std::nullopt; -} - -// Scheduler::Result StrategyScheduler::minimizeHistory(Result nonlinear_history) { -// if (!nonlinear_history.has_value()) return nonlinear_history; - -// auto& full_history = nonlinear_history.value().first; -// auto& sequential_history = nonlinear_history.value().second; - -// log() << "Minimizing history:\n"; -// pretty_printer.PrettyPrint(sequential_history, log()); - -// int task_idx_rm = 0; // task index in the sequential_history which we try to remove - -// while (task_idx_rm < sequential_history.size()) { -// while (std::holds_alternative(sequential_history[task_idx_rm])) { -// task_idx_rm++; -// } - -// const Task& removed_task = std::get(sequential_history[task_idx_rm]).GetTask(); -// log() << "Try remove task: (" << task_idx_rm << ") " << removed_task->GetName() << "\n"; - -// // create a new `std::vector threads_order`, in which `removed_task` will be excluded - -// } -// } +} \ No newline at end of file From d7e7e86964f0b9fee0aa7fd702558320fed60177 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Tue, 17 Dec 2024 18:19:46 +0000 Subject: [PATCH 05/47] Add fix to dumb minimization --- runtime/scheduler.cpp | 28 +++++++++++++++++++++++++--- 1 file changed, 25 insertions(+), 3 deletions(-) diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp index 6098b9e1..0b3e5ad7 100644 --- a/runtime/scheduler.cpp +++ b/runtime/scheduler.cpp @@ -55,6 +55,15 @@ StrategyScheduler::Result StrategyScheduler::replayRound(const std::vector& SeqHistory sequential_history; // TODO: `IsRunning` field might be added to `Task` instead std::unordered_set started_tasks; + std::unordered_map resumes_count; // TaskId -> Appearences in `tasks_ordering` + + for (int next_task_id : tasks_ordering) { + resumes_count[next_task_id]++; + } + + // log() << "\n\n\nReplaying round: "; + // for (int task_id : tasks_ordering) log() << task_id << " "; + // log() << "\n"; for (int next_task_id : tasks_ordering) { bool is_new = started_tasks.contains(next_task_id) ? false : started_tasks.insert(next_task_id).second; @@ -75,8 +84,17 @@ StrategyScheduler::Result StrategyScheduler::replayRound(const std::vector& if (next_task->IsReturned()) continue; - next_task->Resume(); + // if this is the last time this task appears in `tasks_ordering`, then complete it fully. + if (resumes_count[next_task_id] == 0) { + next_task->Terminate(); + } + else { + resumes_count[next_task_id]--; + next_task->Resume(); + } + if (next_task->IsReturned()) { + // log() << "Return from task: " << next_task_id << "\n"; auto result = next_task->GetRetVal(); sequential_history.emplace_back(Response(next_task, result, thread_id)); } @@ -142,11 +160,14 @@ void StrategyScheduler::minimize( if (task_i_id == task_j_id) continue; - // log() << "Try to remove task with id: " << task_i_id << " and " << task_j_id << "\n"; + // log() << "Try to remove tasks with ids: " << task_i_id << " and " << task_j_id << "\n"; std::vector new_ordering = getTasksOrdering(nonlinear_history.first, { task_i_id, task_j_id }); auto new_histories = replayRound(new_ordering); if (new_histories.has_value()) { + // sequential history (Invoke/Response) must have even number of history events + assert(new_histories.value().second.size() % 2 == 0); + nonlinear_history.first.swap(new_histories.value().first); nonlinear_history.second.swap(new_histories.value().second); @@ -159,7 +180,8 @@ void StrategyScheduler::minimize( } } - // replay round one last time to put coroutines in `returned` state + // replay minimized round one last time to put coroutines in `returned` state + // (because multiple failed attempts to minimize new scenarios could leave tasks in invalid state) replayRound(getTasksOrdering(nonlinear_history.first, {})); } From e735ae2ff1c55107733f2855035d93c8255b9014 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Tue, 17 Dec 2024 18:49:07 +0000 Subject: [PATCH 06/47] Remove useless hashmap --- runtime/scheduler.cpp | 5 ----- 1 file changed, 5 deletions(-) diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp index 0b3e5ad7..72f5f933 100644 --- a/runtime/scheduler.cpp +++ b/runtime/scheduler.cpp @@ -123,7 +123,6 @@ std::vector StrategyScheduler::getTasksOrdering(const FullHistory& full_his void StrategyScheduler::minimize( std::pair& nonlinear_history ) { - std::unordered_set removed_tasks; std::vector> tasks; for (const HistoryEvent& event : nonlinear_history.second) { @@ -143,7 +142,6 @@ void StrategyScheduler::minimize( if (new_histories.has_value()) { nonlinear_history.first.swap(new_histories.value().first); nonlinear_history.second.swap(new_histories.value().second); - removed_tasks.insert(task_id); task.get()->SetRemoved(true); } } @@ -171,9 +169,6 @@ void StrategyScheduler::minimize( nonlinear_history.first.swap(new_histories.value().first); nonlinear_history.second.swap(new_histories.value().second); - removed_tasks.insert(task_i_id); - removed_tasks.insert(task_j_id); - task_i.get()->SetRemoved(true); task_j.get()->SetRemoved(true); } From aa84d7a7d2ee280362d54ad1f8cf6352389da2f3 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Wed, 18 Dec 2024 18:37:39 +0000 Subject: [PATCH 07/47] Add nonlinearized round minimization with threads rescheduling (for random startegy only yet) --- runtime/include/pick_strategy.h | 2 +- runtime/include/scheduler.h | 15 ++- runtime/scheduler.cpp | 205 -------------------------------- 3 files changed, 15 insertions(+), 207 deletions(-) delete mode 100644 runtime/scheduler.cpp diff --git a/runtime/include/pick_strategy.h b/runtime/include/pick_strategy.h index 19cff7f0..71d2f5cc 100644 --- a/runtime/include/pick_strategy.h +++ b/runtime/include/pick_strategy.h @@ -76,7 +76,7 @@ struct PickStrategy : public BaseStrategyWithThreads { is_new, current_thread}; } - // TODO: same iplementation for pct + // TODO: same implementation for pct std::optional> GetTask(int task_id) override { // TODO: can this be optimized? int thread_id = 0; diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index 7b13be8f..8d89f5ad 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -274,6 +274,19 @@ 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"; + // debug(stderr, "run round: %d\n", i); + // auto seq_history = runRound(); + // if (seq_history.has_value()) { + // return seq_history; + // } + // log() << "===============================================\n\n"; + // log().flush(); + // strategy.StartNextRound(); + // } + + // return std::nullopt; for (size_t i = 0; i < max_rounds; ++i) { log() << "run round: " << i << "\n"; debug(stderr, "run round: %d\n", i); @@ -312,7 +325,7 @@ struct StrategyScheduler : public SchedulerWithReplay { log().flush(); strategy.StartNextRound(); } - + return std::nullopt; } diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp deleted file mode 100644 index 72f5f933..00000000 --- a/runtime/scheduler.cpp +++ /dev/null @@ -1,205 +0,0 @@ -#include - -#include "include/scheduler.h" -#include "include/logger.h" -#include "include/pretty_print.h" - -StrategyScheduler::StrategyScheduler(Strategy &sched_class, - ModelChecker &checker, - PrettyPrinter &pretty_printer, - size_t max_tasks, size_t max_rounds) - : strategy(sched_class), - checker(checker), - pretty_printer(pretty_printer), - max_tasks(max_tasks), - max_rounds(max_rounds) {} - -Scheduler::Result StrategyScheduler::runRound() { - // History of invoke and response events which is required for the checker - std::vector> sequential_history; - // Full history of the current execution in the Run function - std::vector> full_history; - - for (size_t finished_tasks = 0; finished_tasks < max_tasks;) { - auto [next_task, is_new, thread_id] = strategy.Next(); - - // fill the sequential history - if (is_new) { - sequential_history.emplace_back(Invoke(next_task, thread_id)); - } - full_history.emplace_back(next_task); - - next_task->Resume(); - if (next_task->IsReturned()) { - finished_tasks++; - - auto result = next_task->GetRetVal(); - sequential_history.emplace_back(Response(next_task, result, thread_id)); - } - } - - pretty_printer.PrettyPrint(sequential_history, log()); - - if (!checker.Check(sequential_history)) { - return std::make_pair(full_history, sequential_history); - } - - return std::nullopt; -} - -StrategyScheduler::Result StrategyScheduler::replayRound(const std::vector& tasks_ordering) { - strategy.ResetCurrentRound(); - - // History of invoke and response events which is required for the checker - FullHistory full_history; - SeqHistory sequential_history; - // TODO: `IsRunning` field might be added to `Task` instead - std::unordered_set started_tasks; - std::unordered_map resumes_count; // TaskId -> Appearences in `tasks_ordering` - - for (int next_task_id : tasks_ordering) { - resumes_count[next_task_id]++; - } - - // log() << "\n\n\nReplaying round: "; - // for (int task_id : tasks_ordering) log() << task_id << " "; - // log() << "\n"; - - for (int next_task_id : tasks_ordering) { - bool is_new = started_tasks.contains(next_task_id) ? false : started_tasks.insert(next_task_id).second; - auto task_info = strategy.GetTask(next_task_id); - - if (!task_info.has_value()) { - std::cerr << "No task with id " << next_task_id << " exists in round" << std::endl; - throw std::runtime_error("Invalid task id"); - } - - auto [next_task, thread_id] = task_info.value(); - if (is_new) { - sequential_history.emplace_back(Invoke(next_task, thread_id)); - } - full_history.emplace_back(next_task); - - // log() << "Resume task: id=" << next_task_id << ", " << next_task->GetName() << ", thread-id=" << thread_id << "\n"; - - if (next_task->IsReturned()) continue; - - // if this is the last time this task appears in `tasks_ordering`, then complete it fully. - if (resumes_count[next_task_id] == 0) { - next_task->Terminate(); - } - else { - resumes_count[next_task_id]--; - next_task->Resume(); - } - - if (next_task->IsReturned()) { - // log() << "Return from task: " << next_task_id << "\n"; - auto result = next_task->GetRetVal(); - sequential_history.emplace_back(Response(next_task, result, thread_id)); - } - } - - //pretty_printer.PrettyPrint(sequential_history, log()); - - if (!checker.Check(sequential_history)) { - return std::make_pair(full_history, sequential_history); - } - - return std::nullopt; -} - -std::vector StrategyScheduler::getTasksOrdering(const FullHistory& full_history, const std::unordered_set exclude_task_ids) const { - std::vector tasks_ordering; - - for (auto& task : full_history) { - if (exclude_task_ids.contains(task.get()->GetId())) continue; - tasks_ordering.emplace_back(task.get()->GetId()); - } - - return tasks_ordering; -} - -void StrategyScheduler::minimize( - std::pair& nonlinear_history -) { - std::vector> tasks; - - for (const HistoryEvent& event : nonlinear_history.second) { - if (std::holds_alternative(event)) { - tasks.push_back(std::get(event).GetTask()); - } - } - - // remove single task - for (auto& task : tasks) { - int task_id = task.get()->GetId(); - - // log() << "Try to remove task with id: " << task_id << "\n"; - std::vector new_ordering = getTasksOrdering(nonlinear_history.first, { task_id }); - auto new_histories = replayRound(new_ordering); - - if (new_histories.has_value()) { - nonlinear_history.first.swap(new_histories.value().first); - nonlinear_history.second.swap(new_histories.value().second); - task.get()->SetRemoved(true); - } - } - - // remove two tasks (for operations with semantics of add/remove) - for (auto& task_i : tasks) { - if (task_i.get()->IsRemoved()) continue; - - for (auto& task_j : tasks) { - if (task_j.get()->IsRemoved()) continue; - - int task_i_id = task_i.get()->GetId(); - int task_j_id = task_j.get()->GetId(); - - if (task_i_id == task_j_id) continue; - - // log() << "Try to remove tasks with ids: " << task_i_id << " and " << task_j_id << "\n"; - std::vector new_ordering = getTasksOrdering(nonlinear_history.first, { task_i_id, task_j_id }); - auto new_histories = replayRound(new_ordering); - - if (new_histories.has_value()) { - // sequential history (Invoke/Response) must have even number of history events - assert(new_histories.value().second.size() % 2 == 0); - - nonlinear_history.first.swap(new_histories.value().first); - nonlinear_history.second.swap(new_histories.value().second); - - task_i.get()->SetRemoved(true); - task_j.get()->SetRemoved(true); - } - } - } - - // replay minimized round one last time to put coroutines in `returned` state - // (because multiple failed attempts to minimize new scenarios could leave tasks in invalid state) - replayRound(getTasksOrdering(nonlinear_history.first, {})); -} - -Scheduler::Result StrategyScheduler::Run() { - for (size_t i = 0; i < max_rounds; ++i) { - log() << "run round: " << i << "\n"; - auto histories = runRound(); - - if (histories.has_value()) { - auto& [full_history, sequential_history] = histories.value(); - - log() << "Full nonlinear scenario: \n"; - pretty_printer.PrettyPrint(sequential_history, log()); - - log() << "Minimizing...\n"; - minimize(histories.value()); - - return histories; - } - log() << "===============================================\n\n"; - log().flush(); - strategy.StartNextRound(); - } - - return std::nullopt; -} \ No newline at end of file From c96f4bebc834f7ea8933ba314dcb0eece2f4319c Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Wed, 18 Dec 2024 18:51:08 +0000 Subject: [PATCH 08/47] Add comment --- runtime/include/scheduler.h | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index 8d89f5ad..4c3cb334 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -274,19 +274,6 @@ 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"; - // debug(stderr, "run round: %d\n", i); - // auto seq_history = runRound(); - // if (seq_history.has_value()) { - // return seq_history; - // } - // log() << "===============================================\n\n"; - // log().flush(); - // strategy.StartNextRound(); - // } - - // return std::nullopt; for (size_t i = 0; i < max_rounds; ++i) { log() << "run round: " << i << "\n"; debug(stderr, "run round: %d\n", i); From abfe8aefb1488fc9081050bae5796a27878db3c9 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Thu, 2 Jan 2025 09:08:02 +0000 Subject: [PATCH 09/47] Extract task removal callbacks to classes --- runtime/include/scheduler.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index 4c3cb334..13d1b1e6 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -4,6 +4,7 @@ #include #include +#include "scheduler_fwd.h" #include "lib.h" #include "lincheck.h" #include "logger.h" @@ -12,6 +13,7 @@ #include "pretty_print.h" #include "scheduler_fwd.h" #include "stable_vector.h" +#include "minimization.h" /// Generated by some strategy task, /// that may be not executed due to constraints of data structure From 9b2552dff900382be60480e6367d960f02655270 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Thu, 2 Jan 2025 13:20:09 +0000 Subject: [PATCH 10/47] Add common base for pct and pick strategies --- runtime/include/scheduler.h | 1 + 1 file changed, 1 insertion(+) diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index 13d1b1e6..79762fe6 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -3,6 +3,7 @@ #include #include #include +#include #include "scheduler_fwd.h" #include "lib.h" From 6a3e8aa99ed6124c25ddc94391358dae89f0ed87 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Sat, 4 Jan 2025 15:09:52 +0000 Subject: [PATCH 11/47] Add NextSchedule method for pct --- runtime/include/pct_strategy.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/runtime/include/pct_strategy.h b/runtime/include/pct_strategy.h index dd3d9852..1ecd7c87 100644 --- a/runtime/include/pct_strategy.h +++ b/runtime/include/pct_strategy.h @@ -183,8 +183,7 @@ struct PctStrategy : public BaseStrategyWithThreads { current_schedule_length = 0; // current_depth have been increased - size_t new_k = std::reduce(k_statistics.begin(), k_statistics.end()) / - k_statistics.size(); + size_t new_k = std::reduce(k_statistics.begin(), k_statistics.end()) / k_statistics.size(); log() << "k: " << new_k << "\n"; PrepareForDepth(current_depth, new_k); } From 723169004b5117f6c31dd72dec6cea4c5a257983 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Sat, 4 Jan 2025 15:43:53 +0000 Subject: [PATCH 12/47] Extract minimizors to separate classes --- runtime/scheduler.cpp | 189 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 189 insertions(+) create mode 100644 runtime/scheduler.cpp diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp new file mode 100644 index 00000000..21f36acc --- /dev/null +++ b/runtime/scheduler.cpp @@ -0,0 +1,189 @@ +#include + +#include "include/scheduler.h" +#include "include/logger.h" +#include "include/pretty_print.h" +#include "include/minimization.h" + +StrategyScheduler::StrategyScheduler(Strategy &sched_class, + ModelChecker &checker, + PrettyPrinter &pretty_printer, + size_t max_tasks, size_t max_rounds) + : strategy(sched_class), + checker(checker), + pretty_printer(pretty_printer), + max_tasks(max_tasks), + max_rounds(max_rounds) {} + +Scheduler::Result StrategyScheduler::runRound() { + // History of invoke and response events which is required for the checker + SeqHistory sequential_history; + // Full history of the current execution in the Run function + FullHistory full_history; + + for (size_t finished_tasks = 0; finished_tasks < max_tasks;) { + auto [next_task, is_new, thread_id] = strategy.Next(); + + // fill the sequential history + if (is_new) { + sequential_history.emplace_back(Invoke(next_task, thread_id)); + } + full_history.emplace_back(next_task); + + next_task->Resume(); + if (next_task->IsReturned()) { + finished_tasks++; + + auto result = next_task->GetRetVal(); + sequential_history.emplace_back(Response(next_task, result, thread_id)); + } + } + + pretty_printer.PrettyPrint(sequential_history, log()); + + if (!checker.Check(sequential_history)) { + return std::make_pair(full_history, sequential_history); + } + + return std::nullopt; +} + +StrategyScheduler::Result StrategyScheduler::exploreRound(int runs) { + for (int i = 0; i < runs; ++i) { + // log() << "Run " << i + 1 << "/" << runs << "\n"; + strategy.ResetCurrentRound(); + SeqHistory sequential_history; + FullHistory full_history; + + for (int tasks_to_run = strategy.GetValidTasksCount(); tasks_to_run > 0;) { + auto [next_task, is_new, thread_id] = strategy.NextSchedule(); + + if (is_new) { + sequential_history.emplace_back(Invoke(next_task, thread_id)); + } + full_history.emplace_back(next_task); + + next_task->Resume(); + if (next_task->IsReturned()) { + tasks_to_run--; + + auto result = next_task->GetRetVal(); + sequential_history.emplace_back(Response(next_task, result, thread_id)); + } + } + + + if (!checker.Check(sequential_history)) { + // log() << "New nonlinearized scenario:\n"; + // pretty_printer.PrettyPrint(sequential_history, log()); + return std::make_pair(full_history, sequential_history); + } + } + + return std::nullopt; +} + +StrategyScheduler::Result StrategyScheduler::replayRound(const std::vector& tasks_ordering) { + strategy.ResetCurrentRound(); + + // History of invoke and response events which is required for the checker + FullHistory full_history; + SeqHistory sequential_history; + // TODO: `IsRunning` field might be added to `Task` instead + std::unordered_set started_tasks; + std::unordered_map resumes_count; // task id -> number of appearences in `tasks_ordering` + + for (int next_task_id : tasks_ordering) { + resumes_count[next_task_id]++; + } + + for (int next_task_id : tasks_ordering) { + bool is_new = started_tasks.contains(next_task_id) ? false : started_tasks.insert(next_task_id).second; + auto task_info = strategy.GetTask(next_task_id); + + if (!task_info.has_value()) { + std::cerr << "No task with id " << next_task_id << " exists in round" << std::endl; + throw std::runtime_error("Invalid task id"); + } + + auto [next_task, thread_id] = task_info.value(); + if (is_new) { + sequential_history.emplace_back(Invoke(next_task, thread_id)); + } + full_history.emplace_back(next_task); + + if (next_task->IsReturned()) continue; + + // if this is the last time this task appears in `tasks_ordering`, then complete it fully. + if (resumes_count[next_task_id] == 0) { + next_task->Terminate(); + } + else { + resumes_count[next_task_id]--; + next_task->Resume(); + } + + if (next_task->IsReturned()) { + auto result = next_task->GetRetVal(); + sequential_history.emplace_back(Response(next_task, result, thread_id)); + } + } + + // pretty_printer.PrettyPrint(sequential_history, log()); + + if (!checker.Check(sequential_history)) { + return std::make_pair(full_history, sequential_history); + } + + return std::nullopt; +} + +std::vector StrategyScheduler::getTasksOrdering( + const FullHistory& full_history, + const std::unordered_set exclude_task_ids +) { + std::vector tasks_ordering; + + for (auto& task : full_history) { + if (exclude_task_ids.contains(task.get()->GetId())) continue; + tasks_ordering.emplace_back(task.get()->GetId()); + } + + return tasks_ordering; +} + +void StrategyScheduler::minimize( + Scheduler::Histories& nonlinear_history, + const RoundMinimizor& minimizor +) { + minimizor.minimize(*this, nonlinear_history); +} + +Scheduler::Result StrategyScheduler::Run() { + for (size_t i = 0; i < max_rounds; ++i) { + log() << "run round: " << i << "\n"; + auto histories = runRound(); + // TODO: make `exploration_runs` a command-line argument + int exploration_runs = 10; + + if (histories.has_value()) { + auto& [full_history, sequential_history] = histories.value(); + + log() << "Full nonlinear scenario: \n"; + pretty_printer.PrettyPrint(sequential_history, log()); + + log() << "Minimizing same interleaving...\n"; + minimize(histories.value(), InterleavingMinimizor()); + + log() << "Minimizing with rescheduling (runs: " << exploration_runs << ")...\n"; + minimize(histories.value(), StrategyMinimizor(exploration_runs)); + + return histories; + } + log() << "===============================================\n\n"; + log().flush(); + strategy.StartNextRound(); + } + + return std::nullopt; +} \ No newline at end of file From af6c7b3526afb252c6ccbfbf1cf7c489e5d8e91f Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Sat, 4 Jan 2025 15:54:57 +0000 Subject: [PATCH 13/47] Rename minimizors --- runtime/scheduler.cpp | 189 ------------------------------------------ 1 file changed, 189 deletions(-) delete mode 100644 runtime/scheduler.cpp diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp deleted file mode 100644 index 21f36acc..00000000 --- a/runtime/scheduler.cpp +++ /dev/null @@ -1,189 +0,0 @@ -#include - -#include "include/scheduler.h" -#include "include/logger.h" -#include "include/pretty_print.h" -#include "include/minimization.h" - -StrategyScheduler::StrategyScheduler(Strategy &sched_class, - ModelChecker &checker, - PrettyPrinter &pretty_printer, - size_t max_tasks, size_t max_rounds) - : strategy(sched_class), - checker(checker), - pretty_printer(pretty_printer), - max_tasks(max_tasks), - max_rounds(max_rounds) {} - -Scheduler::Result StrategyScheduler::runRound() { - // History of invoke and response events which is required for the checker - SeqHistory sequential_history; - // Full history of the current execution in the Run function - FullHistory full_history; - - for (size_t finished_tasks = 0; finished_tasks < max_tasks;) { - auto [next_task, is_new, thread_id] = strategy.Next(); - - // fill the sequential history - if (is_new) { - sequential_history.emplace_back(Invoke(next_task, thread_id)); - } - full_history.emplace_back(next_task); - - next_task->Resume(); - if (next_task->IsReturned()) { - finished_tasks++; - - auto result = next_task->GetRetVal(); - sequential_history.emplace_back(Response(next_task, result, thread_id)); - } - } - - pretty_printer.PrettyPrint(sequential_history, log()); - - if (!checker.Check(sequential_history)) { - return std::make_pair(full_history, sequential_history); - } - - return std::nullopt; -} - -StrategyScheduler::Result StrategyScheduler::exploreRound(int runs) { - for (int i = 0; i < runs; ++i) { - // log() << "Run " << i + 1 << "/" << runs << "\n"; - strategy.ResetCurrentRound(); - SeqHistory sequential_history; - FullHistory full_history; - - for (int tasks_to_run = strategy.GetValidTasksCount(); tasks_to_run > 0;) { - auto [next_task, is_new, thread_id] = strategy.NextSchedule(); - - if (is_new) { - sequential_history.emplace_back(Invoke(next_task, thread_id)); - } - full_history.emplace_back(next_task); - - next_task->Resume(); - if (next_task->IsReturned()) { - tasks_to_run--; - - auto result = next_task->GetRetVal(); - sequential_history.emplace_back(Response(next_task, result, thread_id)); - } - } - - - if (!checker.Check(sequential_history)) { - // log() << "New nonlinearized scenario:\n"; - // pretty_printer.PrettyPrint(sequential_history, log()); - return std::make_pair(full_history, sequential_history); - } - } - - return std::nullopt; -} - -StrategyScheduler::Result StrategyScheduler::replayRound(const std::vector& tasks_ordering) { - strategy.ResetCurrentRound(); - - // History of invoke and response events which is required for the checker - FullHistory full_history; - SeqHistory sequential_history; - // TODO: `IsRunning` field might be added to `Task` instead - std::unordered_set started_tasks; - std::unordered_map resumes_count; // task id -> number of appearences in `tasks_ordering` - - for (int next_task_id : tasks_ordering) { - resumes_count[next_task_id]++; - } - - for (int next_task_id : tasks_ordering) { - bool is_new = started_tasks.contains(next_task_id) ? false : started_tasks.insert(next_task_id).second; - auto task_info = strategy.GetTask(next_task_id); - - if (!task_info.has_value()) { - std::cerr << "No task with id " << next_task_id << " exists in round" << std::endl; - throw std::runtime_error("Invalid task id"); - } - - auto [next_task, thread_id] = task_info.value(); - if (is_new) { - sequential_history.emplace_back(Invoke(next_task, thread_id)); - } - full_history.emplace_back(next_task); - - if (next_task->IsReturned()) continue; - - // if this is the last time this task appears in `tasks_ordering`, then complete it fully. - if (resumes_count[next_task_id] == 0) { - next_task->Terminate(); - } - else { - resumes_count[next_task_id]--; - next_task->Resume(); - } - - if (next_task->IsReturned()) { - auto result = next_task->GetRetVal(); - sequential_history.emplace_back(Response(next_task, result, thread_id)); - } - } - - // pretty_printer.PrettyPrint(sequential_history, log()); - - if (!checker.Check(sequential_history)) { - return std::make_pair(full_history, sequential_history); - } - - return std::nullopt; -} - -std::vector StrategyScheduler::getTasksOrdering( - const FullHistory& full_history, - const std::unordered_set exclude_task_ids -) { - std::vector tasks_ordering; - - for (auto& task : full_history) { - if (exclude_task_ids.contains(task.get()->GetId())) continue; - tasks_ordering.emplace_back(task.get()->GetId()); - } - - return tasks_ordering; -} - -void StrategyScheduler::minimize( - Scheduler::Histories& nonlinear_history, - const RoundMinimizor& minimizor -) { - minimizor.minimize(*this, nonlinear_history); -} - -Scheduler::Result StrategyScheduler::Run() { - for (size_t i = 0; i < max_rounds; ++i) { - log() << "run round: " << i << "\n"; - auto histories = runRound(); - // TODO: make `exploration_runs` a command-line argument - int exploration_runs = 10; - - if (histories.has_value()) { - auto& [full_history, sequential_history] = histories.value(); - - log() << "Full nonlinear scenario: \n"; - pretty_printer.PrettyPrint(sequential_history, log()); - - log() << "Minimizing same interleaving...\n"; - minimize(histories.value(), InterleavingMinimizor()); - - log() << "Minimizing with rescheduling (runs: " << exploration_runs << ")...\n"; - minimize(histories.value(), StrategyMinimizor(exploration_runs)); - - return histories; - } - log() << "===============================================\n\n"; - log().flush(); - strategy.StartNextRound(); - } - - return std::nullopt; -} \ No newline at end of file From 33c99bcf736f488d2f4ca0f9c3b87d9d4003dc51 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Wed, 8 Jan 2025 11:45:04 +0000 Subject: [PATCH 14/47] Add 'pragma once' to minimization.h --- runtime/include/lib.h | 2 -- runtime/include/scheduler.h | 3 +-- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/runtime/include/lib.h b/runtime/include/lib.h index 492eac82..26142d75 100644 --- a/runtime/include/lib.h +++ b/runtime/include/lib.h @@ -96,8 +96,6 @@ struct CoroBase : public std::enable_shared_from_this { } return is_blocked; } - // Sets IsRemoved state. - void SetRemoved(bool is_removed); // Checks if the coroutine is parked. bool IsParked() const; diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index 79762fe6..48100971 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -319,7 +319,7 @@ struct StrategyScheduler : public SchedulerWithReplay { return std::nullopt; } - protected: +protected: // Runs a round with some interleaving while generating it Result RunRound() override { // History of invoke and response events which is required for the checker @@ -384,7 +384,6 @@ struct StrategyScheduler : public SchedulerWithReplay { Response(next_task, result, thread_id)); } } - if (!checker.Check(sequential_history)) { // log() << "New nonlinearized scenario:\n"; // pretty_printer.PrettyPrint(sequential_history, log()); From 27ccfce6d99f59d4dad924aa171db0187ccc3820 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Tue, 14 Jan 2025 22:38:07 +0000 Subject: [PATCH 15/47] Fix compilation --- runtime/include/scheduler.h | 1 + runtime/minimization_smart.cpp | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index 48100971..b16c6834 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -15,6 +15,7 @@ #include "scheduler_fwd.h" #include "stable_vector.h" #include "minimization.h" +#include "minimization_smart.h" /// Generated by some strategy task, /// that may be not executed due to constraints of data structure diff --git a/runtime/minimization_smart.cpp b/runtime/minimization_smart.cpp index bc047f00..ca4dc256 100644 --- a/runtime/minimization_smart.cpp +++ b/runtime/minimization_smart.cpp @@ -236,4 +236,4 @@ SmartMinimizor::Solution::Solution(const Strategy& strategy, float SmartMinimizor::Solution::GetFitness() const { return fitness; } -int SmartMinimizor::Solution::GetValidTasks() const { return valid_tasks; } \ No newline at end of file +int SmartMinimizor::Solution::GetValidTasks() const { return valid_tasks; } From 456dc7c59ec1a888fddcb35aa4d6fe8fc4fadf7c Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Wed, 22 Jan 2025 10:34:39 +0000 Subject: [PATCH 16/47] Enhance smart minimization --- runtime/include/scheduler.h | 1 + 1 file changed, 1 insertion(+) diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index b16c6834..d8b5f762 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -142,6 +142,7 @@ struct BaseStrategyWithThreads : public Strategy { } void ResetCurrentRound() override { + // log() << "Terminating tasks\n"; TerminateTasks(); //state.Reset(); for (auto& thread : threads) { From 82996c4b0359aa0194970b4f68d4edc6980f6e0e Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Wed, 5 Feb 2025 23:58:42 +0000 Subject: [PATCH 17/47] Remove some comments --- runtime/include/scheduler.h | 1 - 1 file changed, 1 deletion(-) diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index d8b5f762..b16c6834 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -142,7 +142,6 @@ struct BaseStrategyWithThreads : public Strategy { } void ResetCurrentRound() override { - // log() << "Terminating tasks\n"; TerminateTasks(); //state.Reset(); for (auto& thread : threads) { From 4a2c2633a75883c8253d239aa1cd863a7120fcb7 Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Sat, 8 Feb 2025 18:52:38 +0000 Subject: [PATCH 18/47] Refactor some code --- runtime/scheduler.cpp | 188 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 188 insertions(+) create mode 100644 runtime/scheduler.cpp diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp new file mode 100644 index 00000000..3ae52c23 --- /dev/null +++ b/runtime/scheduler.cpp @@ -0,0 +1,188 @@ +#include + +#include "include/scheduler.h" +#include "include/logger.h" +#include "include/pretty_print.h" +#include "include/minimization.h" +#include "include/minimization_smart.h" + +StrategyScheduler::StrategyScheduler(Strategy &sched_class, + ModelChecker &checker, + PrettyPrinter &pretty_printer, + size_t max_tasks, + size_t max_rounds, + size_t exploration_runs, + size_t minimization_runs) + : strategy(sched_class), + checker(checker), + pretty_printer(pretty_printer), + max_tasks(max_tasks), + max_rounds(max_rounds), + exploration_runs(exploration_runs), + minimization_runs(minimization_runs) {} + +Scheduler::Result StrategyScheduler::RunRound() { + // History of invoke and response events which is required for the checker + SeqHistory sequential_history; + // Full history of the current execution in the Run function + FullHistory full_history; + + for (size_t finished_tasks = 0; finished_tasks < max_tasks;) { + auto [next_task, is_new, thread_id] = strategy.Next(); + + // fill the sequential history + if (is_new) { + sequential_history.emplace_back(Invoke(next_task, thread_id)); + } + full_history.emplace_back(next_task); + + next_task->Resume(); + if (next_task->IsReturned()) { + finished_tasks++; + + auto result = next_task->GetRetVal(); + sequential_history.emplace_back(Response(next_task, result, thread_id)); + } + } + + pretty_printer.PrettyPrint(sequential_history, log()); + + if (!checker.Check(sequential_history)) { + return std::make_pair(full_history, sequential_history); + } + + return std::nullopt; +} + +StrategyScheduler::Result StrategyScheduler::ExploreRound(int runs) { + for (int i = 0; i < runs; ++i) { + // log() << "Run " << i + 1 << "/" << runs << "\n"; + strategy.ResetCurrentRound(); + SeqHistory sequential_history; + FullHistory full_history; + + for (int tasks_to_run = strategy.GetValidTasksCount(); tasks_to_run > 0;) { + auto [next_task, is_new, thread_id] = strategy.NextSchedule(); + + if (is_new) { + sequential_history.emplace_back(Invoke(next_task, thread_id)); + } + full_history.emplace_back(next_task); + + next_task->Resume(); + if (next_task->IsReturned()) { + tasks_to_run--; + + auto result = next_task->GetRetVal(); + sequential_history.emplace_back(Response(next_task, result, thread_id)); + } + } + + if (!checker.Check(sequential_history)) { + // log() << "New nonlinearized scenario:\n"; + // pretty_printer.PrettyPrint(sequential_history, log()); + return std::make_pair(full_history, sequential_history); + } + } + + return std::nullopt; +} + +StrategyScheduler::Result StrategyScheduler::ReplayRound(const std::vector& tasks_ordering) { + strategy.ResetCurrentRound(); + + // History of invoke and response events which is required for the checker + FullHistory full_history; + SeqHistory sequential_history; + // TODO: `IsRunning` field might be added to `Task` instead + std::unordered_set started_tasks; + std::unordered_map resumes_count; // task id -> number of appearences in `tasks_ordering` + + for (int next_task_id : tasks_ordering) { + resumes_count[next_task_id]++; + } + + for (int next_task_id : tasks_ordering) { + bool is_new = started_tasks.contains(next_task_id) ? false : started_tasks.insert(next_task_id).second; + auto task_info = strategy.GetTask(next_task_id); + + if (!task_info.has_value()) { + std::cerr << "No task with id " << next_task_id << " exists in round" << std::endl; + throw std::runtime_error("Invalid task id"); + } + + auto [next_task, thread_id] = task_info.value(); + if (is_new) { + sequential_history.emplace_back(Invoke(next_task, thread_id)); + } + full_history.emplace_back(next_task); + + if (next_task->IsReturned()) continue; + + // if this is the last time this task appears in `tasks_ordering`, then complete it fully. + if (resumes_count[next_task_id] == 0) { + next_task->Terminate(); + } + else { + resumes_count[next_task_id]--; + next_task->Resume(); + } + + if (next_task->IsReturned()) { + auto result = next_task->GetRetVal(); + sequential_history.emplace_back(Response(next_task, result, thread_id)); + } + } + + // pretty_printer.PrettyPrint(sequential_history, log()); + + if (!checker.Check(sequential_history)) { + return std::make_pair(full_history, sequential_history); + } + + return std::nullopt; +} + + +Strategy& StrategyScheduler::GetStrategy() const { + return strategy; +} + +void StrategyScheduler::Minimize( + Scheduler::BothHistories& nonlinear_history, + const RoundMinimizor& minimizor +) { + minimizor.Minimize(*this, nonlinear_history); +} + +Scheduler::Result StrategyScheduler::Run() { + for (size_t i = 0; i < max_rounds; ++i) { + log() << "run round: " << i << "\n"; + auto histories = RunRound(); + + if (histories.has_value()) { + auto& [full_history, sequential_history] = histories.value(); + + log() << "Full nonlinear scenario: \n"; + pretty_printer.PrettyPrint(sequential_history, log()); + + log() << "Minimizing same interleaving...\n"; + Minimize(histories.value(), SameInterleavingMinimizor()); + + log() << "Minimizing with rescheduling (exploration runs: " << exploration_runs << ")...\n"; + Minimize(histories.value(), StrategyExplorationMinimizor(exploration_runs)); + + log() << "Minimizing with smart minimizor (exploration runs: " + << exploration_runs << ", minimization runs: " + << minimization_runs << ")...\n"; + Minimize(histories.value(), SmartMinimizor(exploration_runs, minimization_runs, pretty_printer)); + + return histories; + } + log() << "===============================================\n\n"; + log().flush(); + strategy.StartNextRound(); + } + + return std::nullopt; +} \ No newline at end of file From b497fc89d67022820c0bd0ae06a7c2b9e2fc158a Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Sat, 8 Feb 2025 18:57:06 +0000 Subject: [PATCH 19/47] Minor code-style fixes --- runtime/scheduler.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp index 3ae52c23..a6fcd4ee 100644 --- a/runtime/scheduler.cpp +++ b/runtime/scheduler.cpp @@ -143,7 +143,6 @@ StrategyScheduler::Result StrategyScheduler::ReplayRound(const std::vector& return std::nullopt; } - Strategy& StrategyScheduler::GetStrategy() const { return strategy; } From 10f4cbb7ad483e443dffda7e600c8c86b131514e Mon Sep 17 00:00:00 2001 From: Dmitrii Art Date: Sun, 9 Feb 2025 20:09:03 +0000 Subject: [PATCH 20/47] Add new printing to scheduler after each minimization step --- runtime/scheduler.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp index a6fcd4ee..8f1b9d42 100644 --- a/runtime/scheduler.cpp +++ b/runtime/scheduler.cpp @@ -167,9 +167,13 @@ Scheduler::Result StrategyScheduler::Run() { log() << "Minimizing same interleaving...\n"; Minimize(histories.value(), SameInterleavingMinimizor()); + log() << "Minimized to:\n"; + pretty_printer.PrettyPrint(sequential_history, 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()); log() << "Minimizing with smart minimizor (exploration runs: " << exploration_runs << ", minimization runs: " From 1b1dd07adc80222e96d02756cb1337a322d2f294 Mon Sep 17 00:00:00 2001 From: Dmitrii Art <51288598+dmitrii-artuhov@users.noreply.github.com> Date: Wed, 26 Feb 2025 01:22:56 +0100 Subject: [PATCH 21/47] Add nonlinearized tests for minimization (#4) * Add simple nonlinearized tests * Add new nonlinearizable treiber stack impl * Add nonlinearizable set * Add Michael-Scott queue. Update yieldpass to match the 'master' branch. * Fix bug in round replaying with incorrect 'resume_count' decrementing * Refactor tests --- runtime/scheduler.cpp | 13 +++++++++++-- verifying/targets/nonlinear_set.cpp | 2 +- verifying/targets/nonlinear_treiber_stack.cpp | 2 +- 3 files changed, 13 insertions(+), 4 deletions(-) diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp index 8f1b9d42..6f9622b8 100644 --- a/runtime/scheduler.cpp +++ b/runtime/scheduler.cpp @@ -96,6 +96,7 @@ StrategyScheduler::Result StrategyScheduler::ReplayRound(const std::vector& SeqHistory sequential_history; // TODO: `IsRunning` field might be added to `Task` instead std::unordered_set started_tasks; + std::unordered_set finished_tasks; std::unordered_map resumes_count; // task id -> number of appearences in `tasks_ordering` for (int next_task_id : tasks_ordering) { @@ -112,29 +113,37 @@ StrategyScheduler::Result StrategyScheduler::ReplayRound(const std::vector& } auto [next_task, thread_id] = task_info.value(); + if (next_task->IsReturned()) { + // we could witness the task that still has resumes (`resumes_count[next_task_id] > 0`), + // but is already returned, so we just skip it, because its `Response` was already added + assert(finished_tasks.contains(next_task_id)); + continue; + } + if (is_new) { sequential_history.emplace_back(Invoke(next_task, thread_id)); } full_history.emplace_back(next_task); - if (next_task->IsReturned()) continue; // if this is the last time this task appears in `tasks_ordering`, then complete it fully. + resumes_count[next_task_id]--; if (resumes_count[next_task_id] == 0) { next_task->Terminate(); } else { - resumes_count[next_task_id]--; next_task->Resume(); } if (next_task->IsReturned()) { auto result = next_task->GetRetVal(); sequential_history.emplace_back(Response(next_task, result, thread_id)); + finished_tasks.insert(next_task_id); } } // pretty_printer.PrettyPrint(sequential_history, log()); + assert(started_tasks.size() == finished_tasks.size()); if (!checker.Check(sequential_history)) { return std::make_pair(full_history, sequential_history); diff --git a/verifying/targets/nonlinear_set.cpp b/verifying/targets/nonlinear_set.cpp index 039f4ef1..68868c8c 100644 --- a/verifying/targets/nonlinear_set.cpp +++ b/verifying/targets/nonlinear_set.cpp @@ -86,4 +86,4 @@ LTEST_ENTRYPOINT(spec_t); target_method(generateInt, int, SlotsSet, Insert, int); -target_method(generateInt, int, SlotsSet, Erase, int); \ No newline at end of file +target_method(generateInt, int, SlotsSet, Erase, int); diff --git a/verifying/targets/nonlinear_treiber_stack.cpp b/verifying/targets/nonlinear_treiber_stack.cpp index 66ab8c9d..5b57747e 100644 --- a/verifying/targets/nonlinear_treiber_stack.cpp +++ b/verifying/targets/nonlinear_treiber_stack.cpp @@ -85,4 +85,4 @@ LTEST_ENTRYPOINT(spec_t); target_method(generateInt, void, TreiberStack, Push, int); -target_method(ltest::generators::genEmpty, int, TreiberStack, Pop); \ No newline at end of file +target_method(ltest::generators::genEmpty, int, TreiberStack, Pop); From 5af654ac67a7f39a9896b42e3f8000d4de2ccff2 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Wed, 26 Feb 2025 01:33:32 +0000 Subject: [PATCH 22/47] Fix UB with global variables intialization order from the macros expansion --- verifying/targets/nonlinear_ms_queue.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verifying/targets/nonlinear_ms_queue.cpp b/verifying/targets/nonlinear_ms_queue.cpp index 06e360ff..6eb81e21 100644 --- a/verifying/targets/nonlinear_ms_queue.cpp +++ b/verifying/targets/nonlinear_ms_queue.cpp @@ -130,7 +130,7 @@ using spec_t = ltest::Spec, spec::QueueHash<>, spec::QueueEquals<>>; LTEST_ENTRYPOINT(spec_t); - + target_method(generateInt, void, MSQueue, Push, int); target_method(ltest::generators::genEmpty, int, MSQueue, Pop); From 3eeb9a053b58bb8f858f34beeca831b2d19ff178 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Feb 2025 03:41:47 +0000 Subject: [PATCH 23/47] Run clang-format script --- runtime/include/pct_strategy.h | 3 +- runtime/include/scheduler.h | 12 ++++--- runtime/scheduler.cpp | 65 ++++++++++++++++++---------------- 3 files changed, 45 insertions(+), 35 deletions(-) diff --git a/runtime/include/pct_strategy.h b/runtime/include/pct_strategy.h index 1ecd7c87..dd3d9852 100644 --- a/runtime/include/pct_strategy.h +++ b/runtime/include/pct_strategy.h @@ -183,7 +183,8 @@ struct PctStrategy : public BaseStrategyWithThreads { current_schedule_length = 0; // current_depth have been increased - size_t new_k = std::reduce(k_statistics.begin(), k_statistics.end()) / k_statistics.size(); + size_t new_k = std::reduce(k_statistics.begin(), k_statistics.end()) / + k_statistics.size(); log() << "k: " << new_k << "\n"; PrepareForDepth(current_depth, new_k); } diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index b16c6834..b9af3c97 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -4,8 +4,8 @@ #include #include #include +#include -#include "scheduler_fwd.h" #include "lib.h" #include "lincheck.h" #include "logger.h" @@ -16,6 +16,9 @@ #include "stable_vector.h" #include "minimization.h" #include "minimization_smart.h" +#include "pretty_print.h" +#include "scheduler_fwd.h" +#include "stable_vector.h" /// Generated by some strategy task, /// that may be not executed due to constraints of data structure @@ -316,11 +319,11 @@ struct StrategyScheduler : public SchedulerWithReplay { log().flush(); strategy.StartNextRound(); } - + return std::nullopt; } -protected: + protected: // Runs a round with some interleaving while generating it Result RunRound() override { // History of invoke and response events which is required for the checker @@ -385,6 +388,7 @@ struct StrategyScheduler : public SchedulerWithReplay { Response(next_task, result, thread_id)); } } + if (!checker.Check(sequential_history)) { // log() << "New nonlinearized scenario:\n"; // pretty_printer.PrettyPrint(sequential_history, log()); @@ -497,7 +501,7 @@ struct TLAScheduler : Scheduler { Scheduler::Result Run() override { auto [_, res] = RunStep(0, 0); - return res; + return res; } ~TLAScheduler() { TerminateTasks(); } diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp index 6f9622b8..7000bf04 100644 --- a/runtime/scheduler.cpp +++ b/runtime/scheduler.cpp @@ -1,16 +1,16 @@ +#include "include/scheduler.h" + #include -#include "include/scheduler.h" #include "include/logger.h" -#include "include/pretty_print.h" #include "include/minimization.h" #include "include/minimization_smart.h" +#include "include/pretty_print.h" -StrategyScheduler::StrategyScheduler(Strategy &sched_class, - ModelChecker &checker, - PrettyPrinter &pretty_printer, - size_t max_tasks, - size_t max_rounds, +StrategyScheduler::StrategyScheduler(Strategy& sched_class, + ModelChecker& checker, + PrettyPrinter& pretty_printer, + size_t max_tasks, size_t max_rounds, size_t exploration_runs, size_t minimization_runs) : strategy(sched_class), @@ -88,7 +88,8 @@ StrategyScheduler::Result StrategyScheduler::ExploreRound(int runs) { return std::nullopt; } -StrategyScheduler::Result StrategyScheduler::ReplayRound(const std::vector& tasks_ordering) { +StrategyScheduler::Result StrategyScheduler::ReplayRound( + const std::vector& tasks_ordering) { strategy.ResetCurrentRound(); // History of invoke and response events which is required for the checker @@ -97,25 +98,30 @@ StrategyScheduler::Result StrategyScheduler::ReplayRound(const std::vector& // TODO: `IsRunning` field might be added to `Task` instead std::unordered_set started_tasks; std::unordered_set finished_tasks; - std::unordered_map resumes_count; // task id -> number of appearences in `tasks_ordering` + std::unordered_map + resumes_count; // task id -> number of appearences in `tasks_ordering` for (int next_task_id : tasks_ordering) { resumes_count[next_task_id]++; } for (int next_task_id : tasks_ordering) { - bool is_new = started_tasks.contains(next_task_id) ? false : started_tasks.insert(next_task_id).second; + bool is_new = started_tasks.contains(next_task_id) + ? false + : started_tasks.insert(next_task_id).second; auto task_info = strategy.GetTask(next_task_id); if (!task_info.has_value()) { - std::cerr << "No task with id " << next_task_id << " exists in round" << std::endl; + std::cerr << "No task with id " << next_task_id << " exists in round" + << std::endl; throw std::runtime_error("Invalid task id"); } auto [next_task, thread_id] = task_info.value(); if (next_task->IsReturned()) { - // we could witness the task that still has resumes (`resumes_count[next_task_id] > 0`), - // but is already returned, so we just skip it, because its `Response` was already added + // we could witness the task that still has resumes + // (`resumes_count[next_task_id] > 0`), but is already returned, so we + // just skip it, because its `Response` was already added assert(finished_tasks.contains(next_task_id)); continue; } @@ -125,13 +131,12 @@ StrategyScheduler::Result StrategyScheduler::ReplayRound(const std::vector& } full_history.emplace_back(next_task); - - // if this is the last time this task appears in `tasks_ordering`, then complete it fully. + // if this is the last time this task appears in `tasks_ordering`, then + // complete it fully. resumes_count[next_task_id]--; if (resumes_count[next_task_id] == 0) { next_task->Terminate(); - } - else { + } else { next_task->Resume(); } @@ -152,14 +157,10 @@ StrategyScheduler::Result StrategyScheduler::ReplayRound(const std::vector& return std::nullopt; } -Strategy& StrategyScheduler::GetStrategy() const { - return strategy; -} +Strategy& StrategyScheduler::GetStrategy() const { return strategy; } -void StrategyScheduler::Minimize( - Scheduler::BothHistories& nonlinear_history, - const RoundMinimizor& minimizor -) { +void StrategyScheduler::Minimize(Scheduler::BothHistories& nonlinear_history, + const RoundMinimizor& minimizor) { minimizor.Minimize(*this, nonlinear_history); } @@ -173,21 +174,25 @@ Scheduler::Result StrategyScheduler::Run() { log() << "Full nonlinear scenario: \n"; pretty_printer.PrettyPrint(sequential_history, log()); - + log() << "Minimizing same interleaving...\n"; Minimize(histories.value(), SameInterleavingMinimizor()); log() << "Minimized to:\n"; pretty_printer.PrettyPrint(sequential_history, log()); - log() << "Minimizing with rescheduling (exploration runs: " << exploration_runs << ")...\n"; - Minimize(histories.value(), StrategyExplorationMinimizor(exploration_runs)); + 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()); log() << "Minimizing with smart minimizor (exploration runs: " - << exploration_runs << ", minimization runs: " - << minimization_runs << ")...\n"; - Minimize(histories.value(), SmartMinimizor(exploration_runs, minimization_runs, pretty_printer)); + << exploration_runs << ", minimization runs: " << minimization_runs + << ")...\n"; + Minimize( + histories.value(), + SmartMinimizor(exploration_runs, minimization_runs, pretty_printer)); return histories; } From 4cb805e6bf842f800c9df4d87105344b819efb6b Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Feb 2025 03:45:59 +0000 Subject: [PATCH 24/47] Remove build-cmake folder from .gitignore --- .gitignore | 1 - 1 file changed, 1 deletion(-) diff --git a/.gitignore b/.gitignore index 56dd3bfa..5094ec8e 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,5 @@ __pycache__ build -build-cmake venv .vscode .devcontainer/** From f315844d33965f71e025ab8d432717f1439321d9 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Feb 2025 04:50:11 +0000 Subject: [PATCH 25/47] Remove scheduler.cpp file --- runtime/scheduler.cpp | 205 ------------------------------------------ 1 file changed, 205 deletions(-) delete mode 100644 runtime/scheduler.cpp diff --git a/runtime/scheduler.cpp b/runtime/scheduler.cpp deleted file mode 100644 index 7000bf04..00000000 --- a/runtime/scheduler.cpp +++ /dev/null @@ -1,205 +0,0 @@ -#include "include/scheduler.h" - -#include - -#include "include/logger.h" -#include "include/minimization.h" -#include "include/minimization_smart.h" -#include "include/pretty_print.h" - -StrategyScheduler::StrategyScheduler(Strategy& sched_class, - ModelChecker& checker, - PrettyPrinter& pretty_printer, - size_t max_tasks, size_t max_rounds, - size_t exploration_runs, - size_t minimization_runs) - : strategy(sched_class), - checker(checker), - pretty_printer(pretty_printer), - max_tasks(max_tasks), - max_rounds(max_rounds), - exploration_runs(exploration_runs), - minimization_runs(minimization_runs) {} - -Scheduler::Result StrategyScheduler::RunRound() { - // History of invoke and response events which is required for the checker - SeqHistory sequential_history; - // Full history of the current execution in the Run function - FullHistory full_history; - - for (size_t finished_tasks = 0; finished_tasks < max_tasks;) { - auto [next_task, is_new, thread_id] = strategy.Next(); - - // fill the sequential history - if (is_new) { - sequential_history.emplace_back(Invoke(next_task, thread_id)); - } - full_history.emplace_back(next_task); - - next_task->Resume(); - if (next_task->IsReturned()) { - finished_tasks++; - - auto result = next_task->GetRetVal(); - sequential_history.emplace_back(Response(next_task, result, thread_id)); - } - } - - pretty_printer.PrettyPrint(sequential_history, log()); - - if (!checker.Check(sequential_history)) { - return std::make_pair(full_history, sequential_history); - } - - return std::nullopt; -} - -StrategyScheduler::Result StrategyScheduler::ExploreRound(int runs) { - for (int i = 0; i < runs; ++i) { - // log() << "Run " << i + 1 << "/" << runs << "\n"; - strategy.ResetCurrentRound(); - SeqHistory sequential_history; - FullHistory full_history; - - for (int tasks_to_run = strategy.GetValidTasksCount(); tasks_to_run > 0;) { - auto [next_task, is_new, thread_id] = strategy.NextSchedule(); - - if (is_new) { - sequential_history.emplace_back(Invoke(next_task, thread_id)); - } - full_history.emplace_back(next_task); - - next_task->Resume(); - if (next_task->IsReturned()) { - tasks_to_run--; - - auto result = next_task->GetRetVal(); - sequential_history.emplace_back(Response(next_task, result, thread_id)); - } - } - - if (!checker.Check(sequential_history)) { - // log() << "New nonlinearized scenario:\n"; - // pretty_printer.PrettyPrint(sequential_history, log()); - return std::make_pair(full_history, sequential_history); - } - } - - return std::nullopt; -} - -StrategyScheduler::Result StrategyScheduler::ReplayRound( - const std::vector& tasks_ordering) { - strategy.ResetCurrentRound(); - - // History of invoke and response events which is required for the checker - FullHistory full_history; - SeqHistory sequential_history; - // TODO: `IsRunning` field might be added to `Task` instead - std::unordered_set started_tasks; - std::unordered_set finished_tasks; - std::unordered_map - resumes_count; // task id -> number of appearences in `tasks_ordering` - - for (int next_task_id : tasks_ordering) { - resumes_count[next_task_id]++; - } - - for (int next_task_id : tasks_ordering) { - bool is_new = started_tasks.contains(next_task_id) - ? false - : started_tasks.insert(next_task_id).second; - auto task_info = strategy.GetTask(next_task_id); - - if (!task_info.has_value()) { - std::cerr << "No task with id " << next_task_id << " exists in round" - << std::endl; - throw std::runtime_error("Invalid task id"); - } - - auto [next_task, thread_id] = task_info.value(); - if (next_task->IsReturned()) { - // we could witness the task that still has resumes - // (`resumes_count[next_task_id] > 0`), but is already returned, so we - // just skip it, because its `Response` was already added - assert(finished_tasks.contains(next_task_id)); - continue; - } - - if (is_new) { - sequential_history.emplace_back(Invoke(next_task, thread_id)); - } - full_history.emplace_back(next_task); - - // if this is the last time this task appears in `tasks_ordering`, then - // complete it fully. - resumes_count[next_task_id]--; - if (resumes_count[next_task_id] == 0) { - next_task->Terminate(); - } else { - next_task->Resume(); - } - - if (next_task->IsReturned()) { - auto result = next_task->GetRetVal(); - sequential_history.emplace_back(Response(next_task, result, thread_id)); - finished_tasks.insert(next_task_id); - } - } - - // pretty_printer.PrettyPrint(sequential_history, log()); - assert(started_tasks.size() == finished_tasks.size()); - - if (!checker.Check(sequential_history)) { - return std::make_pair(full_history, sequential_history); - } - - return std::nullopt; -} - -Strategy& StrategyScheduler::GetStrategy() const { return strategy; } - -void StrategyScheduler::Minimize(Scheduler::BothHistories& nonlinear_history, - const RoundMinimizor& minimizor) { - minimizor.Minimize(*this, nonlinear_history); -} - -Scheduler::Result StrategyScheduler::Run() { - for (size_t i = 0; i < max_rounds; ++i) { - log() << "run round: " << i << "\n"; - auto histories = RunRound(); - - if (histories.has_value()) { - auto& [full_history, sequential_history] = histories.value(); - - log() << "Full nonlinear scenario: \n"; - pretty_printer.PrettyPrint(sequential_history, log()); - - log() << "Minimizing same interleaving...\n"; - Minimize(histories.value(), SameInterleavingMinimizor()); - log() << "Minimized to:\n"; - pretty_printer.PrettyPrint(sequential_history, 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()); - - log() << "Minimizing with smart minimizor (exploration runs: " - << exploration_runs << ", minimization runs: " << minimization_runs - << ")...\n"; - Minimize( - histories.value(), - SmartMinimizor(exploration_runs, minimization_runs, pretty_printer)); - - return histories; - } - log() << "===============================================\n\n"; - log().flush(); - strategy.StartNextRound(); - } - - return std::nullopt; -} \ No newline at end of file From cb8afaf94c47b5a8070e6801216ccbbf9af15174 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Feb 2025 04:51:17 +0000 Subject: [PATCH 26/47] Run new nonlinear data structures on CI with minimization --- .github/workflows/run-tests.yaml | 44 +++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/.github/workflows/run-tests.yaml b/.github/workflows/run-tests.yaml index a809b7af..4781332f 100644 --- a/.github/workflows/run-tests.yaml +++ b/.github/workflows/run-tests.yaml @@ -72,7 +72,49 @@ jobs: # fi - name: Run nonlinear_queue with random strategy run: | - ./build/verifying/targets/nonlinear_queue --tasks 4 --rounds 100000 --strategy random --switches 1 || error_code=$? + ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy random --minimization 1 || error_code=$? + if [ "${error_code}" -ne 1 ]; then + exit 1 + fi + - name: Run nonlinear_ms_queue with random strategy (minimization) + run: | + ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy random --minimization 1 || error_code=$? + if [ "${error_code}" -ne 1 ]; then + exit 1 + fi + - name: Run nonlinear_treiber_stack with random strategy (minimization) + run: | + ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy random --minimization 1 || error_code=$? + if [ "${error_code}" -ne 1 ]; then + exit 1 + fi + - name: Run nonlinear_set with random strategy (minimization) + run: | + ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy random --minimization 1 || error_code=$? + if [ "${error_code}" -ne 1 ]; then + exit 1 + fi + - name: Run nonlinear_queue with pct strategy (minimization) + run: | + ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimization 1 || error_code=$? + if [ "${error_code}" -ne 1 ]; then + exit 1 + fi + - name: Run nonlinear_ms_queue with pct strategy (minimization) + run: | + ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy pct --minimization 1 || error_code=$? + if [ "${error_code}" -ne 1 ]; then + exit 1 + fi + - name: Run nonlinear_treiber_stack with pct strategy (minimization) + run: | + ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy pct --minimization 1 || error_code=$? + if [ "${error_code}" -ne 1 ]; then + exit 1 + fi + - name: Run nonlinear_set with pct strategy (minimization) + run: | + ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy pct --minimization 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi From a6ce6dacf9cf7a33fb8564306ac82e9ed8ac8ea6 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Feb 2025 04:54:54 +0000 Subject: [PATCH 27/47] Fix CI --- .github/workflows/run-tests.yaml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/run-tests.yaml b/.github/workflows/run-tests.yaml index 4781332f..f2495991 100644 --- a/.github/workflows/run-tests.yaml +++ b/.github/workflows/run-tests.yaml @@ -78,43 +78,43 @@ jobs: fi - name: Run nonlinear_ms_queue with random strategy (minimization) run: | - ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy random --minimization 1 || error_code=$? + ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy random --minimize 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_treiber_stack with random strategy (minimization) run: | - ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy random --minimization 1 || error_code=$? + ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy random --minimize 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_set with random strategy (minimization) run: | - ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy random --minimization 1 || error_code=$? + ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy random --minimize 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_queue with pct strategy (minimization) run: | - ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimization 1 || error_code=$? + ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimize 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_ms_queue with pct strategy (minimization) run: | - ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy pct --minimization 1 || error_code=$? + ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy pct --minimize 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_treiber_stack with pct strategy (minimization) run: | - ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy pct --minimization 1 || error_code=$? + ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy pct --minimize 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_set with pct strategy (minimization) run: | - ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy pct --minimization 1 || error_code=$? + ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy pct --minimize 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi From 5ffaeff36091cce6aff9862a1cf5c7c0e2b92296 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Feb 2025 05:20:32 +0000 Subject: [PATCH 28/47] Update CI --- .github/workflows/run-tests.yaml | 49 ++++++++++++++++++++++++++------ 1 file changed, 41 insertions(+), 8 deletions(-) diff --git a/.github/workflows/run-tests.yaml b/.github/workflows/run-tests.yaml index f2495991..d3d59dd8 100644 --- a/.github/workflows/run-tests.yaml +++ b/.github/workflows/run-tests.yaml @@ -76,27 +76,48 @@ jobs: if [ "${error_code}" -ne 1 ]; then exit 1 fi - - name: Run nonlinear_ms_queue with random strategy (minimization) + - name: Run nonlinear_queue with pct strategy (minimization) run: | - ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy random --minimize 1 || error_code=$? + ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimize 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - - name: Run nonlinear_treiber_stack with random strategy (minimization) + verifying-test (Release): + runs-on: ubuntu-latest + defaults: + run: + shell: bash + container: + image: silkeh/clang:18 + options: --user root + steps: + - name: Install deps run: | - ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy random --minimize 1 || error_code=$? + apt update && apt install -y git ninja-build valgrind libgoogle-glog-dev libsnappy-dev protobuf-compiler libboost-context-dev pkg-config libcapstone-dev && \ + git clone https://github.com/Kirillog/syscall_intercept.git && \ + cmake syscall_intercept -G Ninja -B syscall_intercept/build -DCMAKE_INSTALL_PREFIX=/usr -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=clang && \ + cmake --build syscall_intercept/build --target install + - name: Check out repository code + uses: actions/checkout@v4 + - name: Build + run: | + cmake -G Ninja -B build -DCMAKE_BUILD_TYPE=Release + cmake --build build --target verifying/targets/nonlinear_queue verifying/targets/nonlinear_ms_queue verifying/targets/nonlinear_treiber_stack verifying/targets/nonlinear_set verifying/blocking/nonlinear_mutex verifying/blocking/simple_mutex + - name: Run nonlinear_queue with random strategy (minimization) + run: | + ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy random --minimize 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - - name: Run nonlinear_set with random strategy (minimization) + - name: Run nonlinear_queue with pct strategy (minimization) run: | - ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy random --minimize 1 || error_code=$? + ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimize 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - - name: Run nonlinear_queue with pct strategy (minimization) + - name: Run nonlinear_ms_queue with random strategy (minimization) run: | - ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimize 1 || error_code=$? + ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy random --minimize 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi @@ -106,12 +127,24 @@ jobs: if [ "${error_code}" -ne 1 ]; then exit 1 fi + - name: Run nonlinear_treiber_stack with random strategy (minimization) + run: | + ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy random --minimize 1 || error_code=$? + if [ "${error_code}" -ne 1 ]; then + exit 1 + fi - name: Run nonlinear_treiber_stack with pct strategy (minimization) run: | ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy pct --minimize 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi + - name: Run nonlinear_set with random strategy (minimization) + run: | + ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy random --minimize 1 || error_code=$? + if [ "${error_code}" -ne 1 ]; then + exit 1 + fi - name: Run nonlinear_set with pct strategy (minimization) run: | ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy pct --minimize 1 || error_code=$? From cb696e6acd4aeea22fcd9642156bc93fc7f5eb6c Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Feb 2025 05:22:40 +0000 Subject: [PATCH 29/47] Update CI --- .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 d3d59dd8..eaff1013 100644 --- a/.github/workflows/run-tests.yaml +++ b/.github/workflows/run-tests.yaml @@ -82,7 +82,7 @@ jobs: if [ "${error_code}" -ne 1 ]; then exit 1 fi - verifying-test (Release): + verifying-test-release: runs-on: ubuntu-latest defaults: run: From 847581fb2bde7eb62329b31ded3841efb0b696e5 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Feb 2025 07:30:20 +0000 Subject: [PATCH 30/47] Fix hanging bugs with simple mutex --- runtime/include/scheduler.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index b9af3c97..38cafcf0 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -190,6 +190,8 @@ struct BaseStrategyWithThreads : public Strategy { // Actually, we assume obstruction free here. // TODO: for locks we need to figure out how to properly terminate: see https://github.com/ITMO-PTDC-Team/LTest/issues/13 void TerminateTasks() { + state.Reset(); + auto& round_schedule = this->round_schedule; assert(round_schedule.size() == this->threads.size() && "sizes expected to be the same"); From 62e610de68520a7d33071b81db8548d38afe7ee7 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Feb 2025 09:21:29 +0000 Subject: [PATCH 31/47] Bug fixes --- runtime/include/scheduler.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index 38cafcf0..b9af3c97 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -190,8 +190,6 @@ struct BaseStrategyWithThreads : public Strategy { // Actually, we assume obstruction free here. // TODO: for locks we need to figure out how to properly terminate: see https://github.com/ITMO-PTDC-Team/LTest/issues/13 void TerminateTasks() { - state.Reset(); - auto& round_schedule = this->round_schedule; assert(round_schedule.size() == this->threads.size() && "sizes expected to be the same"); From 6e373a1c627e05141781c06f7eb7e2fe1d081ea5 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Feb 2025 10:25:41 +0000 Subject: [PATCH 32/47] Modify TerminateTasks, so it does not finish blocked tasks --- runtime/include/scheduler.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index b9af3c97..f03d8894 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -190,6 +190,9 @@ struct BaseStrategyWithThreads : public Strategy { // Actually, we assume obstruction free here. // TODO: for locks we need to figure out how to properly terminate: see https://github.com/ITMO-PTDC-Team/LTest/issues/13 void TerminateTasks() { + // state.Reset(); + + auto& round_schedule = this->round_schedule; assert(round_schedule.size() == this->threads.size() && "sizes expected to be the same"); @@ -228,7 +231,6 @@ struct BaseStrategyWithThreads : public Strategy { } } } - this->sched_checker.Reset(); state.Reset(); } From 935f95ff6096468270e78f8a03c940ea54be592b Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Wed, 26 Mar 2025 23:32:51 +0000 Subject: [PATCH 33/47] Fix tasks termination order (first terminate tasks, then reset the state of the data structure under test) --- runtime/include/scheduler.h | 3 --- 1 file changed, 3 deletions(-) diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index f03d8894..a9fcb7f0 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -190,9 +190,6 @@ struct BaseStrategyWithThreads : public Strategy { // Actually, we assume obstruction free here. // TODO: for locks we need to figure out how to properly terminate: see https://github.com/ITMO-PTDC-Team/LTest/issues/13 void TerminateTasks() { - // state.Reset(); - - auto& round_schedule = this->round_schedule; assert(round_schedule.size() == this->threads.size() && "sizes expected to be the same"); From eca5b6f88bbd4b5fee503167917c05384d04e49b Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Wed, 26 Mar 2025 23:42:25 +0000 Subject: [PATCH 34/47] Add some minor fixes --- .github/workflows/run-tests.yaml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/.github/workflows/run-tests.yaml b/.github/workflows/run-tests.yaml index eaff1013..4da451a9 100644 --- a/.github/workflows/run-tests.yaml +++ b/.github/workflows/run-tests.yaml @@ -78,7 +78,7 @@ jobs: fi - name: Run nonlinear_queue with pct strategy (minimization) run: | - ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimize 1 || error_code=$? + ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimize || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi @@ -105,49 +105,49 @@ jobs: cmake --build build --target verifying/targets/nonlinear_queue verifying/targets/nonlinear_ms_queue verifying/targets/nonlinear_treiber_stack verifying/targets/nonlinear_set verifying/blocking/nonlinear_mutex verifying/blocking/simple_mutex - name: Run nonlinear_queue with random strategy (minimization) run: | - ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy random --minimize 1 || error_code=$? + ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy random --minimize || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_queue with pct strategy (minimization) run: | - ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimize 1 || error_code=$? + ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimize || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_ms_queue with random strategy (minimization) run: | - ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy random --minimize 1 || error_code=$? + ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy random --minimize || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_ms_queue with pct strategy (minimization) run: | - ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy pct --minimize 1 || error_code=$? + ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy pct --minimize || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_treiber_stack with random strategy (minimization) run: | - ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy random --minimize 1 || error_code=$? + ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy random --minimize || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_treiber_stack with pct strategy (minimization) run: | - ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy pct --minimize 1 || error_code=$? + ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy pct --minimize || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_set with random strategy (minimization) run: | - ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy random --minimize 1 || error_code=$? + ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy random --minimize || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi - name: Run nonlinear_set with pct strategy (minimization) run: | - ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy pct --minimize 1 || error_code=$? + ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy pct --minimize || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi From ef59d680c49a9ba9da6d75ce3a29f9c0ebdd001b Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Mar 2025 00:33:01 +0000 Subject: [PATCH 35/47] Change how schedulers terminate their tasks --- runtime/include/scheduler.h | 1 + 1 file changed, 1 insertion(+) diff --git a/runtime/include/scheduler.h b/runtime/include/scheduler.h index a9fcb7f0..b9af3c97 100644 --- a/runtime/include/scheduler.h +++ b/runtime/include/scheduler.h @@ -228,6 +228,7 @@ struct BaseStrategyWithThreads : public Strategy { } } } + this->sched_checker.Reset(); state.Reset(); } From c103a8d2fdc5827a8157e87121e07571df9b2368 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Wed, 19 Mar 2025 21:09:06 +0000 Subject: [PATCH 36/47] Add clangpass sources --- CMakeLists.txt | 1 + clangpass/CMakeLists.txt | 68 +++++++++++ clangpass/clangpass.cpp | 216 ++++++++++++++++++++++++++++++++++ clangpass/clangpass_tool.cpp | 91 ++++++++++++++ clangpass/include/clangpass.h | 59 ++++++++++ 5 files changed, 435 insertions(+) create mode 100644 clangpass/CMakeLists.txt create mode 100644 clangpass/clangpass.cpp create mode 100644 clangpass/clangpass_tool.cpp create mode 100644 clangpass/include/clangpass.h diff --git a/CMakeLists.txt b/CMakeLists.txt index 1a0d66cd..7a0607b7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -24,6 +24,7 @@ include(GoogleTest) fuzztest_setup_fuzzing_flags() enable_testing() +add_subdirectory(clangpass) add_subdirectory(codegen) add_subdirectory(runtime) diff --git a/clangpass/CMakeLists.txt b/clangpass/CMakeLists.txt new file mode 100644 index 00000000..06b5b247 --- /dev/null +++ b/clangpass/CMakeLists.txt @@ -0,0 +1,68 @@ +#=============================================================================== +# SETUP CLANG PLUGIN +#=============================================================================== + +# Set this to a valid LLVM installation dir +set(CT_Clang_INSTALL_DIR "/usr/lib/llvm-19" CACHE PATH "Clang installation directory") + +message("Clang install path: ${CT_Clang_INSTALL_DIR}") + +# Add the location of ClangConfig.cmake to CMake search paths (so that +# find_package can locate it) +list(APPEND CMAKE_PREFIX_PATH "${CT_Clang_INSTALL_DIR}/lib/cmake/clang/") + +find_package(Clang REQUIRED CONFIG) +if("${LLVM_VERSION_MAJOR}" VERSION_LESS 19) + message(FATAL_ERROR "Found LLVM ${LLVM_VERSION_MAJOR}, but need LLVM 19 or above") +endif() + +include_directories(SYSTEM "${LLVM_INCLUDE_DIRS};${CLANG_INCLUDE_DIRS}") + +if(NOT LLVM_ENABLE_RTTI) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fno-rtti") +endif() + +# -fvisibility-inlines-hidden is set when building LLVM and on Darwin warnings +# are triggered if llvm-tutor is built without this flag (though otherwise it +# builds fine). For consistency, add it here too. +include(CheckCXXCompilerFlag) +check_cxx_compiler_flag("-fvisibility-inlines-hidden" + SUPPORTS_FVISIBILITY_INLINES_HIDDEN_FLAG) +if(${SUPPORTS_FVISIBILITY_INLINES_HIDDEN_FLAG} EQUAL "1") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fvisibility-inlines-hidden") +endif() + +add_library(ClangPass SHARED clangpass.cpp) + +# Allow undefined symbols in shared objects on Darwin (this is the default +# behaviour on Linux) +target_link_libraries(ClangPass + "$<$:-undefined dynamic_lookup>") + + +#=============================================================================== +# SETUP CLANG TOOL +#=============================================================================== +set(CLANG_TOOL "ClangPassTool") +set(CLANG_TOOL_SOURCES + "${CMAKE_CURRENT_SOURCE_DIR}/clangpass_tool.cpp" + "${CMAKE_CURRENT_SOURCE_DIR}/clangpass.cpp" +) + +add_executable( + ${CLANG_TOOL} + ${CLANG_TOOL_SOURCES} +) + +# Configure include directories for 'tool' +target_include_directories( + ${CLANG_TOOL} + PRIVATE + "${CMAKE_CURRENT_SOURCE_DIR}/include" +) + +# Link in the required libraries +target_link_libraries( + ${CLANG_TOOL} + clangTooling +) \ No newline at end of file diff --git a/clangpass/clangpass.cpp b/clangpass/clangpass.cpp new file mode 100644 index 00000000..fdbc660c --- /dev/null +++ b/clangpass/clangpass.cpp @@ -0,0 +1,216 @@ +//============================================================================== +// FILE: +// clangpass.cpp +// +// DESCRIPTION: +// Substitutes all input files std::atomic usages with MyAtomic with +// the same API. +// +// USAGE: +// clang++ -Xclang -load -Xclang ./build/lib/libClangPass.so -Xclang -add-plugin -Xclang ClangPass ./AtomicsReplacer/test-project/main.cpp +// +// License: The Unlicense +//============================================================================== + +#include "clang/AST/ASTConsumer.h" +#include "clang/ASTMatchers/ASTMatchFinder.h" +#include "clang/Rewrite/Core/Rewriter.h" +#include "clang/Rewrite/Frontend/FixItRewriter.h" +#include "clang/Tooling/CommonOptionsParser.h" +#include "clang/AST/Expr.h" +#include "clang/AST/ExprCXX.h" +#include "clang/AST/RecursiveASTVisitor.h" +#include "clang/ASTMatchers/ASTMatchers.h" +#include "clang/Frontend/CompilerInstance.h" +#include "clang/Frontend/FrontendPluginRegistry.h" +#include "clang/Tooling/Refactoring/Rename/RenamingAction.h" +#include "llvm/ADT/StringMap.h" +#include "llvm/Support/raw_ostream.h" +#include "llvm/Support/raw_ostream.h" + +#include "clangpass.h" + +using namespace clang; +using namespace ast_matchers; +using namespace llvm; + +//----------------------------------------------------------------------------- +// ASTFinder callback +//----------------------------------------------------------------------------- +CodeRefactorMatcher::CodeRefactorMatcher( + ASTContext& Context, + clang::Rewriter &RewriterForCodeRefactor, + std::string ClassNameToReplace, + std::string ClassNameToInsert +) : Context(Context), + CodeRefactorRewriter(RewriterForCodeRefactor), + ClassNameToReplace(ClassNameToReplace), + ClassNameToInsert(ClassNameToInsert) {} + +void CodeRefactorMatcher::onEndOfTranslationUnit() { + const SourceManager& SM = CodeRefactorRewriter.getSourceMgr(); + FileID MainFileID = SM.getMainFileID(); + const RewriteBuffer& Buffer = CodeRefactorRewriter.getEditBuffer(MainFileID); + + // Output to stdout + llvm::outs() << "Transformed code:\n"; + Buffer.write(llvm::outs()); + llvm::outs() << "\n"; + + // Output to file + const FileEntry *Entry = SM.getFileEntryForID(MainFileID); + StringRef OriginalFilename = Entry->tryGetRealPathName(); + + size_t slashIndex = OriginalFilename.rfind("/"); + // the path should be absolute, so in the worst case we will get '/' as index 0 + assert(slashIndex != std::string::npos); + slashIndex += 1; // include the '/' itself + + std::string Path = std::string(OriginalFilename.begin(), OriginalFilename.begin() + slashIndex); + std::string SourceFilename = std::string(OriginalFilename.begin() + slashIndex, OriginalFilename.end()); + + llvm::outs() << "Original filename: " << OriginalFilename << "\n"; + std::string OutputFilename = Path + "__tmp_" + SourceFilename; + + std::error_code EC; + llvm::raw_fd_ostream OS(OutputFilename, EC, llvm::sys::fs::OF_None); + + if (EC) { + llvm::errs() << "Error: Could not open output file: " << EC.message() << "\n"; + return; + } + + llvm::outs() << "Writing to file: " << OutputFilename << "\n"; + //OS << std::string(Buffer->begin(), Buffer->end()); + Buffer.write(OS); + OS.close(); +} + +void CodeRefactorMatcher::run(const clang::ast_matchers::MatchFinder::MatchResult &Result) { + if (const auto* ETL = Result.Nodes.getNodeAs("ElaboratedTypeLoc")) { + const auto* TemplType = ETL->getType()->getAs(); + if (!TemplType) { + return; + } + + CodeRefactorRewriter.ReplaceText(ETL->getSourceRange(), ClassNameToInsert + GetArgumentsFromTemplateType(TemplType)); + } + + if (const auto* QTL = Result.Nodes.getNodeAs("QualifiedTypeLoc")) { + const auto* TemplType = QTL->getType()->getAs(); + if (!TemplType) { + return; + } + + CodeRefactorRewriter.ReplaceText(QTL->getSourceRange(), ClassNameToInsert + GetArgumentsFromTemplateType(TemplType)); + } +} + +std::string CodeRefactorMatcher::GetArgumentsFromTemplateType(const TemplateSpecializationType *TST) { + std::string args; + llvm::raw_string_ostream os(args); + printTemplateArgumentList(os, TST->template_arguments(), Context.getPrintingPolicy()); + return args; +} + +// Util function for debugging purposes +std::string CodeRefactorMatcher::getSourceRangeAsString(const SourceRange& SR) const { + auto& sm = CodeRefactorRewriter.getSourceMgr(); + auto& langOpts = CodeRefactorRewriter.getLangOpts(); + + clang::SourceLocation start = SR.getBegin(); + clang::SourceLocation end = SR.getEnd(); + end = clang::Lexer::getLocForEndOfToken(end, 0, sm, langOpts); + + bool isInvalid = false; + const char *startData = sm.getCharacterData(start, &isInvalid); + + if (isInvalid) { + return ""; + isInvalid = false; + } + + const char *endData = sm.getCharacterData(end, &isInvalid); + + if (isInvalid) { + return ""; + isInvalid = false; + } + size_t length = endData - startData; + + return std::string(startData, length); +} + + +//----------------------------------------------------------------------------- +// ASTConsumer +//----------------------------------------------------------------------------- +CodeRefactorASTConsumer::CodeRefactorASTConsumer( + ASTContext& Context, + clang::Rewriter &R, + std::string ClassNameToReplace, + std::string ClassNameToInsert +): CodeRefactorHandler(Context, R, ClassNameToReplace, ClassNameToInsert), + ClassNameToReplace(ClassNameToReplace), + ClassNameToInsert(ClassNameToInsert) { + // Does not support matching the parameters of the functions + const auto MatcherForFQTemplateTypes = elaboratedTypeLoc( + hasNamedTypeLoc( + loc( + templateSpecializationType( + hasDeclaration( + classTemplateSpecializationDecl( + hasName(ClassNameToReplace) + ) + ) + ) + ) + ) + ); + + // Uses previous matcher inside, but returns a wrapping QualifiedTypeLoc node + // which is used in the function parameters + const auto MatcherForFQTemplateParams = qualifiedTypeLoc( + hasUnqualifiedLoc( + MatcherForFQTemplateTypes + ) + ); + + Finder.addMatcher(MatcherForFQTemplateTypes.bind("ElaboratedTypeLoc"), &CodeRefactorHandler); + Finder.addMatcher(MatcherForFQTemplateParams.bind("QualifiedTypeLoc"), &CodeRefactorHandler); +} + +void CodeRefactorASTConsumer::HandleTranslationUnit(clang::ASTContext &Ctx) { + Finder.matchAST(Ctx); +} + + +//----------------------------------------------------------------------------- +// FrontendAction +//----------------------------------------------------------------------------- +class CodeRefactorAddPluginAction : public PluginASTAction { +public: + bool ParseArgs(const CompilerInstance &CI, const std::vector &Args) override { + return true; + } + + // Returns our ASTConsumer per translation unit. + std::unique_ptr CreateASTConsumer(CompilerInstance &CI, + StringRef file) override { + RewriterForCodeRefactor.setSourceMgr(CI.getSourceManager(), + CI.getLangOpts()); + return std::make_unique( + CI.getASTContext(), RewriterForCodeRefactor, ClassNameToReplace, ClassNameToInsert); + } + +private: + Rewriter RewriterForCodeRefactor; + std::string ClassNameToReplace = "::std::atomic"; + std::string ClassNameToInsert = "MyAtomic"; +}; + + +static FrontendPluginRegistry::Add X( + "ClangPass", + "Replace all std::atomic usages with MyAtomic" +); \ No newline at end of file diff --git a/clangpass/clangpass_tool.cpp b/clangpass/clangpass_tool.cpp new file mode 100644 index 00000000..86eddd7c --- /dev/null +++ b/clangpass/clangpass_tool.cpp @@ -0,0 +1,91 @@ +//============================================================================== +// FILE: +// clangpass_tool.cpp +// +// DESCRIPTION: +// A standalone tool that runs the clangpass plugin. See +// clangpass.cpp for a complete description. +// +// USAGE: +// * ./build/bin/clangpass_tool --replace-name=::std::atomic '\' +// --insert-name=MyAtomic ./AtomicsReplacer/test-project/main.cpp +// +// +// License: The Unlicense +//============================================================================== +#include "clangpass.h" + +#include "clang/Frontend/CompilerInstance.h" +#include "clang/Frontend/FrontendPluginRegistry.h" +#include "clang/Tooling/CommonOptionsParser.h" +#include "clang/Tooling/Refactoring.h" +#include "llvm/Support/CommandLine.h" + +using namespace llvm; +using namespace clang; + +//===----------------------------------------------------------------------===// +// Command line options +//===----------------------------------------------------------------------===// +static cl::OptionCategory CodeRefactorCategory("atomics-replacer options"); + +static cl::opt ClassNameToReplaceOpt{ + "replace-name", + cl::desc("The name of the class/struct which usages should be renamed"), + cl::Required, cl::init(""), cl::cat(CodeRefactorCategory)}; +static cl::opt ClassNameToInsertOpt{ + "insert-name", cl::desc("The name of the class/struct which should be used instead"), + cl::Required, cl::init(""), cl::cat(CodeRefactorCategory)}; + +//===----------------------------------------------------------------------===// +// PluginASTAction +//===----------------------------------------------------------------------===// +class CodeRefactorPluginAction : public PluginASTAction { +public: + explicit CodeRefactorPluginAction() {}; + // Not used + bool ParseArgs( + const CompilerInstance &CI, + const std::vector &args + ) override { + return true; + } + + std::unique_ptr CreateASTConsumer( + CompilerInstance &CI, + StringRef file + ) override { + RewriterForCodeRefactor.setSourceMgr( + CI.getSourceManager(), + CI.getLangOpts() + ); + return std::make_unique( + CI.getASTContext(), RewriterForCodeRefactor, ClassNameToReplaceOpt, ClassNameToInsertOpt); + } + +private: + Rewriter RewriterForCodeRefactor; +}; + +//===----------------------------------------------------------------------===// +// Main driver code. +//===----------------------------------------------------------------------===// +int main(int Argc, const char **Argv) { + Expected eOptParser = + clang::tooling::CommonOptionsParser::create( + Argc, + Argv, + CodeRefactorCategory + ); + if (auto E = eOptParser.takeError()) { + errs() << "Problem constructing CommonOptionsParser " + << toString(std::move(E)) << '\n'; + return EXIT_FAILURE; + } + clang::tooling::RefactoringTool Tool( + eOptParser->getCompilations(), + eOptParser->getSourcePathList() + ); + + return Tool.run(clang::tooling::newFrontendActionFactory().get()); +} diff --git a/clangpass/include/clangpass.h b/clangpass/include/clangpass.h new file mode 100644 index 00000000..fcf4aedc --- /dev/null +++ b/clangpass/include/clangpass.h @@ -0,0 +1,59 @@ +#pragma once + +#include "clang/AST/ASTConsumer.h" +#include "clang/ASTMatchers/ASTMatchFinder.h" +#include "clang/Rewrite/Core/Rewriter.h" +#include "clang/Tooling/CommonOptionsParser.h" +#include "clang/ASTMatchers/ASTMatchers.h" + +using namespace clang; +using namespace ast_matchers; +using namespace llvm; + + +//----------------------------------------------------------------------------- +// ASTFinder callback +//----------------------------------------------------------------------------- +class CodeRefactorMatcher : public clang::ast_matchers::MatchFinder::MatchCallback { +public: + explicit CodeRefactorMatcher( + ASTContext& Context, + clang::Rewriter &RewriterForCodeRefactor, + std::string ClassNameToReplace, + std::string ClassNameToInsert + ); + + void onEndOfTranslationUnit() override; + void run(const clang::ast_matchers::MatchFinder::MatchResult &Result) override; + std::string GetArgumentsFromTemplateType(const TemplateSpecializationType *TST); + +private: + ASTContext& Context; + clang::Rewriter CodeRefactorRewriter; + std::string ClassNameToReplace; + std::string ClassNameToInsert; + + std::string getSourceRangeAsString(const SourceRange& SR) const; +}; + +//----------------------------------------------------------------------------- +// ASTConsumer +//----------------------------------------------------------------------------- +class CodeRefactorASTConsumer : public clang::ASTConsumer { +public: + CodeRefactorASTConsumer( + ASTContext& Context, + clang::Rewriter &R, + std::string ClassNameToReplace, + std::string ClassNameToInsert + ); + + void HandleTranslationUnit(clang::ASTContext &Ctx) override; + +private: + clang::ast_matchers::MatchFinder Finder; + CodeRefactorMatcher CodeRefactorHandler; + + std::string ClassNameToReplace; + std::string ClassNameToInsert; +}; \ No newline at end of file From 2879d78e2714fe1553634f4abd1563247d91accf Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Wed, 19 Mar 2025 23:25:30 +0000 Subject: [PATCH 37/47] Setup clangpass in cmake --- clangpass/CMakeLists.txt | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/clangpass/CMakeLists.txt b/clangpass/CMakeLists.txt index 06b5b247..060e6c21 100644 --- a/clangpass/CMakeLists.txt +++ b/clangpass/CMakeLists.txt @@ -34,6 +34,12 @@ endif() add_library(ClangPass SHARED clangpass.cpp) +target_include_directories( + ClangPass + PRIVATE + "${CMAKE_CURRENT_SOURCE_DIR}/include" +) + # Allow undefined symbols in shared objects on Darwin (this is the default # behaviour on Linux) target_link_libraries(ClangPass From cc7987f18e7fa920beefacee1d083f45afe5c667 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Wed, 19 Mar 2025 23:25:30 +0000 Subject: [PATCH 38/47] Setup clangpass in cmake --- CMakeLists.txt | 5 +++++ clangpass/CMakeLists.txt | 10 --------- clangpass/clangpass.cpp | 8 ++++--- clangpass/clangpass_tool.cpp | 4 ++-- runtime/include/ltest_atomic.h | 38 ++++++++++++++++++++++++++++++++++ runtime/include/verifying.h | 4 ++++ verifying/CMakeLists.txt | 38 +++++++++++++++++++++++++++++++--- 7 files changed, 89 insertions(+), 18 deletions(-) create mode 100644 runtime/include/ltest_atomic.h diff --git a/CMakeLists.txt b/CMakeLists.txt index 7a0607b7..e16ac4b1 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -5,8 +5,13 @@ project(lintest) set(CMAKE_CXX_STANDARD 20) +# in order for clang tool to work, this must be ON (it will generate the compilation database) +# see https://clang.llvm.org/docs/JSONCompilationDatabase.html set(CMAKE_EXPORT_COMPILE_COMMANDS ON) +# set this to ON in order to substitute std::atomic with custom implementation +set(APPLY_CLANG_TOOL OFF) + # TODO(kmitkin): require to understand, what is it considered to be "optimized" build # set(CMAKE_CXX_FLAGS_RELEASE "???") set(CMAKE_CXX_FLAGS_DEBUG "-g -ggdb3 -O0 -fno-omit-frame-pointer") diff --git a/clangpass/CMakeLists.txt b/clangpass/CMakeLists.txt index 060e6c21..735e6368 100644 --- a/clangpass/CMakeLists.txt +++ b/clangpass/CMakeLists.txt @@ -1,16 +1,6 @@ #=============================================================================== # SETUP CLANG PLUGIN #=============================================================================== - -# Set this to a valid LLVM installation dir -set(CT_Clang_INSTALL_DIR "/usr/lib/llvm-19" CACHE PATH "Clang installation directory") - -message("Clang install path: ${CT_Clang_INSTALL_DIR}") - -# Add the location of ClangConfig.cmake to CMake search paths (so that -# find_package can locate it) -list(APPEND CMAKE_PREFIX_PATH "${CT_Clang_INSTALL_DIR}/lib/cmake/clang/") - find_package(Clang REQUIRED CONFIG) if("${LLVM_VERSION_MAJOR}" VERSION_LESS 19) message(FATAL_ERROR "Found LLVM ${LLVM_VERSION_MAJOR}, but need LLVM 19 or above") diff --git a/clangpass/clangpass.cpp b/clangpass/clangpass.cpp index fdbc660c..8b03e5ef 100644 --- a/clangpass/clangpass.cpp +++ b/clangpass/clangpass.cpp @@ -3,7 +3,7 @@ // clangpass.cpp // // DESCRIPTION: -// Substitutes all input files std::atomic usages with MyAtomic with +// Substitutes all input files std::atomic usages with LTestAtomic with // the same API. // // USAGE: @@ -205,12 +205,14 @@ class CodeRefactorAddPluginAction : public PluginASTAction { private: Rewriter RewriterForCodeRefactor; + // The shared library has predefined replace- and insert-class names, + // users are intended to use clangpass_tool.cpp instead. std::string ClassNameToReplace = "::std::atomic"; - std::string ClassNameToInsert = "MyAtomic"; + std::string ClassNameToInsert = "LTestAtomic"; }; static FrontendPluginRegistry::Add X( "ClangPass", - "Replace all std::atomic usages with MyAtomic" + "Replace all std::atomic usages with LTestAtomic" ); \ No newline at end of file diff --git a/clangpass/clangpass_tool.cpp b/clangpass/clangpass_tool.cpp index 86eddd7c..a60d0537 100644 --- a/clangpass/clangpass_tool.cpp +++ b/clangpass/clangpass_tool.cpp @@ -7,8 +7,7 @@ // clangpass.cpp for a complete description. // // USAGE: -// * ./build/bin/clangpass_tool --replace-name=::std::atomic '\' -// --insert-name=MyAtomic ./AtomicsReplacer/test-project/main.cpp +// * ./build/bin/clangpass_tool --replace-name=::std::atomic --insert-name=LTestAtomic ./AtomicsReplacer/test-project/main.cpp // // // License: The Unlicense @@ -29,6 +28,7 @@ using namespace clang; //===----------------------------------------------------------------------===// static cl::OptionCategory CodeRefactorCategory("atomics-replacer options"); +// TODO: make the prefix (e.g. `__tmp_`source.cpp) a external parameter as well static cl::opt ClassNameToReplaceOpt{ "replace-name", cl::desc("The name of the class/struct which usages should be renamed"), diff --git a/runtime/include/ltest_atomic.h b/runtime/include/ltest_atomic.h new file mode 100644 index 00000000..a8b6f26d --- /dev/null +++ b/runtime/include/ltest_atomic.h @@ -0,0 +1,38 @@ +#pragma once + +#include +#include + +// TODO: write proper delegration to std::atomic here. +// This class is intended to be the entry point +// for the weak memory logic later. +template +struct LTestAtomic { + std::atomic a; + + T load(std::memory_order order = std::memory_order_seq_cst) const { + std::cout << "LTestAtomic load()" << std::endl; + return a.load(order); + } + + void store(T desired, std::memory_order order = std::memory_order_seq_cst) noexcept { + std::cout << "LTestAtomic store()" << std::endl; + a.store(desired, order); + } + + T fetch_add(T arg, std::memory_order order = std::memory_order_seq_cst) noexcept { + std::cout << "LTestAtomic fetch_add()" << std::endl; + return a.fetch_add(arg, order); + } + + bool compare_exchange_strong(T& expected, T val, std::memory_order order = std::memory_order_seq_cst) noexcept { + std::cout << "LTestAtomic compare_exchange_strong()" << std::endl; + return a.compare_exchange_strong(expected, val, order); + } + + T operator=(T desired) noexcept { + std::cout << "LTestAtomic operator=()" << std::endl; + store(desired); + return desired; + } +}; \ No newline at end of file diff --git a/runtime/include/verifying.h b/runtime/include/verifying.h index 810a8445..0363ee41 100644 --- a/runtime/include/verifying.h +++ b/runtime/include/verifying.h @@ -14,6 +14,10 @@ #include "strategy_verifier.h" #include "syscall_trap.h" #include "verifying_macro.h" +// This include is important, because when clangpass substitutes std::atomic usages with +// LTestAtomic, the new class should be included into the target source files. +// It will be guaranteed, since verifying.h is included in all targets. +#include "ltest_atomic.h" namespace ltest { diff --git a/verifying/CMakeLists.txt b/verifying/CMakeLists.txt index 9e279b1f..3006115e 100644 --- a/verifying/CMakeLists.txt +++ b/verifying/CMakeLists.txt @@ -1,18 +1,50 @@ include_directories(lib) include_directories(specs) -set (PASS YieldPass) -set (PASS_PATH ${CMAKE_BINARY_DIR}/codegen/lib${PASS}.so) +set(PASS YieldPass) +set(PASS_PATH ${CMAKE_BINARY_DIR}/codegen/lib${PASS}.so) + +set(CLANG_PASS ClangPass) +set(CLANG_TOOL ClangPassTool) +set(CLANG_PASS_LIB ${CMAKE_BINARY_DIR}/clangpass/lib${CLANG_PASS}.so) +set(CLANG_TOOL_EXECUTABLE ${CMAKE_BINARY_DIR}/clangpass/${CLANG_TOOL}) find_package(Boost REQUIRED COMPONENTS context) function(verify_target target) - add_executable(${target} ${source_name}) + # message("Target: ${target}, sources: ${source_name}") + + if (APPLY_CLANG_TOOL) + # here we prefix the actual source file name with '__tmp_' which will be generate by clang pass tool + add_executable(${target} __tmp_${source_name}) + else() + add_executable(${target} ${source_name}) + endif() add_dependencies(${target} runtime plugin_pass) target_include_directories(${target} PRIVATE ${CMAKE_SOURCE_DIR} ${CMAKE_SOURCE_DIR}/third_party) target_link_options(${target} PRIVATE ${CMAKE_ASAN_FLAGS}) target_compile_options(${target} PRIVATE -fpass-plugin=${PASS_PATH} ${CMAKE_ASAN_FLAGS}) target_link_libraries(${target} PRIVATE runtime ${PASS} gflags ${Boost_LIBRARIES}) + + add_custom_command( + OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/__tmp_${source_name} + COMMAND ${CLANG_TOOL_EXECUTABLE} + -p=${CMAKE_BINARY_DIR}/compile_commands.json + --replace-name=::std::atomic + --insert-name=LTestAtomic + ${CMAKE_CURRENT_SOURCE_DIR}/${source_name} + DEPENDS ${CLANG_TOOL} + COMMENT "Running Clang Pass Tool on ${source_name}" + ) + + if (APPLY_CLANG_TOOL) + add_custom_command( + TARGET ${target} + POST_BUILD + COMMAND ${CMAKE_COMMAND} -E echo "Removing temporary file '${CMAKE_CURRENT_SOURCE_DIR}/__tmp_${source_name}' generated after building ${target}" + COMMAND ${CMAKE_COMMAND} -E remove ${CMAKE_CURRENT_SOURCE_DIR}/__tmp_${source_name} + ) + endif() endfunction() add_subdirectory(targets) From 0b466e9f538d79d8b74d6231e1bf8f32263ce2a6 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Wed, 19 Mar 2025 23:33:49 +0000 Subject: [PATCH 39/47] Add some comments --- verifying/CMakeLists.txt | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/verifying/CMakeLists.txt b/verifying/CMakeLists.txt index 3006115e..97150790 100644 --- a/verifying/CMakeLists.txt +++ b/verifying/CMakeLists.txt @@ -26,18 +26,21 @@ function(verify_target target) target_compile_options(${target} PRIVATE -fpass-plugin=${PASS_PATH} ${CMAKE_ASAN_FLAGS}) target_link_libraries(${target} PRIVATE runtime ${PASS} gflags ${Boost_LIBRARIES}) - add_custom_command( - OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/__tmp_${source_name} - COMMAND ${CLANG_TOOL_EXECUTABLE} - -p=${CMAKE_BINARY_DIR}/compile_commands.json - --replace-name=::std::atomic - --insert-name=LTestAtomic - ${CMAKE_CURRENT_SOURCE_DIR}/${source_name} - DEPENDS ${CLANG_TOOL} - COMMENT "Running Clang Pass Tool on ${source_name}" - ) - + if (APPLY_CLANG_TOOL) + # here we are applying clangpass to the ${source_name} file + add_custom_command( + OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/__tmp_${source_name} + COMMAND ${CLANG_TOOL_EXECUTABLE} + -p=${CMAKE_BINARY_DIR}/compile_commands.json + --replace-name=::std::atomic + --insert-name=LTestAtomic + ${CMAKE_CURRENT_SOURCE_DIR}/${source_name} + DEPENDS ${CLANG_TOOL} + COMMENT "Running Clang Pass Tool on ${source_name}" + ) + + # here we delete the temp file generated by previous command add_custom_command( TARGET ${target} POST_BUILD From 775223c443901358dd29df27799c1526a12cddc2 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Wed, 19 Mar 2025 23:35:06 +0000 Subject: [PATCH 40/47] Add comments --- verifying/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verifying/CMakeLists.txt b/verifying/CMakeLists.txt index 97150790..c2dcc06e 100644 --- a/verifying/CMakeLists.txt +++ b/verifying/CMakeLists.txt @@ -32,7 +32,7 @@ function(verify_target target) add_custom_command( OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/__tmp_${source_name} COMMAND ${CLANG_TOOL_EXECUTABLE} - -p=${CMAKE_BINARY_DIR}/compile_commands.json + -p=${CMAKE_BINARY_DIR}/compile_commands.json # passing compilation database, make sure CMAKE_EXPORT_COMPILE_COMMANDS flag is set --replace-name=::std::atomic --insert-name=LTestAtomic ${CMAKE_CURRENT_SOURCE_DIR}/${source_name} From 4540df9d9f0c2e0ecf315d60c3c7164f1b3138fd Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Mar 2025 00:48:52 +0000 Subject: [PATCH 41/47] Fix clangpass shared lib compilation --- clangpass/CMakeLists.txt | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/clangpass/CMakeLists.txt b/clangpass/CMakeLists.txt index 735e6368..aa06bccc 100644 --- a/clangpass/CMakeLists.txt +++ b/clangpass/CMakeLists.txt @@ -22,7 +22,13 @@ if(${SUPPORTS_FVISIBILITY_INLINES_HIDDEN_FLAG} EQUAL "1") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fvisibility-inlines-hidden") endif() -add_library(ClangPass SHARED clangpass.cpp) +add_library(ClangPass SHARED "${CMAKE_CURRENT_SOURCE_DIR}/clangpass.cpp") + +target_include_directories( + ClangPass + PRIVATE + "${CMAKE_CURRENT_SOURCE_DIR}/include" +) target_include_directories( ClangPass From 988d9bad08aaa464c04dd2e4726cdc3900116219 Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Mar 2025 02:05:53 +0000 Subject: [PATCH 42/47] Mirrow the std::atomic public API --- runtime/include/ltest_atomic.h | 312 +++++++++++++++++++++++++++++++-- 1 file changed, 295 insertions(+), 17 deletions(-) diff --git a/runtime/include/ltest_atomic.h b/runtime/include/ltest_atomic.h index a8b6f26d..b44489bf 100644 --- a/runtime/include/ltest_atomic.h +++ b/runtime/include/ltest_atomic.h @@ -3,36 +3,314 @@ #include #include -// TODO: write proper delegration to std::atomic here. // This class is intended to be the entry point // for the weak memory logic later. template -struct LTestAtomic { - std::atomic a; +class LTestAtomic { + std::atomic atomicValue; - T load(std::memory_order order = std::memory_order_seq_cst) const { - std::cout << "LTestAtomic load()" << std::endl; - return a.load(order); +public: + #if __cplusplus >= 201703L // C++17 + static constexpr bool is_always_lock_free = std::atomic::is_always_lock_free; + #endif + + // Constructors + constexpr LTestAtomic() noexcept = default; + constexpr LTestAtomic(T desired) noexcept : atomicValue(desired) {} + LTestAtomic(const LTestAtomic&) = delete; + LTestAtomic& operator=(const LTestAtomic&) = delete; + LTestAtomic& operator=(const LTestAtomic&) volatile = delete; + + // operator= + T operator=(T desired) noexcept { + store(desired); + return desired; } + T operator=(T desired) volatile noexcept { + store(desired); + return desired; + } + + // is_lock_free + bool is_lock_free() const noexcept { + return atomicValue.is_lock_free(); + } + + bool is_lock_free() const volatile noexcept { + return atomicValue.is_lock_free(); + } + + // store void store(T desired, std::memory_order order = std::memory_order_seq_cst) noexcept { - std::cout << "LTestAtomic store()" << std::endl; - a.store(desired, order); + atomicValue.store(desired, order); + } + + void store(T desired, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + atomicValue.store(desired, order); + } + + // load + T load(std::memory_order order = std::memory_order_seq_cst) const noexcept { + return atomicValue.load(order); + } + + T load(std::memory_order order = std::memory_order_seq_cst) const volatile noexcept { + return atomicValue.load(order); + } + + // operator T() + operator T() const noexcept { + return atomicValue.load(); + } + + operator T() const volatile noexcept { + return atomicValue.load(); + } + + // exchange + T exchange(T desired, std::memory_order order = std::memory_order_seq_cst) noexcept { + return atomicValue.exchange(desired, order); + } + + T exchange(T desired, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + return atomicValue.exchange(desired, order); + } + + // compare_exchange_weak + bool compare_exchange_weak(T& expected, T desired, std::memory_order success, std::memory_order failure) noexcept { + atomicValue.compare_exchange_weak(expected, desired, success, failure); + } + + bool compare_exchange_weak(T& expected, T desired, std::memory_order success, std::memory_order failure) volatile noexcept { + atomicValue.compare_exchange_weak(expected, desired, success, failure); + } + + bool compare_exchange_weak(T& expected, T desired, std::memory_order order = std::memory_order_seq_cst) noexcept { + atomicValue.compare_exchange_weak(expected, desired, order); + } + + bool compare_exchange_weak(T& expected, T desired, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + atomicValue.compare_exchange_weak(expected, desired, order); + } + + // compare_exchange_strong + bool compare_exchange_strong(T& expected, T desired, std::memory_order success, std::memory_order failure) noexcept { + return atomicValue.compare_exchange_strong(expected, desired, success, failure); + } + + bool compare_exchange_strong(T& expected, T desired, std::memory_order success, std::memory_order failure) volatile noexcept { + return atomicValue.compare_exchange_strong(expected, desired, success, failure); + } + + bool compare_exchange_strong(T& expected, T desired, std::memory_order order = std::memory_order_seq_cst) noexcept { + return atomicValue.compare_exchange_strong(expected, desired, order); + } + + bool compare_exchange_strong(T& expected, T desired, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + return atomicValue.compare_exchange_strong(expected, desired, order); + } + + // wait + #if __cplusplus >= 202002L // C++20 + void wait(T old, std::memory_order order = std::memory_order_seq_cst) const noexcept { + atomicValue.wait(old, order); + } + + void wait(T old, std::memory_order order = std::memory_order_seq_cst) const volatile noexcept { + atomicValue.wait(old, order); } + // notify_one + void notify_one() noexcept { + atomicValue.notify_one(); + } + + void notify_one() volatile noexcept { + atomicValue.notify_one(); + } + + // notify all + void notify_all() noexcept { + atomicValue.notify_all(); + } + + void notify_all() volatile noexcept { + atomicValue.notify_all(); + } + #endif + + // fetch_add T fetch_add(T arg, std::memory_order order = std::memory_order_seq_cst) noexcept { - std::cout << "LTestAtomic fetch_add()" << std::endl; - return a.fetch_add(arg, order); + return atomicValue.fetch_add(arg, order); + } + + T fetch_add(T arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + return atomicValue.fetch_add(arg, order); + } + + T* fetch_add(std::ptrdiff_t arg, std::memory_order order = std::memory_order_seq_cst) noexcept { + return atomicValue.fetch_add(arg, order); } - bool compare_exchange_strong(T& expected, T val, std::memory_order order = std::memory_order_seq_cst) noexcept { - std::cout << "LTestAtomic compare_exchange_strong()" << std::endl; - return a.compare_exchange_strong(expected, val, order); + T* fetch_add(std::ptrdiff_t arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + return atomicValue.fetch_add(arg, order); } - T operator=(T desired) noexcept { - std::cout << "LTestAtomic operator=()" << std::endl; - store(desired); - return desired; + // fetch_sub + T fetch_sub(T arg, std::memory_order order = std::memory_order_seq_cst) noexcept { + return atomicValue.fetch_sub(arg, order); + } + + T fetch_sub(T arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + return atomicValue.fetch_sub(arg, order); + } + + T* fetch_sub(std::ptrdiff_t arg, std::memory_order order = std::memory_order_seq_cst) noexcept { + return atomicValue.fetch_sub(arg, order); + } + + T* fetch_sub(std::ptrdiff_t arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + return atomicValue.fetch_sub(arg, order); + } + + // operator+= + T operator+=(T arg) noexcept { + return atomicValue.operator+=(arg); + } + + T operator+=(T arg) volatile noexcept { + return atomicValue.operator+=(arg); + } + + T* operator+=(std::ptrdiff_t arg) noexcept { + return atomicValue.operator+=(arg); + } + + T* operator+=(std::ptrdiff_t arg) volatile noexcept { + return atomicValue.operator+=(arg); + } + + // operator-= + T operator-=(T arg) noexcept { + return atomicValue.operator-=(arg); + } + + T operator-=(T arg) volatile noexcept { + return atomicValue.operator-=(arg); + } + + T* operator-=(std::ptrdiff_t arg) noexcept { + return atomicValue.operator-=(arg); + } + + T* operator-=(std::ptrdiff_t arg) volatile noexcept { + return atomicValue.operator-=(arg); + } + + // fetch_max + T fetch_max(T arg, std::memory_order order = std::memory_order_seq_cst) noexcept { + return atomicValue.fetch_max(arg, order); + } + + T fetch_max(T arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + return atomicValue.fetch_max(arg, order); + } + + // fetch_min + T fetch_min(T arg, std::memory_order order = std::memory_order_seq_cst) noexcept { + return atomicValue.fetch_min(arg, order); + } + + T fetch_min(T arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + return atomicValue.fetch_min(arg, order); + } + + // operator++ + T operator++() noexcept { + return atomicValue.operator++(); + } + + T operator++() volatile noexcept { + return atomicValue.operator++(); + } + + T operator++(int) noexcept { + return atomicValue.operator++(0); + } + + T operator++(int) volatile noexcept { + return atomicValue.operator++(0); + } + + // operator-- + T operator--() noexcept { + return atomicValue.operator--(); + } + + T operator--() volatile noexcept { + return atomicValue.operator--(); + } + + T operator--(int) noexcept { + return atomicValue.operator--(0); + } + + T operator--(int) volatile noexcept { + return atomicValue.operator--(0); + } + + // fetch_and + T fetch_and(T arg, std::memory_order order = std::memory_order_seq_cst) noexcept { + return atomicValue.fetch_and(arg, order); + } + + T fetch_and(T arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + return atomicValue.fetch_and(arg, order); + } + + // fetch_or + T fetch_or(T arg, std::memory_order order = std::memory_order_seq_cst) noexcept { + return atomicValue.fetch_or(arg, order); + } + + T fetch_or(T arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + return atomicValue.fetch_or(arg, order); + } + + // fetch_xor + T fetch_xor(T arg, std::memory_order order = std::memory_order_seq_cst) noexcept { + return atomicValue.fetch_xor(arg, order); + } + + T fetch_xor(T arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + return atomicValue.fetch_xor(arg, order); + } + + // operator&= + T operator&=(T arg) noexcept { + return atomicValue.operator&=(arg); + } + + T operator&=(T arg) volatile noexcept { + return atomicValue.operator&=(arg); + } + + // operator|= + T operator|=(T arg) noexcept { + return atomicValue.operator|=(arg); + } + + T operator|=(T arg) volatile noexcept { + return atomicValue.operator|=(arg); + } + + // operator^= + T operator^=(T arg) noexcept { + return atomicValue.operator^=(arg); + } + + T operator^=(T arg) volatile noexcept { + return atomicValue.operator^=(arg); } }; \ No newline at end of file From 6370af2e38742a677f44bd9d1959d460ef3cbacb Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Mar 2025 02:13:14 +0000 Subject: [PATCH 43/47] Comment out ambigious overload for T*. Add todo for fixing that --- clangpass/CMakeLists.txt | 6 ------ 1 file changed, 6 deletions(-) diff --git a/clangpass/CMakeLists.txt b/clangpass/CMakeLists.txt index aa06bccc..2eae4dda 100644 --- a/clangpass/CMakeLists.txt +++ b/clangpass/CMakeLists.txt @@ -30,12 +30,6 @@ target_include_directories( "${CMAKE_CURRENT_SOURCE_DIR}/include" ) -target_include_directories( - ClangPass - PRIVATE - "${CMAKE_CURRENT_SOURCE_DIR}/include" -) - # Allow undefined symbols in shared objects on Darwin (this is the default # behaviour on Linux) target_link_libraries(ClangPass From f2b8044f12dd82b99201df2c6ac56e1321da72ee Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Thu, 27 Mar 2025 02:13:14 +0000 Subject: [PATCH 44/47] Comment out ambigious overload for T*. Add todo for fixing that --- runtime/include/ltest_atomic.h | 52 ++++++++++++++++++---------------- 1 file changed, 28 insertions(+), 24 deletions(-) diff --git a/runtime/include/ltest_atomic.h b/runtime/include/ltest_atomic.h index b44489bf..dd6c00eb 100644 --- a/runtime/include/ltest_atomic.h +++ b/runtime/include/ltest_atomic.h @@ -149,13 +149,14 @@ class LTestAtomic { return atomicValue.fetch_add(arg, order); } - T* fetch_add(std::ptrdiff_t arg, std::memory_order order = std::memory_order_seq_cst) noexcept { - return atomicValue.fetch_add(arg, order); - } + // TODO: fix ambiguity with specialization for T* + // T* fetch_add(std::ptrdiff_t arg, std::memory_order order = std::memory_order_seq_cst) noexcept { + // return atomicValue.fetch_add(arg, order); + // } - T* fetch_add(std::ptrdiff_t arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { - return atomicValue.fetch_add(arg, order); - } + // T* fetch_add(std::ptrdiff_t arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + // return atomicValue.fetch_add(arg, order); + // } // fetch_sub T fetch_sub(T arg, std::memory_order order = std::memory_order_seq_cst) noexcept { @@ -166,13 +167,14 @@ class LTestAtomic { return atomicValue.fetch_sub(arg, order); } - T* fetch_sub(std::ptrdiff_t arg, std::memory_order order = std::memory_order_seq_cst) noexcept { - return atomicValue.fetch_sub(arg, order); - } + // TODO: fix ambiguity with specialization for T* + // T* fetch_sub(std::ptrdiff_t arg, std::memory_order order = std::memory_order_seq_cst) noexcept { + // return atomicValue.fetch_sub(arg, order); + // } - T* fetch_sub(std::ptrdiff_t arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { - return atomicValue.fetch_sub(arg, order); - } + // T* fetch_sub(std::ptrdiff_t arg, std::memory_order order = std::memory_order_seq_cst) volatile noexcept { + // return atomicValue.fetch_sub(arg, order); + // } // operator+= T operator+=(T arg) noexcept { @@ -183,13 +185,14 @@ class LTestAtomic { return atomicValue.operator+=(arg); } - T* operator+=(std::ptrdiff_t arg) noexcept { - return atomicValue.operator+=(arg); - } + // TODO: fix ambiguity with specialization for T* + // T* operator+=(std::ptrdiff_t arg) noexcept { + // return atomicValue.operator+=(arg); + // } - T* operator+=(std::ptrdiff_t arg) volatile noexcept { - return atomicValue.operator+=(arg); - } + // T* operator+=(std::ptrdiff_t arg) volatile noexcept { + // return atomicValue.operator+=(arg); + // } // operator-= T operator-=(T arg) noexcept { @@ -200,13 +203,14 @@ class LTestAtomic { return atomicValue.operator-=(arg); } - T* operator-=(std::ptrdiff_t arg) noexcept { - return atomicValue.operator-=(arg); - } + // TODO: fix ambiguity with specialization for T* + // T* operator-=(std::ptrdiff_t arg) noexcept { + // return atomicValue.operator-=(arg); + // } - T* operator-=(std::ptrdiff_t arg) volatile noexcept { - return atomicValue.operator-=(arg); - } + // T* operator-=(std::ptrdiff_t arg) volatile noexcept { + // return atomicValue.operator-=(arg); + // } // fetch_max T fetch_max(T arg, std::memory_order order = std::memory_order_seq_cst) noexcept { From 70ffe4dd68befca6f1ee3d6424f138b95d5ef99d Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Tue, 1 Apr 2025 21:47:43 +0000 Subject: [PATCH 45/47] Fix github actions (take from master) --- .github/workflows/run-tests.yaml | 79 +------------------------------- 1 file changed, 2 insertions(+), 77 deletions(-) diff --git a/.github/workflows/run-tests.yaml b/.github/workflows/run-tests.yaml index 4da451a9..ca8aaccd 100644 --- a/.github/workflows/run-tests.yaml +++ b/.github/workflows/run-tests.yaml @@ -72,82 +72,7 @@ jobs: # fi - name: Run nonlinear_queue with random strategy run: | - ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy random --minimization 1 || error_code=$? - if [ "${error_code}" -ne 1 ]; then - exit 1 - fi - - name: Run nonlinear_queue with pct strategy (minimization) - run: | - ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimize || error_code=$? - if [ "${error_code}" -ne 1 ]; then - exit 1 - fi - verifying-test-release: - runs-on: ubuntu-latest - defaults: - run: - shell: bash - container: - image: silkeh/clang:18 - options: --user root - steps: - - name: Install deps - run: | - apt update && apt install -y git ninja-build valgrind libgoogle-glog-dev libsnappy-dev protobuf-compiler libboost-context-dev pkg-config libcapstone-dev && \ - git clone https://github.com/Kirillog/syscall_intercept.git && \ - cmake syscall_intercept -G Ninja -B syscall_intercept/build -DCMAKE_INSTALL_PREFIX=/usr -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=clang && \ - cmake --build syscall_intercept/build --target install - - name: Check out repository code - uses: actions/checkout@v4 - - name: Build - run: | - cmake -G Ninja -B build -DCMAKE_BUILD_TYPE=Release - cmake --build build --target verifying/targets/nonlinear_queue verifying/targets/nonlinear_ms_queue verifying/targets/nonlinear_treiber_stack verifying/targets/nonlinear_set verifying/blocking/nonlinear_mutex verifying/blocking/simple_mutex - - name: Run nonlinear_queue with random strategy (minimization) - run: | - ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy random --minimize || error_code=$? - if [ "${error_code}" -ne 1 ]; then - exit 1 - fi - - name: Run nonlinear_queue with pct strategy (minimization) - run: | - ./build/verifying/targets/nonlinear_queue --tasks 40 --rounds 100000 --strategy pct --minimize || error_code=$? - if [ "${error_code}" -ne 1 ]; then - exit 1 - fi - - name: Run nonlinear_ms_queue with random strategy (minimization) - run: | - ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy random --minimize || error_code=$? - if [ "${error_code}" -ne 1 ]; then - exit 1 - fi - - name: Run nonlinear_ms_queue with pct strategy (minimization) - run: | - ./build/verifying/targets/nonlinear_ms_queue --tasks 40 --rounds 100000 --strategy pct --minimize || error_code=$? - if [ "${error_code}" -ne 1 ]; then - exit 1 - fi - - name: Run nonlinear_treiber_stack with random strategy (minimization) - run: | - ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy random --minimize || error_code=$? - if [ "${error_code}" -ne 1 ]; then - exit 1 - fi - - name: Run nonlinear_treiber_stack with pct strategy (minimization) - run: | - ./build/verifying/targets/nonlinear_treiber_stack --tasks 40 --rounds 100000 --strategy pct --minimize || error_code=$? - if [ "${error_code}" -ne 1 ]; then - exit 1 - fi - - name: Run nonlinear_set with random strategy (minimization) - run: | - ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy random --minimize || error_code=$? - if [ "${error_code}" -ne 1 ]; then - exit 1 - fi - - name: Run nonlinear_set with pct strategy (minimization) - run: | - ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy pct --minimize || error_code=$? + ./build/verifying/targets/nonlinear_queue --tasks 4 --rounds 100000 --strategy random --switches 1 || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 fi @@ -237,4 +162,4 @@ jobs: ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy pct --minimize || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 - fi + fi \ No newline at end of file From 16ee54ca7a3e90ccf9956fcd3b2d0343ad86713f Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Tue, 1 Apr 2025 21:48:07 +0000 Subject: [PATCH 46/47] Fix github actions --- .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 ca8aaccd..a809b7af 100644 --- a/.github/workflows/run-tests.yaml +++ b/.github/workflows/run-tests.yaml @@ -162,4 +162,4 @@ jobs: ./build/verifying/targets/nonlinear_set --tasks 40 --rounds 200000 --strategy pct --minimize || error_code=$? if [ "${error_code}" -ne 1 ]; then exit 1 - fi \ No newline at end of file + fi From fc03f76ff8b5c2ddd0998fd0be6b50f2f00a4ffb Mon Sep 17 00:00:00 2001 From: Dmitrii Artiukhov Date: Tue, 1 Apr 2025 21:53:53 +0000 Subject: [PATCH 47/47] Take CI & Dockerfile from PR #18 --- .github/workflows/clang-format.yaml | 3 ++- .github/workflows/run-tests.yaml | 13 +++++++------ Dockerfile | 2 +- 3 files changed, 10 insertions(+), 8 deletions(-) diff --git a/.github/workflows/clang-format.yaml b/.github/workflows/clang-format.yaml index cbb2777e..fb99263a 100644 --- a/.github/workflows/clang-format.yaml +++ b/.github/workflows/clang-format.yaml @@ -10,5 +10,6 @@ jobs: - name: Run clang-format style check uses: jidicula/clang-format-action@v4.13.0 with: - clang-format-version: '14' + clang-format-version: '19' check-path: '.' + fallback-style: 'Google' diff --git a/.github/workflows/run-tests.yaml b/.github/workflows/run-tests.yaml index a809b7af..493977b8 100644 --- a/.github/workflows/run-tests.yaml +++ b/.github/workflows/run-tests.yaml @@ -3,6 +3,7 @@ on: push: pull_request: branches: [ "master" ] + jobs: unit-tests: runs-on: ubuntu-latest @@ -10,11 +11,11 @@ jobs: run: shell: bash container: - image: silkeh/clang:18 + image: silkeh/clang:19 options: --user root steps: - name: Install deps - run: apt update && apt install -y git ninja-build valgrind libboost-context-dev libgflags-dev + run: apt update && apt install -y git ninja-build valgrind libboost-context-dev libgflags-dev libclang-19-dev - name: Check out repository code uses: actions/checkout@v4 - name: Build @@ -29,12 +30,12 @@ jobs: run: shell: bash container: - image: silkeh/clang:18 + image: silkeh/clang:19 options: --user root steps: - name: Install deps run: | - apt update && apt install -y git ninja-build valgrind libgoogle-glog-dev libsnappy-dev protobuf-compiler libboost-context-dev pkg-config libcapstone-dev && \ + apt update && apt install -y git ninja-build valgrind libgoogle-glog-dev libsnappy-dev protobuf-compiler libboost-context-dev pkg-config libcapstone-dev libclang-19-dev && \ git clone https://github.com/Kirillog/syscall_intercept.git && \ cmake syscall_intercept -G Ninja -B syscall_intercept/build -DCMAKE_INSTALL_PREFIX=/usr -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=clang && \ cmake --build syscall_intercept/build --target install @@ -100,12 +101,12 @@ jobs: run: shell: bash container: - image: silkeh/clang:18 + image: silkeh/clang:19 options: --user root steps: - name: Install deps run: | - apt update && apt install -y git ninja-build valgrind libgoogle-glog-dev libsnappy-dev protobuf-compiler libboost-context-dev pkg-config libcapstone-dev && \ + apt update && apt install -y git ninja-build valgrind libgoogle-glog-dev libsnappy-dev protobuf-compiler libboost-context-dev pkg-config libcapstone-dev libclang-19-dev && \ git clone https://github.com/Kirillog/syscall_intercept.git && \ cmake syscall_intercept -G Ninja -B syscall_intercept/build -DCMAKE_INSTALL_PREFIX=/usr -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=clang && \ cmake --build syscall_intercept/build --target install diff --git a/Dockerfile b/Dockerfile index 377dbfd1..1b55f1ad 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,6 +1,6 @@ FROM silkeh/clang:19 AS ltest -RUN apt update && apt install -y git ninja-build valgrind libboost-context-dev libgflags-dev libstdc++-11-dev +RUN apt update && apt install -y git ninja-build valgrind libboost-context-dev libgflags-dev libstdc++-11-dev libclang-19-dev RUN mv /usr/lib/gcc/x86_64-linux-gnu/12 /usr/lib/gcc/x86_64-linux-gnu/_12 FROM ltest as blocking