Lock invariants and a "well-bracketed" control flow refinement

theories/examples/lock.v

 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import excl.
 From iris_logrel Require Export logrel.
 
 Definition newlock : val := λ: <>, ref #false.
@@ -38,8 +39,106 @@ Proof. solve_typed. Qed.
 
 Hint Resolve with_lock_type : typeable.
 
-Section proof.
+Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
+Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
+
+Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Proof. solve_inG. Qed.
+
+Section lockG_rules.
+  Context `{!lockG Σ, !logrelG Σ} (N: namespace).
+
+  Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
+    (∃ b : bool, l ↦ᵢ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I.
+
+  Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
+    (∃ l: loc, ⌜lk = #l⌝ ∧ inv N (lock_inv γ l R))%I.
+
+  Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
+
+  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
+  Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
+
+  Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
+  Proof. solve_proper. Qed.
+  Global Instance is_lock_ne l : NonExpansive (is_lock γ l).
+  Proof. solve_proper. Qed.
+
+  Global Instance is_lock_persistent γ l R : PersistentP (is_lock γ l R).
+  Proof. apply _. Qed.
+  Global Instance locked_timeless γ : TimelessP (locked γ).
+  Proof. apply _. Qed.
+
+  Lemma bin_log_related_newlock_l (R : iProp Σ) Δ Γ E K t τ :
+    R -∗
+    ▷(∀ (lk : loc) γ, is_lock γ #lk R
+      -∗ ({E,E;Δ;Γ} ⊨ fill K #lk ≤log≤ t: τ)) -∗
+    {E,E;Δ;Γ} ⊨ fill K (newlock #()) ≤log≤ t: τ.
+  Proof.
+    iIntros "HR Hlog".
+    iApply bin_log_related_wp_l.
+    rewrite -wp_fupd /newlock /=. unlock.
+    wp_seq. wp_alloc l as "Hl".
+    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
+    iMod (inv_alloc N _ (lock_inv γ l R) with "[-Hlog]") as "#?".
+    { iIntros "!>". iExists false. by iFrame. }
+    iModIntro. iApply "Hlog". iExists l. eauto.
+  Qed.
+
+  Lemma bin_log_related_release_l (R : iProp Σ) (lk : loc) γ Δ Γ E K t τ :
+    ↑N ⊆ E →
+    is_lock γ #lk R -∗
+    locked γ -∗
+    R -∗
+    ▷({E,E;Δ;Γ} ⊨ fill K #() ≤log≤ t: τ) -∗
+    {E,E;Δ;Γ} ⊨ fill K (release #lk) ≤log≤ t: τ.
+  Proof.
+    iIntros (?) "Hlock Hlocked HR Hlog".
+    iDestruct "Hlock" as (l) "[% #?]"; simplify_eq.
+    unlock release. simpl.
+    rel_let_l.
+    rel_store_l_atomic.
+    iInv N as (b) "[Hl _]" "Hclose".
+    iModIntro. iExists _. iFrame.
+    iNext. iIntros "Hl".
+    iMod ("Hclose" with "[-Hlog]").
+    { iNext. iExists false. by iFrame. }
+    iApply "Hlog".
+  Qed.
+
+  Lemma bin_log_related_acquire_l (R : iProp Σ) (lk : loc) γ Δ Γ E K t τ :
+    ↑N ⊆ E →
+    is_lock γ #lk R -∗
+    ▷(locked γ -∗ R -∗ {E,E;Δ;Γ} ⊨ fill K #() ≤log≤ t: τ) -∗
+    {E,E;Δ;Γ} ⊨ fill K (acquire #lk) ≤log≤ t: τ.
+  Proof.
+    iIntros (?) "#Hlock Hlog".
+    iLöb as "IH".
+    unlock acquire. simpl.
+    rel_rec_l.
+    iDestruct "Hlock" as (l) "[% #?]". simplify_eq.
+    rel_cas_l_atomic.
+    iInv N as (b) "[Hl HR]" "Hclose".
+    iModIntro. iExists _. iFrame.
+    iSplit.
+    - iIntros (?). iNext. iIntros "Hl".
+      assert (b = true) as ->. { destruct b; congruence. }
+      rel_if_l.
+      iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+      by iApply "IH".
+    - iIntros (?). simplify_eq.
+      iNext. iIntros "Hl".
+      rel_if_l.
+      iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+      iDestruct "HR" as "[Hlocked HR]".
+      iApply ("Hlog" with "Hlocked HR").
+  Qed.
+
+End lockG_rules.
+
+Section lock_rules_r.
   Context `{logrelG Σ}.
+
   Variable (E1 E2 : coPset).
   Variable (Δ : list (prodC valC valC -n> iProp Σ)).
 
@@ -67,7 +166,7 @@ Section proof.
     iApply ("Hlog" with "Hl").
   Qed.
 
-  Lemma bin_log_related_newlock_l Γ K t τ :
+  Lemma bin_log_related_newlock_l_simp Γ K t τ :
     (∀ l : loc, l ↦ᵢ #false -∗ {E1,E1;Δ;Γ} ⊨ fill K #l ≤log≤ t : τ) -∗
     {E1,E1;Δ;Γ} ⊨ fill K (newlock #()) ≤log≤ t : τ.
   Proof.
@@ -232,4 +331,4 @@ Section proof.
     iApply ("Hlog" with "HQ Hl").
   Qed.
 
-End proof.
+End lock_rules_r.

theories/examples/various.v

@@ -4,7 +4,7 @@
 *)
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import csum agree excl.
-From iris_logrel Require Import logrel.
+From iris_logrel Require Import logrel examples.lock.
 
 Section refinement.
   Context `{logrelG Σ}.
@@ -207,5 +207,58 @@ Section refinement.
     unlock bot; simpl_subst/=.
     iApply ("IH" with "Hlog").
   Qed.
-        
+
+  (* /Sort of/ a well-bracketedness example.
+     Without locking in the first expression, the callback can reenter
+     the body in a forked thread to change the value of x
+  *)
+  Lemma refinement4  Γ `{!lockG Σ}:
+    Γ ⊨
+      (let: "x" := ref #1 in
+       let: "l" := newlock #() in
+       λ: "f", acquire "l";;
+               "x" <- #0;; "f" #();;
+               "x" <- #1;; "f" #();;
+               let: "v" := !"x" in
+               release "l";; "v")
+    ≤log≤
+      (let: "x" := ref #0 in
+       λ: "f", "f" #();; "x" <- #1;; "f" #();; !"x")
+    : TArrow (TArrow TUnit TUnit) TNat.
+  Proof.
+    iIntros (Δ).
+    rel_alloc_l as x "Hx".
+    rel_alloc_r as y "Hy".
+    rel_let_l; rel_let_r.
+    pose (N:=logrelN.@"lock").
+    rel_apply_l (bin_log_related_newlock_l N (∃ (n m : nat), x ↦ᵢ #n ∗ y ↦ₛ #m)%I with "[Hx Hy]").
+    { iExists _, _. iFrame. }
+    iIntros (l γ) "#Hl".
+    rel_let_l.
+    iApply bin_log_related_arrow_val; auto.
+    iIntros "!#" (f1 f2) "#Hf".
+    rel_let_l. rel_let_r.
+    rel_apply_l (bin_log_related_acquire_l N _ l with "Hl"); auto.
+    iIntros "Hlocked". iDestruct 1 as (n m) "[Hx Hy]".
+    rel_seq_l.
+    rel_store_l. rel_seq_l.
+    iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit with "[Hf]"); auto.
+    { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hf]").
+      iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
+      iApply bin_log_related_unit. }
+    rel_store_l. rel_seq_l.
+    rel_store_r. rel_seq_r.
+    iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit with "[Hf]"); auto.
+    { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hf]").
+      iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
+      iApply bin_log_related_unit. }
+    rel_load_l.
+    rel_let_l.
+    rel_load_r.
+    rel_apply_l (bin_log_related_release_l N _ l γ with "Hl Hlocked [Hx Hy]"); eauto.
+    { iExists _,_. iFrame. }
+    rel_seq_l.
+    rel_vals; eauto.
+  Qed.
+
 End refinement.