Equations
- Mt.TaskM.instIsReservationReservation = spec.is_reservation
Validation primitive for reasoning for composable tasks.
Validation may assume assuming and must ensure the following:
- The task has to behave conform to the specification at all times
- The task never panics
- Finally,
motiveholds after the task completes
Proving valid #
The definition is rather cumbersome to work with. You should use
helper theorems like valid_pure, valid_bind, valid_rmr, ...
They are designed to be used with the apply tactic.
Blocking predicate: assuming #
When validating our task, we can assume assuming state = true. However,
in most cases we have assuming = λ _ => true, i.e. our hypothesis does
not provide anything useful.
There is one important exception: Blocking threads. If a thread waits for a certain condition before it continues its task, we can safely assume that this condition holds when the task is excuting.
Final goal: motive #
A valid thread must drop its reservations in the end. Therefore, the
final goal on those tasks is λ _ r => r = IsReservation.empty.
However, intermediate tasks (i.e. single operations) do not need to
share this goal.
In fact, they usally do not. If one operation prepares the next operation, it usually creates some reservation to ensure that no other thread undos this preparation. In this example, the motive should encode that the preparation has been made.
motive is the only way to pass facts from one iteration to the next.
See valid_bind for more information.
Equations
- One or more equations did not get rendered due to their size.
To prove that pure t is valid you need to prove that the motive holds
To prove that a >>= f is valid you need to prove that both a and f u
for all results u are valid.
In many cases, a does something to prepare f u. Since only f u needs
to fulfil the final motive, we can choose an arbitrary motive to validate a
as "intermediate goal".
To validate f u with the original motive, we can use the fact that the
intermediate goal motive_u has been ensured by a. Motives use only results
and reservations, which cannot be changed by other threads. Therefore, they
stay valid even if other threads become active between a and f u.