1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208
/*!
Adapted from a file automatically generated by rust-bindgen 0.60.1 from `lean.h`.
Comments adapted from `lean.h`.
*/
mod incomplete_array;
use core::ffi::{c_char, c_int, c_uint, c_void};
pub use incomplete_array::*;
/**
Lean object header.
The reference counter `m_rc` field also encodes whether the object is single threaded (> 0), multi threaded (< 0), or
reference counting is not needed (== 0). We don't use reference counting for objects stored in compact regions, or
marked as persistent.
For "small" objects stored in compact regions, the field `m_cs_sz` contains the object size. For "small" objects not
stored in compact regions, we use the page information to retrieve its size.
During deallocation and 64-bit machines, the fields `m_rc` and `m_cs_sz` store the next object in the deletion TODO list.
These two fields together have 48-bits, and this is enough for modern computers.
In 32-bit machines, the field `m_rc` is sufficient.
The field `m_other` is used to store the number of fields in a constructor object and the element size in a scalar array.
*/
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_object {
pub m_rc: c_int,
pub m_cs_sz: u16,
pub m_other: u8,
pub m_tag: u8,
}
/// Standard object argument
pub type lean_obj_arg = *mut lean_object;
/// Borrowed object argument
pub type b_lean_obj_arg = *mut lean_object;
/// Unique (aka non shared) object argument
pub type u_lean_obj_arg = *mut lean_object;
/// Standard object result
pub type lean_obj_res = *mut lean_object;
/// Borrowed object result
pub type b_lean_obj_res = *mut lean_object;
#[repr(C)]
#[derive(Debug)]
pub struct lean_ctor_object {
pub m_header: lean_object,
pub m_objs: IncompleteArrayField<*mut lean_object>,
}
/// Array arrays
#[repr(C)]
#[derive(Debug)]
pub struct lean_array_object {
pub m_header: lean_object,
pub m_size: usize,
pub m_capacity: usize,
pub m_data: IncompleteArrayField<*mut lean_object>,
}
/// Scalar arrays
#[repr(C)]
#[derive(Debug)]
pub struct lean_sarray_object {
pub m_header: lean_object,
pub m_size: usize,
pub m_capacity: usize,
pub m_data: IncompleteArrayField<u8>,
}
#[repr(C)]
#[derive(Debug)]
pub struct lean_string_object {
pub m_header: lean_object,
/// Byte length including `\0` terminator
pub m_size: usize,
pub m_capacity: usize,
/// UTF-8 length
pub m_length: usize,
pub m_data: IncompleteArrayField<c_char>,
}
#[repr(C)]
#[derive(Debug)]
pub struct lean_closure_object {
pub m_header: lean_object,
pub m_fun: *mut c_void,
/// Number of arguments expected by `m_fun`
pub m_arity: u16,
//TODO: already been fixed?
/// Number of arguments that have been already fixed
pub m_num_fixed: u16,
pub m_objs: IncompleteArrayField<*mut lean_object>,
}
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_ref_object {
pub m_header: lean_object,
pub m_value: *mut lean_object,
}
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_thunk_object {
pub m_header: lean_object,
pub m_value: u64,
pub m_closure: u64,
}
/** Data required for executing a Lean task. It is released as soon as
the task terminates even if the task object itself is still referenced. */
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_task_imp {
pub m_closure: *mut lean_object,
pub m_head_dep: *mut lean_task,
pub m_next_dep: *mut lean_task,
pub m_prio: c_uint,
pub m_canceled: u8,
/// If true, task will not be freed until finished
pub m_keep_alive: u8,
pub m_deleted: u8,
}
/** 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)
*/
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_task {
pub m_header: lean_object,
pub m_value: u64,
pub m_imp: *mut lean_task_imp,
}
pub type lean_task_object = lean_task;
pub type lean_external_finalize_proc = Option<unsafe extern "C" fn(arg1: *mut c_void)>;
pub type lean_external_foreach_proc =
Option<unsafe extern "C" fn(arg1: *mut c_void, arg2: b_lean_obj_arg)>;
/* Object for wrapping external data. */
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_external_class {
pub m_finalize: lean_external_finalize_proc,
pub m_foreach: lean_external_foreach_proc,
}
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_external_object {
pub m_header: lean_object,
pub m_class: *mut lean_external_class,
pub m_data: *mut c_void,
}