based on: https://gist.github.com/pervognsen/052f3062db9545b43a7e9350130cb964
type TaskFn = fn (_ : void*) -> void*;
fn create(task_data : void*, task_fn : TaskFn) : TaskId;
fn discard(task : TaskId);
fn blocked_by(task : TaskId, predecessor : TaskId);
fn start(task : TaskId);
tasks(task_id, ptr, fn). % unique(task_id)
blocked_by(task_id, p_task_id). % unique(task_id, p_task_id)
started_tasks(task_id, status). % unique(task_id)
executing(task_id, core_id). % unique(task_id), @pre: started_tasks(T, status=started), all(blocked_by(T, T2), started_tasks(T2, status=done)))
fn create(task_data : void*, task_fn : TaskFn) : TaskId;
post: tasks(new_task_id, task_data, task_fn).
post: frame(ret0, new_task_id).
fn discard(task : TaskId);
pre: not(started_tasks(task_id=task)).
post: retract(blocked_by(T, task_id=task). retract(tasks(task_id=task).
fn blocked_by(task : TaskId, predecessor : TaskId);
pre: tasks(task, P, F), \+ started_tasks(task).
post: blocked_by(task, predecessor).
fn start(task : TaskId);
pre: tasks(task, Ptr, Fn), \+ started_tasks(task, started).
post: started_tasks(task, started).
also sometimes later: execute_task
transform is performed on task and w/ any core C which is available
fn dispatch_per_core();
post: execute_task on random_combination((CoreId,TaskId), idle_cores(CoreId), started_tasks(TaskId, status=started) ^ not(executing(TaskId)) ^ all(blocked_by(TaskId, T), started_tasks(T, status=done)).
Pairs each executable task with a core, in order to call execute_task
fairly over the available cores.
fn execute_task(task : TaskId, core);
pre: started_tasks(task, started), \+ executing(task, AnyCore), all(blocked_by(task, PrevTask), started_tasks(PrevTask, done)).
post: executing(task, core).
post: tasks(task, Ptr, Fn), pc(core, value=Fn), frame(core, arg0, data=Ptr).
fn finish_task(task : TaskId, core);
pre: pc(core,Value). % Value returned from Fn, Ptr for task
post: retract(executing(core, task)), started_tasks(task, done).