More logical atomicity for the ticket lock

- relational specifications for weak increment
- logically atomic specification for `ticket_lock.acquire`

theories/examples/ticket_lock.v

@@ -16,8 +16,9 @@ Definition acquire : val := λ: "lk",
   let: "n" := FG_increment (Snd "lk") #() in
   wait_loop "n" "lk".
 
-Definition release : val :=
-  λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
+Definition wkincr : val := λ: "l",
+  "l" <- !"l" + #1.
+Definition release : val := λ: "lk", wkincr (Fst "lk").
 
 Definition LockType : type := ref TNat × ref TNat.
 
@@ -40,7 +41,7 @@ Qed.
 Hint Resolve acquire_type : typeable.
 
 Lemma release_type Γ : typed Γ release (LockType → TUnit).
-Proof. solve_typed. Qed.
+Proof. unlock release wkincr. solve_typed. Qed.
 
 Hint Resolve release_type : typeable.
 
@@ -221,7 +222,7 @@ Section refinement.
   Instance lockInt_persistent γp ww : Persistent (lockInt γp ww).
   Proof. apply _. Qed.
 
-  (** * Refinement proofs *)  
+  (** * Refinement proofs *)
   Definition N := logrelN.@"locked".
 
   Local Ltac openI N := iInv N as (P) ">[HP HPinv]" "Hcl".
@@ -296,9 +297,110 @@ Section refinement.
       unlock wait_loop. simpl_subst/=. by iApply "IH".
   Qed.
 
+  (** Logically atomic spec for `acquire`.
+      Parameter type: nat
+      Precondition:
+        λo, ∃ n, lo ↦ᵢ o ∗ ln ↦ᵢ n ∗ issuedTickets γ n
+      Postcondition:
+        λo, ∃ n, lo ↦ᵢ o ∗ ln ↦ᵢ n ∗ issuedTickets γ n ∗ ticket γ o *)
+  Lemma acquire_l_logatomic R P γ Δ Γ E1 E2 K lo ln t τ :
+    P -∗
+    □ (|={E1,E2}=> ∃ o n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ R o ∗
+       ((∃ o n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ R o) ={E2,E1}=∗ True) ∧
+        (∀ o n : nat, lo ↦ᵢ #o ∗ ln ↦ᵢ #n ∗ issuedTickets γ n ∗ ticket γ o ∗ R o -∗ P -∗
+            {E2,E1;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ))
+    -∗ ({E1;Δ;Γ} ⊨ fill K (acquire (#lo, #ln)) ≤log≤ t : τ).
+  Proof.
+    iIntros "HP #H".
+    rewrite /acquire. unlock. simpl.
+    rel_rec_l. rel_proj_l.
+    rel_bind_l ((FG_increment #ln) #())%E.
+    rel_rec_l.
+    rel_apply_l (bin_log_FG_increment_logatomic _ (fun n : nat => ∃ o : nat, lo ↦ᵢ #o ∗ issuedTickets γ n ∗ R o)%I P%I with "HP").
+    iAlways.
+    iPoseProof "H" as "H2".
+    iMod "H" as (o n) "(Hlo & Hln & Hissued & HR & Hrest)". iModIntro.
+    iExists _; iFrame.
+    iSplitL "Hlo HR".
+    { iExists _. iFrame. }
+    iSplit.
+    - iDestruct "Hrest" as "[H _]".
+      iDestruct 1 as (n') "[Hln Ho]".
+      iDestruct "Ho" as (o') "[Ho HR]".
+      iApply "H".
+      iExists _, _. iFrame.
+    - iDestruct "Hrest" as "[H _]".
+      iIntros (n') "[Hln Ho] HP".
+      iDestruct "Ho" as (o') "[Ho [Hissued HR]]".
+      iMod (issueNewTicket with "Hissued") as "[Hissued Hm]".
+      iMod ("H" with "[-HP Hm]") as "_".
+      { iExists _,_. iFrame. }
+      rel_let_l. clear o n o'.
+      rel_rec_l.
+      iLöb as "IH".
+      unlock wait_loop. simpl.
+      rel_rec_l. rel_proj_l.
+      rel_load_l_atomic.
+      iMod "H2" as (o n) "(Hlo & Hln & Hissued & HR & Hrest)". iModIntro.
+      iExists _. iFrame. iNext. iIntros "Hlo".
+      rel_op_l.
+      case_decide; subst; rel_if_l.
+      (* Whether the ticket is called out *)
+      + iDestruct "Hrest" as "[_ H]".
+        iApply ("H" with "[-HP] HP").
+        { iFrame. }
+      + iDestruct "Hrest" as "[H _]".
+        iMod ("H" with "[-HP Hm]") as "_".
+        { iExists _,_; iFrame. }
+        rel_rec_l. iApply ("IH" with "HP Hm").
+  Qed.
+
   Lemma acquire_refinement Δ Γ γp :
     inv N (moduleInv γp) -∗
     {(lockInt γp :: Δ); ⤉Γ} ⊨ acquire ≤log≤ lock.acquire : (TVar 0 → Unit).
+  Proof.
+    iIntros "#Hinv".
+    iApply bin_log_related_arrow_val; eauto.
+    { by unlock acquire. }
+    { by unlock lock.acquire. }
+    iAlways. iIntros (? ?) "/= #Hl".
+    iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq/=.
+    rel_apply_l (acquire_l_logatomic
+                   (fun o => ∃ (b : bool),
+                             l' ↦ₛ #b ∗
+                             if b then ticket γ o else True)%I
+                   True%I γ); first done.
+    iAlways.
+    openI N.
+    iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)".
+    rewrite {1}/lockInv.
+    iDestruct "Hls" as (o n b) "(Hlo & Hln & Hissued & Hl' & Hticket)".
+    iModIntro. iExists _,_; iFrame.
+    iSplitL "Hticket Hl'".
+    { iExists _. iFrame. }
+    clear b o n.
+    iSplit.
+    - iDestruct 1 as (o' n') "(Hlo & Hln & Hissued & Hrest)".
+      iDestruct "Hrest" as (b) "[Hl' Ht]".
+      iApply ("Hcl" with "[-]").
+      iNext. iExists P; iFrame.
+      iApply "HPinv". iExists _,_,_. by iFrame.
+    - iIntros (o n) "(Hlo & Hln & Hissued & Ht & Hrest) _".
+      iDestruct "Hrest" as (b) "[Hl' Ht']".
+      destruct b.
+      { iDestruct (ticket_nondup with "Ht Ht'") as %[]. }
+      rel_apply_r (bin_log_related_acquire_r with "Hl'").
+      { solve_ndisj. }
+      iIntros "Hl'".
+      iMod ("Hcl" with "[-]") as "_".
+      { iNext. iExists P; iFrame.
+        iApply "HPinv". iExists _,_,_; by iFrame. }
+      iApply bin_log_related_unit.
+  Qed.
+
+  Lemma acquire_refinement_direct Δ Γ γp :
+    inv N (moduleInv γp) -∗
+    {(lockInt γp :: Δ); ⤉Γ} ⊨ acquire ≤log≤ lock.acquire : (TVar 0 → Unit).
   Proof.
     iIntros "#Hinv".
     unlock acquire; simpl.
@@ -332,6 +434,48 @@ Section refinement.
   Qed.
 
   (* Releasing the lock *)
+  Lemma wkincr_l x (n : nat) Δ Γ E K t τ :
+    x ↦ᵢ #n -∗
+    (x ↦ᵢ #(n+1) -∗ {E;Δ;Γ} ⊨ fill K Unit ≤log≤ t : τ) -∗
+    ({E;Δ;Γ} ⊨ fill K (wkincr #x) ≤log≤ t : τ).
+  Proof.
+    iIntros "Hx Hlog".
+    unlock wkincr. rel_rec_l.
+    rel_load_l. rel_op_l. rel_store_l.
+    by iApply "Hlog".
+  Qed.
+
+  (* Logically atomic specification for wkincr,
+     cf wkIncr specification from (da Rocha Pinto, Dinsdale-Young, Gardner)
+     Parameter type: nat
+     Precondition: λn, x ↦ᵢ n
+     Postcondition λ_, ∃ n, x ↦ᵢ n
+ *)
+  Lemma wkincr_atomic_l R1 R2 Δ Γ E1 E2 K x t τ  :
+    R2 -∗
+    □ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R1 n ∗
+       ((∃ n : nat, x ↦ᵢ #n ∗ R1 n) ={E2,E1}=∗ True) ∧
+        (∀ m, (∃ n : nat, x ↦ᵢ #n) ∗ R1 m -∗ R2 -∗
+            {E2,E1;Δ;Γ} ⊨ fill K Unit ≤log≤ t : τ))
+    -∗ ({E1;Δ;Γ} ⊨ fill K (wkincr #x) ≤log≤ t : τ).
+  Proof.
+    iIntros "HR2 #H".
+    unlock wkincr.
+    rel_rec_l.
+    iPoseProof "H" as "H2".
+    rel_load_l_atomic.
+    iMod "H" as (n) "[Hx [HR1 [Hrev _]]]". iModIntro.
+    iExists _; iFrame. iNext. iIntros "Hx".
+    iMod ("Hrev" with "[HR1 Hx]") as "_"; simpl.
+    { iExists _. iFrame. }
+    rel_op_l.
+    rel_store_l_atomic.
+    iMod "H2" as (m) "[Hx [HR1 [_ Hmod]]]". iModIntro.
+    iExists _; iFrame. iNext. iIntros "Hx".
+    iApply ("Hmod" with "[$HR1 Hx] HR2").
+    iExists _; iFrame.
+  Qed.
+
   Lemma release_refinement Δ Γ γp :
     inv N (moduleInv γp) -∗
     {(lockInt γp :: Δ); ⤉Γ} ⊨ release ≤log≤ lock.release : (TVar 0 → Unit).
@@ -342,33 +486,36 @@ Section refinement.
     { by unlock lock.release. }
     iAlways. iIntros (? ?) "/= #Hl".
     iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq.
-    rel_let_l. repeat rel_proj_l.
-    rel_load_l_atomic.
-    openI N.
-    iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)".
-    rewrite {1}/lockInv.
-    iDestruct "Hls" as (o n b) "(Hlo & Hln & Hissued & Hl' & Hticket)".
-    iModIntro. iExists _; iFrame.
-    iNext. iIntros "Hlo".
-    iMod ("Hcl" with "[-]") as "_".
-    { iNext. iExists P; iFrame.
-      iApply "HPinv". iExists _,_,_; by iFrame. }
-    rel_op_l.
-    rel_store_l_atomic. clear n b P.
+    rel_let_l. rel_proj_l.
+    pose (R := fun (o : nat) =>
+                 (∃ (n : nat) (b : bool), ln ↦ᵢ #n
+                 ∗ issuedTickets γ n ∗ l' ↦ₛ #b
+                 ∗ if b then ticket γ o else True)%I).
+    rel_apply_l (wkincr_atomic_l R True%I); first done.
+    iAlways.
     openI N.
     iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)".
     rewrite {1}/lockInv.
-    iDestruct "Hls" as (o' n b) "(Hlo & Hln & Hissued & Hl' & Hticket)".
+    iDestruct "Hls" as (o n b) "(Hlo & Hrest)".
     iModIntro. iExists _; iFrame.
-    iNext. iIntros "Hlo".
-
-    rel_apply_r (bin_log_related_release_r with "Hl'").
-    { solve_ndisj. }
-    iIntros "Hl'".
-    iMod ("Hcl" with "[-]") as "_".
-    { iNext. iExists P; iFrame.
-      iApply "HPinv". iExists _,_,_. by iFrame. }
-    iApply bin_log_related_unit.
+    rewrite {1}/R. iSplitL "Hrest".
+    { iExists _,_; iFrame. } clear o n b.
+    iSplit.
+    - iDestruct 1 as (o) "[Hlo HR]".
+      unfold R. iDestruct "HR" as (n b) "HR".
+      iApply "Hcl".
+      iNext. iExists P; iFrame.
+      iApply "HPinv". iExists _,_,_; by iFrame.
+    - iIntros (?) "[Hlo HR] _".
+      iDestruct "Hlo" as (o) "Hlo".
+      unfold R. iDestruct "HR" as (n b) "(Hln & Hissued & Hl' & Hticket)".
+      rel_apply_r (bin_log_related_release_r with "Hl'").
+      { solve_ndisj. }
+      iIntros "Hl'".
+      iMod ("Hcl" with "[-]") as "_".
+      { iNext. iExists P; iFrame.
+        iApply "HPinv". iExists _,_,_. by iFrame. }
+      iApply bin_log_related_unit.
   Qed.
 
   Lemma ticket_lock_refinement Γ :