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).