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

feat(library/task_queue): add flag to prevent priority inversion

Browse source
This commit is contained in:
Gabriel Ebner 2016-12-16 13:41:00 -05:00 • committed by Leonardo de Moura
parent 063130ee18
commit bc09a53f71
3 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/kernel/environment.cpp
View file

@ -218,6 +218,7 @@ public:
environment_check_task(environment const & env) : m_env(env) {}
bool is_tiny() const override { return true; }
bool do_priority_inversion() const override { return false; }
void description(std::ostream & out) const override {
out << "checking environment for incorrect proofs (" << get_module_id() << ")";

10
src/library/mt_task_queue.cpp
View file

@ -268,10 +268,12 @@ bool mt_task_queue::check_deps(generic_task_result const & t) {
try {
deps = unwrap(t)->m_task->get_dependencies();
} catch (...) {}
for (auto & dep : deps) {
if (dep) {
submit_core(dep);
bump_prio(dep, get_prio(t));
if (unwrap(t)->m_task->do_priority_inversion()) {
for (auto & dep : deps) {
if (dep) {
submit_core(dep);
bump_prio(dep, get_prio(t));
}
}
}
for (auto & dep : deps) {

2
src/util/task_queue.h
View file

@ -138,6 +138,8 @@ public:
virtual std::vector<generic_task_result> get_dependencies() { return {}; }
virtual bool is_tiny() const { return false; }
virtual bool do_priority_inversion() const { return true; }
virtual task_kind get_kind() const { return task_kind::elab; }
virtual pos_info get_pos() const { return get_task_pos(); }