#[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)
- condition: in
- 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
underspawn_worker
lock)
- condition: reachable from task via
- Promised
- condition: obtained as result from promise
- invariant:
m_imp != nullptr && m_value == nullptr
- transition: promise resolved ==> Finished (
resolve_core
underspawn_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)
- condition:
- 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 bydeactivate_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
- condition:
- Finished
- condition:
m_value != nullptr
- invariant:
m_imp == nullptr
- transition: RC becomes 0 ==> freed (
deactivate_task
lock)
- condition:
Fields§
§m_header: lean_object
§m_value: u64
§m_imp: *mut lean_task_imp
Trait Implementations§
Auto Trait Implementations§
impl RefUnwindSafe for lean_task
impl !Send for lean_task
impl !Sync for lean_task
impl Unpin for lean_task
impl UnwindSafe for lean_task
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more