comments.org 10.7 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
* Rules that didn't make it
** A binding rule for the semantic judgment that /nearly/ works.
A rule that we would like to have
#+BEGIN_SRC 
WP e {{ v, {E,E;Γ} ⊧ K[v] ≤ e₂ : τ }}
-----------------------------------------
{E,E;Γ} ⊧ K[e₁] ≤ e₂ : τ
#+END_SRC
However, this rule is too weak. Consider a derivation where =e₁= is
atomic and we want to open an invariant to symbolically execute it.
#+BEGIN_SRC 
|={E1,E2}=> WP e {{ v, |={E2,E1}=> {E1,E1;Γ} ⊧ K[v] ≤ e₂ : τ }}
---------------------------------------------------------------- wp-atomic
WP e {{ v, {E1,E1;Γ} ⊧ K[v] ≤ e₂ : τ }}_E1
-----------------------------------------
{E1,E1;Γ} ⊧ K[e₁] ≤ e₂ : τ
#+END_SRC
After employing such reasoning we can open up an invariant, and
symbolically execute =e₁=. But then we are left with
#+BEGIN_SRC 
|={E2,E1}=> {E1,E1;Γ} ⊧ K[v] ≤ e₂ : τ
#+END_SRC
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
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
** 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.
Dan Frumin's avatar
Dan Frumin committed
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118
** 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]]

We already have =bin_log_related_cas_suc_l= and
=bin_log_related_cas_fail_l=. However, those rules are not sufficient
for our purposes, as we might not know whether the CAS succeeds
/before/ we open the invariant.

Example: proof of =bin_log_FG_increment_logatomic= in counter.v
** subst_p_rec with binders
#+BEGIN_SRC 
  Lemma subst_p_rec (x f : binder) e1 e2 e `{Closed ∅ e2} :
    subst_p (<[x:=e2]>{[f:=(Rec f x e1)]}) e =
    subst' f (Rec f x e1) (subst' x e2 e).
#+END_SRC
We need a version of this lemma with x and f binders
in order to prove the compatibility lemma for lambdas

#+BEGIN_SRC 
□ (<[x:=τ1]>(<[f:=TArrow τ1 τ2]>Γ) ⊨ e ≤log≤ e' : τ2) -∗
Γ ⊨ Rec f x e ≤log≤ Rec f x e' : TArrow τ1 τ2.
#+END_SRC

To show tht (rec f x e, rec f x e') are related, we use the definition
of the arrow type, so we have some values (v, v') related at τ1. Then
we would like to use the hypothesis by inserting (v, v') in the
environment substitution. But then we have =subst_p (<[x:=(v,v')]>
...) e=. You would like to convert that to =subst' x ..= so that one
can actually use the hypothesis.

119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
* Comments on the design
** Common setting for different symbolic execution tactics
There are multiple layers of tactics for symbolic execution in the code.
*** Layers of tactics
We have symbolic execution rules (either as lemmas or as tactics and tactic lemmas) for
- WP calculus
- Symbolic execution in the ghost threadpool
- Symbolic execution in the relational interpretation
*** Tactics and tactic lemmas
Here we make a distinction between an actual /tactic/ and a /tacic lemma/.
A /tactic lemma/ is a lemma in Coq that is a Coq proposition that is saying more than a certain ~iProp~ holds.
Hence, the tacic lemma is typechecked. A /tactic/ is an actual piece of Ltac code that makes it more convenient to apply the aforementioned lemma.
For instance, this is a tactic lemma for symbolically executing a ~Load~ in the ghost threadpool.
#+BEGIN_SRC coq
Lemma tac_tp_load `{logrelG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e l v Q q :
  nclose specN ⊆ E1 →
  envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
  envs_lookup_delete i2 Δ1 = Some (false, j ⤇ e, Δ2)%I →
  e = fill K' (Load (Loc l)) →
  envs_lookup i3 Δ2 = Some (false, l ↦ₛ{q} v)%I →
  envs_simple_replace i3 false 
    (Esnoc (Esnoc Enil i2 (j ⤇ fill K' (of_val v))) i3 (l ↦ₛ{q} v)%I) Δ2 = Some Δ3 →
  (Δ3 ⊢ |={E1,E2}=> Q) →
  (Δ1 ⊢ |={E1,E2}=> Q).
#+END_SRC
It takes care of managing the context in a typesafe way.
Then this lemma is actually applied with the help of the following tactic
#+BEGIN_SRC coq
Tactic Notation "tp_load" constr(j) :=
  iStartProof;
  eapply (tac_tp_load j);
    [solve_ndisj || fail "tp_load: cannot prove 'nclose specN ⊆ ?'"
    |iAssumptionCore || fail "tp_load: cannot find spec_ctx" (* spec_ctx *)
    |iAssumptionCore || fail "tp_load: cannot find '" j " ⤇ ?'" 
    |tp_bind_helper
    |iAssumptionCore || fail "tp_load: cannot find '? ↦ₛ ?'"
    |env_cbv; reflexivity || fail "tp_load: this should not happen"
    |(* new goal *)].
#+END_SRC
The tactic itself provides error messages as well as some means of discharging the assumptions for the tactic lemma.
Since the tactic lemma is being ~eapply~ed, it is always important to think about the order we put the assumptions in the lemma.
At the moment we apply the lemma Coq's unification mechanism instantiates ~Δ1~, ~E1~, ~E2~, and ~Q~.
We need to make sure that by discharging the assumptions in the correct order we can instantiate ~Δ3~ to something meaningful.
For instance, the fourth assumption says something about the shape of the expression that is executed in thread ~j~; however, this expression is not known until we lookup it up in the context.
Hence, the fourth assumption should come *after* the third one.
Likewise, the fifth assumption says that there is a resource ~l ↦ₛ v~ in context ~Δ2~, but we only know the location ~l~ once we decompose the expression ~e~ into an evaluation context and a load expression.
Thus, this assumption should come after ~e = fill K'(Load (Loc l))~.
*** Pure reductions
Since ultimately all the levels of the symbolic executions operate on the same language we can share some machinery between the levels.
One observation is that the easiest (as well as the most numerous) tactics to write are those that preform symbolic execution of pure reductions.
To that extent we would like to have one generic "pure symbolic reduction" tactic/tactic lemma per level.
This is achieved by writing "open ended" tactic lemmas that are parameterized  over a typeclass of pure reductions.
The typeclass ~PureExec φ e1 e2~ says that there is a pure (and deterministic) reduction from ~e1~ to ~e2~ in the language under some (pure) assumption φ.
Dan Frumin's avatar
Dan Frumin committed
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
Using this typeclass and typeclass resolution we can write tactic lemmas that are easy to apply:
#+BEGIN_SRC
Lemma tac_rel_pure_r `{logrelG Σ} K e1 ℶ E1 E2 Δ Γ e e2 eres ϕ t τ :
  e = fill K e1 →
  PureExec ϕ e1 e2 →
  ϕ →
  nclose specN ⊆ E1 →
  eres = fill K e2 →
  (ℶ ⊢ {E1,E2;Δ;Γ} t ≤log≤ (fill K e2) : τ) →
  (ℶ ⊢ {E1,E2;Δ;Γ} t ≤log≤ e : τ).
#+END_SRC
When ~tac_rel_pure~ is applied, it tries to solve the first goal ~e = fill K e1~ by decomposing expression ~e~ in all the possible ways
and trying to unify it with ~e1~. After that it searches for an appropriate ~PureExec~ instance.
The whole process is implemented in the following tactic
#+BEGIN_SRC
Tactic Notation "rel_pure_r" open_constr(ef) :=
  iStartProof;
  rel_reshape_cont_r ltac:(fun K e' =>
      unify e' ef;
      simple eapply (tac_rel_pure_r K e');
      [tac_bind_helper             (* e = fill K e1 *)
      |apply _                     (* PureExec ϕ e1 e2 *)
      |try (exact I || reflexivity || tac_rel_done)  (* φ *)
      |solve_ndisj                 (* ↑specN ⊆ E1 *)
      |simpl; reflexivity          (* eres = fill K e2 *)
      |simpl_subst/=               (* new goal *)])
  || fail "rel_pure_r: cannot find the reduct".
#+END_SRC
Ignoring the "fail" part, we can see from the outline what is going on in the tactic:
- It tries to reshape the expression on the right hand side in the relational interpretation, until the tactic succeeds.
- It only proceeds with the specific decomposition if ~e = K[e']~ and ~e'~ unifies with ~ef~.
- After that, it applies the tactic lemma and tries to discharge the proof obligations in order
- Sometimes, the dependency ~φ~ in ~PureExec φ e1 e2~ can be discharged trivially by ~reflexivity~ or ~tac_rel_done~.
- We simplify the substitutions in the new goal, in case we do a beta-reduction