max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(util/task): remove switch to disable priority inversion

Browse source
This commit is contained in:
Gabriel Ebner 2017-02-24 15:21:59 +01:00
parent 26ba9c23a7
commit 45820531c4
3 changed files with 1 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/mt_task_queue.cpp
View file

@ -215,12 +215,11 @@ bool mt_task_queue::check_deps(gtask const & t) {
get_data(t)->m_imp->get_dependencies(deps);
} catch (...) {}
auto do_prio_inv = get_data(t)->m_flags.m_do_priority_inversion;
auto prio = get_prio(t);
for (auto & dep : deps) {
if (dep) {
submit_core(dep, prio);
if (do_prio_inv) bump_prio(dep, prio);
bump_prio(dep, prio);
}
}

1
src/util/task.h
View file

@ -24,7 +24,6 @@ struct scheduling_info {
};
struct task_flags {
bool m_do_priority_inversion = true;
bool m_needs_separate_thread = true;
bool m_eager_execution = false;
};

6
src/util/task_builder.h
View file

@ -68,12 +68,6 @@ public:
m_imp(new base_task_imp<Fn>(std::forward<Fn>(fn))),
m_cancel_tok(global_cancellation_token()) {}
task_builder<Res> disable_priority_inversion() {
lean_assert(m_imp);
m_flags.m_do_priority_inversion = false;
return std::move(*this);
}
task_builder<Res> does_not_require_own_thread() {
lean_assert(m_imp);
m_flags.m_needs_separate_thread = false;