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

chore: checkInterrupted ~> checkCanceled, requestInterrupt ~> cancel

Browse source
This commit is contained in:
Sebastian Ullrich 2020-09-04 14:00:06 +02:00
parent 77cbaa752c
commit 469a822cc6
4 changed files with 24 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/include/lean/lean.h
View file

@ -211,7 +211,7 @@ typedef struct {
struct lean_task * m_head_dep;
struct lean_task * m_next_dep;
unsigned m_prio;
uint8_t m_interrupted;
uint8_t m_canceled;
// If true, task will not be freed until finished
uint8_t m_keep_alive;
uint8_t m_deleted;
@ -1189,13 +1189,13 @@ static inline lean_obj_res lean_task_get_own(lean_obj_arg t) {
return r;
}
/* primitive for implementing `IO.checkInterrupt : IO bool` */
bool lean_io_check_interrupt_core();
/* primitive for implementing `IO.requestInterrupt : Task a -> IO Unit` */
void lean_io_request_interrupt_core(b_lean_obj_arg t);
/* primitive for implementing `IO.checkCanceled : IO Bool` */
bool lean_io_check_canceled_core();
/* primitive for implementing `IO.cancel : Task a -> IO Unit` */
void lean_io_cancel_core(b_lean_obj_arg t);
/* primitive for implementing `IO.hasFinished : Task a -> IO Unit` */
bool lean_io_has_finished_core(b_lean_obj_arg t);
/* primitive for implementing `IO.waitAny : List (Task a) -> IO (Task a) */
/* primitive for implementing `IO.waitAny : List (Task a) -> IO (Task a)` */
b_lean_obj_res lean_io_wait_any_core(b_lean_obj_arg task_list);
/* External objects */

8
src/include/lean/object.h
View file

@ -304,13 +304,9 @@ inline obj_res task_bind(obj_arg x, obj_arg f, unsigned prio = 0, bool keep_aliv
inline obj_res task_map(obj_arg f, obj_arg t, unsigned prio = 0, bool keep_alive = false) { return lean_task_map_with_prio(f, t, prio, keep_alive); }
inline b_obj_res task_get(b_obj_arg t) { return lean_task_get(t); }
/* primitive for implementing `io.check_interrupt : io bool` */
inline bool io_check_interrupt_core() { return lean_io_check_interrupt_core(); }
/* primitive for implementing `io.request_interrupt : task A -> io unit` */
inline void io_request_interrupt_core(b_obj_arg t) { return lean_io_request_interrupt_core(t); }
/* primitive for implementing `io.has_finished : task A -> io unit` */
inline bool io_check_canceled_core() { return lean_io_check_canceled_core(); }
inline void io_cancel_core(b_obj_arg t) { return lean_io_cancel_core(t); }
inline bool io_has_finished_core(b_obj_arg t) { return lean_io_has_finished_core(t); }
/* primitive for implementing `io.wait_any : list (task A) -> io (task A) */
inline b_obj_res io_wait_any_core(b_obj_arg task_list) { return lean_io_wait_any_core(task_list); }
// =======================================

20
src/runtime/object.cpp
View file

@ -623,7 +623,7 @@ static lean_task_imp * alloc_task_imp(obj_arg c, unsigned prio, bool keep_alive)
imp->m_head_dep = nullptr;
imp->m_next_dep = nullptr;
imp->m_prio = prio;
imp->m_interrupted = false;
imp->m_canceled = false;
imp->m_keep_alive = keep_alive;
imp->m_deleted = false;
return imp;
@ -772,8 +772,8 @@ class task_manager {
lean_task_object * it = t->m_imp->m_head_dep;
t->m_imp->m_head_dep = nullptr;
while (it) {
if (t->m_imp->m_interrupted)
it->m_imp->m_interrupted = true;
if (t->m_imp->m_canceled)
it->m_imp->m_canceled = true;
lean_task_object * next_it = it->m_imp->m_next_dep;
it->m_imp->m_next_dep = nullptr;
if (it->m_imp->m_deleted) {
@ -806,7 +806,7 @@ public:
for (worker_info * info : m_workers) {
if (info->m_task) {
lean_assert(info->m_task->m_imp);
info->m_task->m_imp->m_interrupted = true;
info->m_task->m_imp->m_canceled = true;
}
}
m_shutting_down = true;
@ -883,10 +883,10 @@ public:
}
}
void request_interrupt(lean_task_object * t) {
void cancel(lean_task_object * t) {
unique_lock<mutex> lock(m_mutex);
if (t->m_imp)
t->m_imp->m_interrupted = true;
t->m_imp->m_canceled = true;
}
};
@ -1032,18 +1032,18 @@ extern "C" obj_res lean_task_bind_with_prio(obj_arg x, obj_arg f, unsigned prio,
}
}
extern "C" bool lean_io_check_interrupt_core() {
extern "C" bool lean_io_check_canceled_core() {
if (lean_task_object * t = g_current_task_object) {
lean_assert(t->m_imp); // task is being executed
return t->m_imp->m_interrupted;
return t->m_imp->m_canceled;
}
return false;
}
extern "C" void lean_io_request_interrupt_core(b_obj_arg t) {
extern "C" void lean_io_cancel_core(b_obj_arg t) {
if (lean_to_task(t)->m_value)
return;
g_task_manager->request_interrupt(lean_to_task(t));
g_task_manager->cancel(lean_to_task(t));
}
extern "C" bool lean_io_has_finished_core(b_obj_arg t) {

12
src/tests/util/object.cpp
View file

@ -200,7 +200,7 @@ void tst6() {
obj_res task4_fn(obj_arg) {
show_msg("task 4 started...\n");
while (!io_check_interrupt_core()) {
while (!io_check_canceled_core()) {
show_msg("task 4 loop...\n");
this_thread::sleep_for(std::chrono::milliseconds(10));
}
@ -215,7 +215,7 @@ void tst7() {
std::cout << "task4 has finished: " << io_has_finished_core(task4.raw()) << "\n";
this_thread::sleep_for(std::chrono::milliseconds(100));
show_msg("request interrupt...\n");
io_request_interrupt_core(task4.raw());
io_cancel_core(task4.raw());
object * r = task_get(task4.raw());
std::cout << "task4 has finished after get: " << io_has_finished_core(task4.raw()) << "\n";
std::cout << "r: " << unbox(r) << "\n";
@ -250,7 +250,7 @@ void tst8() {
}
obj_res loop_until_interrupt_fn(obj_arg) {
while (!io_check_interrupt_core()) {
while (!io_check_canceled_core()) {
this_thread::sleep_for(std::chrono::milliseconds(1));
}
return box(0);
@ -283,8 +283,8 @@ void tst9() {
show_msg("wait_any returned...\n");
object * v = task_get(t);
lean_assert(unbox(v) == 42);
io_request_interrupt_core(t1.raw());
io_request_interrupt_core(t2.raw());
io_cancel_core(t1.raw());
io_cancel_core(t2.raw());
task_get(t1.raw());
task_get(t2.raw());
}
@ -315,7 +315,7 @@ void tst11() {
static atomic<bool> g_finished;
obj_res loop_until_interrupt_fn2(obj_arg) {
while (!io_check_interrupt_core()) {
while (!io_check_canceled_core()) {
this_thread::sleep_for(std::chrono::milliseconds(1));
}
g_finished = true;