Commit 52e1ebe5 by Dan Frumin

### [lock proof] Put the masks variables in a section

parent f7f0423d
 ... ... @@ -54,20 +54,22 @@ Hint Resolve with_lock_type : typeable. Section proof. Context `{cfgSG Σ}. Context `{heapIG Σ}. Lemma steps_newlock E ρ j K : nclose specN ⊆ E → Variable (E1 E2 : coPset). Lemma steps_newlock ρ j K (Hcl : nclose specN ⊆ E1) : spec_ctx ρ -∗ j ⤇ fill K newlock ={E}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ (#♭v false). ={E1}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ (#♭v false). Proof. iIntros (HNE) "#Hspec Hj". iIntros "#Hspec Hj". tp_alloc j as l "Hl". tp_normalise j. by iExists _; iFrame. Qed. Lemma bin_log_related_newlock_r Γ K t τ : (∀ l : loc, l ↦ₛ (#♭v false) -∗ Γ ⊨ t ≤log≤ fill K (Loc l) : τ)%I -∗ Γ ⊨ t ≤log≤ fill K newlock : τ. Lemma bin_log_related_newlock_r Γ K t τ (Hcl : nclose specN ⊆ E1) : (∀ l : loc, l ↦ₛ (#♭v false) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (Loc l) : τ)%I -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K newlock : τ. Proof. iIntros "Hlog". unfold newlock. ... ... @@ -77,21 +79,21 @@ Section proof. Global Opaque newlock. Transparent acquire. Lemma steps_acquire E ρ j K l : nclose specN ⊆ E → Lemma steps_acquire ρ j K l (Hcl : nclose specN ⊆ E1) : spec_ctx ρ -∗ l ↦ₛ (#♭v false) -∗ j ⤇ fill K (App acquire (Loc l)) ={E}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ (#♭v true). ={E1}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ (#♭v true). Proof. iIntros (HNE) "#Hspec Hl Hj". iIntros "#Hspec Hl Hj". unfold acquire. tp_rec j. tp_cas_suc j. tp_if_true j. tp_normalise j. by iFrame. Qed. Qed. Lemma bin_log_related_acquire_r Γ E1 E2 K l t τ (Hspec : nclose specN ⊆ E1) : Lemma bin_log_related_acquire_r Γ K l t τ (Hcl : nclose specN ⊆ E1) : l ↦ₛ (#♭v false) -∗ (l ↦ₛ (#♭v true) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ)%I -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App acquire (Loc l)) : τ. ... ... @@ -109,19 +111,19 @@ Section proof. Global Opaque acquire. Transparent release. Lemma steps_release E ρ j K l b: nclose specN ⊆ E → Lemma steps_release ρ j K l b (Hcl : nclose specN ⊆ E1) : spec_ctx ρ -∗ l ↦ₛ (#♭v b) -∗ j ⤇ fill K (App release (Loc l)) ={E}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ (#♭v false). ={E1}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ (#♭v false). Proof. iIntros (HNE) "#Hspec Hl Hj". unfold release. iIntros "#Hspec Hl Hj". unfold release. tp_rec j. tp_store j. tp_normalise j. by iFrame. Qed. Lemma bin_log_related_release_r Γ K E1 E2 l t τ b (Hspec : nclose specN ⊆ E1): Lemma bin_log_related_release_r Γ K l t τ b (Hcl : nclose specN ⊆ E1) : l ↦ₛ (#♭v b) -∗ (l ↦ₛ (#♭v false) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ)%I -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App release (Loc l)) : τ. ... ... @@ -134,16 +136,16 @@ Section proof. Global Opaque release. Lemma steps_with_lock E ρ j K e ev l P Q v w: nclose specN ⊆ E → Lemma steps_with_lock ρ j K e ev l P Q v w: to_val e = Some ev → (∀ K', spec_ctx ρ -∗ P -∗ j ⤇ fill K' (App e (of_val w)) ={E}=∗ j ⤇ fill K' (of_val v) ∗ Q) → ={E1}=∗ j ⤇ fill K' (of_val v) ∗ Q) → (nclose specN ⊆ E1) → spec_ctx ρ -∗ P -∗ l ↦ₛ (#♭v false) -∗ j ⤇ fill K (App (with_lock e (Loc l)) (of_val w)) ={E}=∗ j ⤇ fill K (of_val v) ∗ Q ∗ l ↦ₛ (#♭v false). ={E1}=∗ j ⤇ fill K (of_val v) ∗ Q ∗ l ↦ₛ (#♭v false). Proof. iIntros (HNE Hev Hpf) "#Hspec HP Hl Hj". iIntros (Hev Hpf ?) "#Hspec HP Hl Hj". unfold with_lock. unlock. (* TODO :( *) tp_rec j; eauto; simpl. rewrite !Closed_subst_id. (* simplify subst automatically? *) ... ... @@ -166,11 +168,11 @@ Section proof. by iFrame. Qed. Lemma bin_log_related_with_lock_r Γ K E1 E2 Q e ev ew cl v w l t τ : (nclose specN ⊆ E1) → Lemma bin_log_related_with_lock_r Γ K Q e ev ew cl v w l t τ : (to_val e = Some cl) → (to_val ev = Some v) → (to_val ew = Some w) → (nclose specN ⊆ E1) → (∀ K, (Q -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K ev : τ) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App e ew) : τ) -∗ l ↦ₛ (#♭v false) -∗ ... ... @@ -185,7 +187,7 @@ Section proof. iApply (bin_log_related_rec_r); eauto. simpl. rewrite !Closed_subst_id. iApply (bin_log_related_rec_r); eauto. simpl. rewrite !Closed_subst_id. rel_bind_r (App acquire (Loc l)). iApply (bin_log_related_acquire_r Γ E1 E2 (_ ++ K) l with "Hl"); auto. iApply (bin_log_related_acquire_r Γ (_ ++ K) l with "Hl"); auto. iIntros "Hl". simpl. iApply (bin_log_related_rec_r); eauto. simpl. rel_bind_r (App e ew). ... ... @@ -198,41 +200,5 @@ Section proof. iApply ("Hlog" with "HQ Hl"). Qed. (* TODO: is this still useful? *) (* Lemma bin_log_related_with_lock_r' Γ K E1 E2 P Q e v w l t τ : *) (* (nclose specN ⊆ E1) → *) (* (∀ f, e.[f] = e) (* e is a closed term *) → *) (* (∀ f, (of_val v).[f] = of_val v) (* v is a closed term *) → *) (* (∀ f, (of_val w).[f] = of_val w) (* w is a closed term *) → *) (* (∀ ρ j K', spec_ctx ρ -∗ P -∗ j ⤇ fill K' (App e (of_val w)) *) (* ={E1}=∗ j ⤇ fill K' (of_val v) ∗ Q) → *) (* P -∗ *) (* l ↦ₛ (#♭v false) -∗ *) (* (l ↦ₛ (#♭v false) -∗ Q -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (of_val v) : τ)%I *) (* -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App (with_lock e (Loc l)) (of_val w)) : τ. *) (* Proof. *) (* iIntros (?????) "HP Hl Hlog". *) (* pose (Φ := (fun (w: val) => ⌜w = v⌝ ∗ Q ∗ l ↦ₛ (#♭v false))%I). *) (* iApply (bin_log_related_step_r Φ with "[HP Hl]"). *) (* { intros. *) (* replace ((App (with_lock e (Loc l)) (of_val w)).[f]) *) (* with (App (with_lock e (Loc l)).[f] (of_val w).[f]); auto. *) (* rewrite with_lock_closed. *) (* all: repeat lazymatch goal with *) (* | [Hcl : ∀ s, ?e.[s] = ?e |- context[?e.[_]]] *) (* => rewrite Hcl *) (* | [Hcl : ∀ s, ?e = ?e.[s] |- context[?e.[?F]]] *) (* => rewrite -(Hcl F) *) (* end; try done. } *) (* { cbv[Φ]. *) (* iIntros (ρ j K') "#Hs Hj /=". *) (* iMod (steps_with_lock _ _ j K' _ l P Q with "Hs HP Hl Hj") *) (* as "[Hj [HQ Hl]]"; auto. *) (* iExists v. iFrame. *) (* iModIntro. auto. } *) (* iIntros (v') "[% [HQ Hl]]". subst. *) (* iApply ("Hlog" with "Hl HQ"). *) (* Qed. *) Global Opaque with_lock. End proof.
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