From 9a90024f7a837cf9827d312c449631cd8053fbdb Mon Sep 17 00:00:00 2001
From: Dan Frumin
Date: Tue, 11 Jul 2017 11:44:06 +0200
Subject: [PATCH] Add comments on logically atomic specifications
---
comments.org | 62 ++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 62 insertions(+)
diff --git a/comments.org b/comments.org
index 8983079..6a09745 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]]
--
GitLab