Struct lean_sys::lean_task

source ·

#[repr(C)]pub struct lean_task {
    pub m_header: lean_object,
    pub m_value: u64,
    pub m_imp: *mut lean_task_imp,
}

Expand description

Object of type Task _. The lifetime of a lean_task object can be represented as a state machine with atomic state transitions.

In the following, condition describes a predicate uniquely identifying a state.

creation:

Task.spawn ==> Queued
Task.map/bind ==> Waiting
Task.pure ==> Finished
Promise.new ==> Promised

states:

Queued
- condition: in task_manager::m_queues && m_imp != nullptr && !m_imp->m_deleted
- invariant: m_value == nullptr
- transition: RC becomes 0 ==> Deactivated (deactivate_task lock)
- transition: dequeued by worker thread ==> Running (spawn_worker lock)
Waiting
- condition: reachable from task via m_head_dep->m_next_dep->... && !m_imp->m_deleted
- invariant: m_imp != nullptr && m_value == nullptr
- invariant: task dependency is Queued/Waiting/Running
  - It cannot become Deactivated because this task should be holding an owned reference to it
- transition: RC becomes 0 ==> Deactivated (deactivate_task lock)
- transition: task dependency Finished ==> Queued (handle_finished under spawn_worker lock)
Promised
- condition: obtained as result from promise
- invariant: m_imp != nullptr && m_value == nullptr
- transition: promise resolved ==> Finished (resolve_core under spawn_worker lock)
- transition: RC becomes 0 ==> Deactivated (deactivate_task lock)
Running
- condition: m_imp != nullptr && m_imp->m_closure == nullptr
  - The worker takes ownership of the closure when running it
- invariant: m_value == nullptr
- transition: RC becomes 0 ==> Deactivated (deactivate_task lock)
- transition: finished execution ==> Finished (spawn_worker lock)
Deactivated
- condition: m_imp != nullptr && m_imp->m_deleted
- invariant: RC == 0
- invariant: m_imp->m_closure == nullptr && m_imp->m_head_dep == nullptr (both freed by deactivate_task_core)
  - Note that all dependent tasks must have already been Deactivated by the converse of the second Waiting invariant
- invariant: m_value == nullptr
- transition: dequeued by worker thread ==> freed
- transition: finished execution ==> freed
- transition: task dependency Finished ==> freed
- We must keep the task object alive until one of these transitions because in either case, we have live (internal, unowned) references to the task up to that point
- transition: task dependency Deactivated ==> freed
Finished
- condition: m_value != nullptr
- invariant: m_imp == nullptr
- transition: RC becomes 0 ==> freed (deactivate_task lock)