Commit 9a90024f authored by Dan Frumin's avatar Dan Frumin

Add comments on logically atomic specifications

parent b2e55982
...@@ -24,6 +24,68 @@ which means that we have to close the invariant *now*. However, it ...@@ -24,6 +24,68 @@ which means that we have to close the invariant *now*. However, it
might be the case that we need to symbolically execute =e₂= in order might be the case that we need to symbolically execute =e₂= in order
to restore the invariant before closing it. to restore the invariant before closing it.
* Assorted * Assorted
** Logically atomic rules for the relatoinal interpretation
<2017-07-10 ma>
Consider the following rule for the left hand side for some function `inc`:
x ↦ᵢ n+1 ⊢ {E,E;Γ} ⊧ K[()] ≤ t : τ
x ↦ᵢ n ⊢ {E,E;Γ} ⊧ K[inc #x ()] ≤ t : τ
For a definition of =inc= in F_mu_ref_conc we can prove this rule
using basic inductive rules for the left hand side. However, we may
encounter the same issue as with Hoare triples: this rule is unusable
in situations when `x ↦ n` is in the invariant. The program =inc= is
not actually atomic, so we cannot open the invariant around it.
However, it is /logically/ atomic, i.e. it behaves "as if" it is physically
We may want to write the aforementioned rule in a different style:
Lemma bin_log_FG_increment_logatomic R Γ E1 E2 K x t τ :
□ (|={E1,E2}=> ∃ n, x ↦ᵢ (#nv n) ∗ R(n) ∗
((∃ n, x ↦ᵢ (#nv n) ∗ R(n)) ={E2,E1}=∗ True) ∧
(∀ m, x ↦ᵢ (#nv (S m)) ∗ R(m) -∗
{E2,E1;Γ} ⊨ fill K (Lit Unit) ≤log≤ t : τ))
-∗ ({E1,E1;Γ} ⊨ fill K (FG_increment (Loc x) Unit) ≤log≤ t : τ).
To use this rule, we need to provide, possibly under an invariant (by
opening invariants in E1)
- a way of obtaining =x ↦ᵢ n= and a "frame" =R(n)=;
- a way of "reversing" the rule in case of failure;
- a way of "finishing up" the rule in case of success;
where the two last points do not have to be provided simultaneously.
*** Some references on logical atomicity
- Triples for logical atomicity have originally been introduced in the following paper:
TaDA: A Logic for Time and Data Abstraction
Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner
- In the original Iris 1.0 paper, it has been shown how atomic triples can be encoded in Iris (using view shifts, and higher-order quantification).
- Zhen Zhang, a former intern of Derek Dreyer, has made some progress at formalizing logical atomicity in Coq. His results can be found here:
He improved the definition of the logical atomic triple somewhat.
The relevant files to look at are: atomic.v, the definition of
logical atomic triples, atomic_incr.v, a proof for a simple atomic
incrementer, and treiber.v for Treiber stack.
** Why do we need the expressions to be closed everywhere?
<2017-07-10 ma>
(For many lemmas in [[file:F_mu_ref_conc/relational_properties.v]]
This is not a very serious restriction, as the "real" programs are always closed,
and you shouldn't attempt symbolic execution of open expressions.
For =wp_lift_pure_det_head_step_no_fork= you have to prove that your
expression is not a value -- this is no longer true if you have open
expressions. If you have =x=, then closing it up by an env
substitution will yield a value.
** Why do we have a single =bin_log_related_cas_l=? ** Why do we have a single =bin_log_related_cas_l=?
=bin_log_related_cas_l= is a rule in [[file:F_mu_ref_conc/relational_properties.v]] =bin_log_related_cas_l= is a rule in [[file:F_mu_ref_conc/relational_properties.v]]
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