Commit 7c97c6ec authored by Dan Frumin's avatar Dan Frumin

Describe the threadpool tactics in greater detail

parent dbed0373
......@@ -4,29 +4,56 @@ iris-logrel reference manual
Threadpool tactics
------------------
All of the tactics in this section assume that you have a resource `j ⤇ e`
and a goal of the form `|={E}=>` with `↑specN ⊆ E`, e.g. `P ∗ (j ⤇ e) ⊢ |={⊤}=> Q`.
The tactics below allow for a symbolic execution of the logical
threadpool.
- `tp_normalise j`: simplify the term/expression in `j ⤇ e`
- `tp_bind j e'`: if `j ⤇ e` and `e` can be decomposed as `K[e']`,
then turn the resource into `j ⤇ K[e']`. For example if, `j ⤇ f
(!x + 2)`, then invoking `tp_bind j (Load x)` converts the resource
then turn the resource into `j ⤇ K[e']`. For example if, `j ⤇ f (!x + 2)`,
then invoking `tp_bind j (Load x)` converts the resource
to `j ⤇ fill [AppRCtx f, PlusLCtx 2] (!x)`. All the tactics below,
apart from `tp_apply` use this bind facility to find a subterm in
the threadpool of an appropriate shape.
- `tp_store j`
- `tp_load j`
- `tp_rec j`
- `tp_op j`/`tp_nat_binop j`
- `tp_cas_fail j` and `tp_cas_suc j`
- `tp_tlam j`
- `tp_fold j`
- `tp_pack j`
- `tp_fst j`, `tp_snd j`
- `tp_case_inl j`,`tp_case_inr j`
- `tp_if_true j`,`tp_if_false j`
- `tp_fork i as j "Hj"`
- `tp_store j`: if `j ⤇ K[#l <- v2]` and `l ↦ₛ v1` are in the
context, then replace them with `j ⤇ K[#()]` and `l ↦ₛ v2`
- `tp_load j`: if `j ⤇ K[! #l]` and `l ↦ₛ v` are in the context,
then replace them with `j ⤇ K[v]` and `l ↦ₛ v`.
- `tp_rec j`: if `j ⤇ K[(rec f x := e) v]` (or `j ⤇ K[(λx. e) v]`)
is in the context, then replace it with `j ⤇ K[e[x:=v,f:=(rec f x := e)]]`
(or `j ⤇ K[e[x:=v]]`).
- `tp_op j`/`tp_nat_binop j`: if `j ⤇ K[v1 ⊕ v2]` is in the context, then
replace it with `j ⤇ K[v3]` whenever `v1 ⊕ v2` evaluates to `v3`.
- `tp_cas_fail j`: if `j ⤇ K[CAS #l v1 v2]` and `l ↦ₛ v'` are in the
context and `v' ≠ v1` holds, then replace the threadpool resource with `j ⤇ K[#♭ false]`.
- `tp_cas_suc j`: if `j ⤇ K[CAS #l v1 v2]` and `l ↦ₛ v'` are in the
context and `v' = v1` holds, then replace the threadpool resource with `j ⤇ K[#♭ true]`
and replace `l ↦ₛ v'` with `l ↦ₛ v2`
- `tp_tlam j`: if `j ⤇ K[Λ.e]` is in the context, then replace it with
`j ⤇ K[e]`
- `tp_fold j`: if `j ⤇ K[Unfold (Fold v)]` is in the context, then replace it with
`j ⤇ K[v]`
- `tp_pack j`: if `j ⤇ K[unpack v e]` is in the context, then replace
it with `j ⤇ K[e v]`
- `tp_fst j`, `tp_snd j`: if `j ⤇ K[fst (v1,v2)]` (resp. `j ⤇ K[snd (v1,v2)]`)
is in the context, then replace it with `j ⤇ K[v1]` (resp. `j ⤇ K[v2]`)
- `tp_case_inl j`,`tp_case_inr j`: if `j ⤇ K[case (inl v) e1 e2]` (resp. `j ⤇ K[case (inr v) e1 e2]`)
is in the context, the replace it with `j ⤇ K[e1 v]` (resp. `j ⤇ K[e2 v]`)
- `tp_if_true j`,`tp_if_false j`: if `j ⤇ K[if (#♭ true) e1 e2]` (resp. `j ⤇ K[if (#♭ false) e1 e2]`)
is in the context, the replace it with `j ⤇ K[e1]` (resp. `j ⤇ K[e2]`)
- `tp_fork j as i "Hi"`: if `j ⤇ K[fork(e)]` is in the context, then replace it with `j ⤇ K[#()]`
and add `Hi: i ⤇ e` to the context.
Additional forms:
+ `tp_fork i as j` is the same thing as `let H := iFresh in tp_fork i as j H`
+ `tp_fork i` has a similar behaviour, but...
- `tp_alloc j as l "Hl"`
- `tp_apply j lem with "H1 ... Hn" as "S"`
+ `tp_fork i` has a similar behaviour, but changes your goal from `|={E}=> Q` to
`∀ (j' : nat), j' ⤇ e' ={E}=∗ Q`.
- `tp_alloc j as l "Hl"`: if `j ⤇ K[alloc v]` is in the context, then replace it with `j ⤇ K[#l]`
and add `Hl : l ↦ₛ v` to the context.
Additional forms:
+ `tp_alloc i as j` is the same thing as `let H := iFresh in tp_alloc i as j H`
- `tp_apply j lem with "H1 ... Hn" as "S"`: **TODO**
Weakest precondition calculus tactics
-------------------------------------
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment