Add pseudo code for MS queue and cleanup a few things

theories/logrel/F_mu_ref_conc/examples/queue/MS_queue.v

@@ -13,13 +13,11 @@ Definition TMaybe τ := (TSum TUnit τ).
 Definition none := InjL Unit.
 Definition some v := InjR v.
 
-(* Definition nil := InjL Unit. *)
-(* Definition cons val tail := InjR (Pair val tail). *)
-
 Definition TNodeBody τ v := TMaybe (TProd (TMaybe τ.[ren (+1)]) (Tref (Tref v))).
 Definition TNode τ := TRec (TNodeBody τ (TVar 0)).
 Definition MS_QueueType τ := Tref (Tref (TNode τ)).
 
+(* Get the value of a some and spin it the argument is a none. *)
 Definition getValue (e : expr) : expr :=
   (Case
      e
@@ -27,6 +25,18 @@ Definition getValue (e : expr) : expr :=
      (Var 0)
   ).
 
+(* Pseudo code for dequeue:
+  rec try() =>
+    let n = !head
+        c = getValue (unfold !n)
+    in case unfold !!(snd c) with
+      Nil => none
+      Cons x xs =>
+        if CAS head n !(snd c)
+        then some (getValue x)
+        else (try ())
+*)
+
 Definition MS_dequeue :=
   (Rec (* try(_) *)
      (LetIn
@@ -39,8 +49,7 @@ Definition MS_dequeue :=
               none (* The queue is empty, return none *)
               (* Snd n = InjR n' => *)
               (If
-                 (CAS (Var 5 (* head *)) (Var 2 (* n *)) (Load (Snd (Var 1 (* n' *)))))
-                 (* (CAS (Var 5 (* head *)) (Var 2 (* n *)) (Var 0 (* n' *))) *)
+                 (CAS (Var 5 (* head *)) (Var 2 (* n *)) (Load (Snd (Var 1 (* c *)))))
                  (some (getValue (Fst (Var 0 (* n' *)))))
                  (App (Var 3 (* try *)) Unit)
               )
@@ -49,6 +58,22 @@ Definition MS_dequeue :=
      )
   ).
 
+(* Pseudo code for enqueue:
+  fun x =>
+    let n = alloc (fold (some (some x), (alloc (alloc (fold none))))))
+    in
+      (rec try(c) =>
+        let t = !c
+        in case (unfold !t) with
+            Left _ => if CAS c t n
+                      then ()
+                      else try(c)
+            Right c' =>
+              try (snd c')
+      )
+      (snd (getValue (unfold !!head)))
+*)
+
 Definition MS_enqueue :=
   (Lam (* x. *)
      (LetIn
@@ -58,7 +83,7 @@ Definition MS_enqueue :=
               (LetIn
                  (* t = *) (Load (Var 1 (* c *)))
                  (Case
-                    (Unfold (Load (Var 0 (* t' *))))
+                    (Unfold (Load (Var 0 (* t *))))
                     (* c = InjL ... Tail is nil, we can try to insert now *)
                     (If
                        (CAS (Var 3 (* c *)) (Var 1 (* t *)) (Var 4 (* n *)))
@@ -165,19 +190,4 @@ Section MS_queue.
       + apply MS_enqueue_type.
   Qed.
 
-  Definition program : expr :=
-    LetIn
-      (* lock = *) (App MS_queue Unit)
-      (Seq
-         (App (Snd (Var 0)) (#n 3))
-         (App (Fst (Var 0)) Unit)
-      ).
-
-  (* Lemma MS_queue_test : WP program {{ v, ⌜v = #nv 3⌝ }}%I. *)
-  (* Proof. *)
-  (*   rewrite /program. *)
-  (*   iApply (wp_bind (fill [LetInCtx _])). *)
-  (*   iApply wp_pure_step_later; auto. iNext. *)
-  (* Admitted. *)
-
 End MS_queue.

theories/logrel/F_mu_ref_conc/examples/queue/refinement.v

@@ -8,11 +8,13 @@ From iris_examples.logrel.F_mu_ref_conc.examples.queue Require Import
 
 From iris.proofmode Require Import tactics.
 
+Definition locO := leibnizO loc.
+
 Definition queueN : namespace := nroot .@ "queue".
 Definition nodeN : namespace := nroot .@ "node".
 Definition sentinelN : namespace := nroot .@ "sentinel".
 
-Definition fracAgreeR : cmraT := prodR fracR (agreeR (leibnizO loc)).
+Definition fracAgreeR : cmraT := prodR fracR (agreeR locO).
 Definition exlTokR : cmraT := exclR (unitR).
 
 Section Queue_refinement.
@@ -57,8 +59,6 @@ Section Queue_refinement.
     by apply cmra_update_exclusive.
   Qed.
 
-  Definition locO := leibnizO loc. (* FIXME: This should be included in Iris? *)
-
   Program Definition nodeInv_pre γ : (locO -n> iPropO Σ) -n> (locO -n> iPropO Σ) :=
     λne P ℓ,
       (∃ ℓ2 q,
@@ -308,7 +308,7 @@ Section Queue_refinement.
     iModIntro. iFrame.
   Qed.
 
-  (* If you have the token and the nodeList and a cas *)
+  (* With the token and the nodeList one can perform a CAS on the last node. *)
   Lemma enqueue_cas E γ xs x ℓ ℓ2 ℓhdPt ℓnil ℓtail ℓnode :
     {{{
       ℓnil ↦ᵢ FoldV (InjLV UnitV) ∗
@@ -367,7 +367,6 @@ Section Queue_refinement.
     iIntros (j K) "Hj".
     iApply wp_value.
     iExists (TLamV _). iFrame "Hj". clear j K.
-    (* unfold interp. unfold interp_forall. *)
     iAlways. iIntros (τi) "%". iIntros (j K) "Hj /=".
     iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
     iMod (steps_newlock _ j (LetInCtx _ :: K) with "[$Hj]")
@@ -527,14 +526,11 @@ Section Queue_refinement.
         iLeft. iExists (_, _). simpl. done.
       + (* xs is not the empty list *)
         iDestruct "Right" as (x next) "(>[hdPtPts hdPtPts'] & >[otherPts otherPts'] & nodeInvNext)".
-        (* iDestruct "first" as (ℓhd next q0) "(hdPts & hdPts' & Hnodes)". *)
         iApply (wp_load with "[$hdPtPts]"). iNext. iIntros "hdPts".
         simpl.
         iMod ("closeNodeInv" with "[hdPtPts' otherPts' nodeInvNext]").
         { iNext. iExists _, _. iRight. iExists _, _. iFrame. }
         iModIntro.
-        (* destruct xsₛ as [|xₛ xsₛ'].
-        { inversion H3. } *)
         iApply (wp_load with "[$otherPts]"). iNext. iIntros "otherPts'".
         simpl.
         iApply wp_pure_step_later; auto. iNext.
@@ -548,7 +544,6 @@ Section Queue_refinement.
         iApply wp_value. simpl.
         iApply (wp_load with "hdPts"). iNext. iIntros "hdPts".
         simpl.
-        (* rename ℓq into ℓq'. *)
         iInv queueN as (ℓ'2 xs2 xsₛ2) "(isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
         rewrite /isMSQueue.
         iDestruct "isMSQ" as (ℓsentinel2 v2 ℓhdPt2 q2 ι')