diff --git a/comments.org b/comments.org index 8983079caf6d68bff453fa6ffdc4d32391e22c38..6a09745d48259482f2fb2f26acd82312802750cb 100644 --- a/comments.org +++ b/comments.org @@ -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 to restore the invariant before closing it. * 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`: +#+BEGIN_SRC +x ↦ᵢ n+1 ⊢ {E,E;Γ} ⊧ K[()] ≤ t : τ +---------------------------------------- +x ↦ᵢ n ⊢ {E,E;Γ} ⊧ K[inc #x ()] ≤ t : τ +#+END_SRC +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 +atomic. + +We may want to write the aforementioned rule in a different style: +#+BEGIN_SRC + 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 : τ). +#+END_SRC +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 + ECOOP'2014 + + http://www.doc.ic.ac.uk/~pmd09/research/publications/2014/ecoop/tada-a-logic-for-time-and-data-abstraction + +- 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: + + https://gitlab.mpi-sws.org/FP/iris-atomic + + 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=? =bin_log_related_cas_l= is a rule in [[file:F_mu_ref_conc/relational_properties.v]]