Monad to describe single threaded algorithms. Tasks can be iterated step by step until they finally complete or panic.
TaskM is a monad, i.e. you can use the do-notation to write code:
import Mt.Task.Basic
open Mt
abbrev spec : Spec :={
State := Nat,
Reservation := UnitReservation,
validate :=λ _ _ => True
}
def sample_task : TaskM spec Bool :=do
if (<- TaskM.atomic_read λ n => n) > 100 then
-- reset to 100
TaskM.atomic_read_modify λ _ => 100
return false
TaskM.atomic_assert λ n => n < 500
TaskM.atomic_read_modify λ n => n + 7
return true
Note: TaskM hat an associative bind operator, but it is not
a lawful monad: Binding two pure cannot be simplified into
a single pure, because it requires two iterations to complete.
Equations
- Mt.TaskM spec T = Mt.TaskM.impl.TaskM spec T
- Done: {spec : Mt.Spec} → {T : Type} → spec.State → T → Mt.TaskM.IterationResult spec T
- Panic: {spec : Mt.Spec} → {T : Type} → spec.State → String → Mt.TaskM.IterationResult spec T
- Running: {spec : Mt.Spec} → {T : Type} → spec.State → (spec.State → Bool) → Mt.TaskM spec T → Mt.TaskM.IterationResult spec T
The result of a single iteration of TaskM.
Independent of the result, the resulting shared state after
the iteration can be retrieved using IterationResult.state
Instances For
Equations
- One or more equations did not get rendered due to their size.
Atomic TaskM primitive with read/write-access to the shared state.
Additional to performing a read-modify operation, it returns a value.
Example: Compare Exchange (https://en.wikipedia.org/wiki/Compare-and-swap)
Atomic TaskM primitive to perform read-modify operations on the
shared state. It does not return anything.
Equations
- Mt.TaskM.atomic_read_modify f = Mt.TaskM.atomic_read_modify_read fun s => (PUnit.unit, f s)
Atomic TaskM primitive to perform read the shared state. It
does not change anything
Equations
- Mt.TaskM.atomic_read f = Mt.TaskM.atomic_read_modify_read fun s => let t := f s; (t, s)
Atomic TaskM primitive which throws an exception. The current thread
panics and will be removed from the system
Equations
- Mt.TaskM.panic msg = Mt.TaskM.impl.TaskM.panic msg
Atomic TaskM primitive to assert a given condition. The condition
is checked atomically. If it returns false, the current thread panics.
Equations
TaskM primitive which blocks the current thread until a given
condition holds, and executes a read-modify-read operation afterwards.
There are neither spurious wakeups nor race conditions: The system will only perform the read-modify-read operation if the provided condition holds. If it does not, the thread will block.
Equations
- Mt.TaskM.atomic_blocking_rmr block_until f = Mt.TaskM.impl.TaskM.atomic_blocking_rmr block_until f
Iterate a given thread on a given state and provides an IterationResult.
The task may complete or panic. If it is does not, it is still running and a continuation will be provided in the result
Equations
- One or more equations did not get rendered due to their size.
Iteration of pure t always completes with result t
Iteration of a >>= f iterates a and returns a continuation.
- If the
aiteration has completed with resultt, the next iteration will start work onf t - If the
aiteration has not completed yet, the next iteration will continue. - If
ahas panicked, the exception is propagated.
Iteration of a read-modify-read-operation will perform the read modify and complete with the computed result.
Iteration of a read-modify operation will perform the read modify
operation and complete with Unit.unit
Iteration of a read operation will compute a value based on the current shared state and complete with the result
Iteration of a panic will fail
Iteration of an assertion will atomically check the condition and succeed or fail depending on the result.
Iteration of a atomic_blocking_rmr operation will always
return a continuation.
The IterationResult contains the blocking predicate and
the desired read-modify-read operation. The caller should ensure
that the read-modify-operation is only iterated when the blocking
predicate holds.
- running: ∀ {spec : Mt.Spec} {T : Type} {p cont : Mt.TaskM spec T} {s s' : spec.State} {block_until : spec.State → Bool}, Mt.TaskM.iterate p s = Mt.TaskM.IterationResult.Running s' block_until cont → Mt.TaskM.is_direct_cont cont p
Well founded relation on TaskM fulfilled by continuations with their parents.
It can be used to perform well founded recursion TaskM without using the
implementation details of TaskM. Whenever TaskM.iterate returns a
continuation, the continuation will be smaller according to this
relation.
Instances For
Equations
- Mt.TaskM.instWf = { rel := Mt.TaskM.is_direct_cont, wf := (_ : WellFounded Mt.TaskM.is_direct_cont) }