Finish dequeue non-empty case when CAS succeeds

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

@@ -34,14 +34,14 @@ Definition MS_dequeue :=
         (LetIn
            (* c = *) (getValue (Unfold (Load ((Var 0 (* n *))))))
            (Case
-              (Unfold (Load (Load (Snd (Var 0 (* n *)))))) (* Get next node after sentinel *)
+              (Unfold (Load (Load (Snd (Var 0 (* c *)))))) (* Get next node after sentinel *)
               (* Snd n = InjL Unit => *)
               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' *))) *)
-                 (some (getValue (Fst (Var 1 (* n *)))))
+                 (some (getValue (Fst (Var 0 (* n' *)))))
                  (App (Var 3 (* try *)) Unit)
               )
            )

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

@@ -23,7 +23,7 @@ Section Queue_refinement.
         ⌜n = LocV ℓ⌝ ∗ ℓ ↦ᵢ{q} (FoldV v)
                   ∗ (⌜v = noneV⌝
                      ∨ (∃ (n' : valO) ℓtail,
-                           ⌜v = someV (PairV v (LocV ℓtail))⌝ ∗ ℓtail ↦ᵢ n' ∗ ▷ (P n'))
+                           ⌜v = someV (PairV (InjRV v) (LocV ℓtail))⌝ ∗ ℓtail ↦ᵢ n' ∗ ▷ (P n'))
     ))%I.
   Solve Obligations with solve_proper.
 
@@ -33,12 +33,15 @@ Section Queue_refinement.
 
   Definition nodeInv : valO -n> iPropO Σ := fixpoint (nodeInv_pre).
 
-  Definition isStackList (ℓ : loc) (xs : list val) : iProp Σ :=
+  Fixpoint isCGQueue_go (xs : list val) : val :=
     match xs with
-    | nil => ℓ ↦ₛ FoldV noneV
-    | x :: xs' => True (* FIXME *)
+    | nil => FoldV noneV
+    | x :: xs' => FoldV (InjRV (PairV x (isCGQueue_go xs')))
     end.
 
+  Definition isCGQueue (ℓ : loc) (xs : list val) : iProp Σ :=
+    ℓ ↦ₛ (isCGQueue_go xs).
+
   (* Represents the information that the location ℓ points to a series of nodes
      correscponding to the list `xs`.
    *)
@@ -47,21 +50,22 @@ Section Queue_refinement.
     | nil => ℓ ↦ᵢ FoldV noneV
     | x :: xs' =>
       (∃ ℓtail ℓnext,
-          ℓ ↦ᵢ{q} FoldV (someV (PairV x (LocV ℓtail)))
+          ℓ ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV ℓtail)))
             ∗ ℓtail ↦ᵢ{q} (LocV ℓnext)
             ∗ isNodeList q ℓnext xs')
     end.
 
   (* Represents that the location ℓ points to a series of nodes corresponding to
      the list `xs` _and potentially more nodes_. The difference between this and
-     isStackList is that this predicates does not say exactly what the end, i.e.
-     the final node, is because this may change. *)
+     isNodeList is that this predicates does not say exactly what the end is,
+     i.e. the final node, is because this may change. Loosely speaking this
+     represent the persistent information in isNodeList. *)
   Fixpoint firstXsValues q (ℓ : loc) (xs : list val) : iProp Σ :=
     match xs with
     | nil => True (* Here we should be able to say that ℓ is either another node or the end. *)
     | x :: xs' =>
       (∃ ℓtail ℓnext,
-          ℓ ↦ᵢ{q} FoldV (someV (PairV x (LocV ℓtail)))
+          ℓ ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV ℓtail)))
             ∗ ℓtail ↦ᵢ{q} (LocV ℓnext)
             ∗ firstXsValues q ℓnext xs')
     end.
@@ -85,7 +89,7 @@ Section Queue_refinement.
           ∗ ℓhdPt ↦ᵢ{q} (LocV ℓhd)
           ∗ isNodeList p ℓhd xsᵢ)%I.
 
-  (* Definition isStackList (τi : D) (ℓ : loc) (xs : list val) (xs' : list val) : iProp Σ := *)
+  (* Definition isCGQueue (τi : D) (ℓ : loc) (xs : list val) (xs' : list val) : iProp Σ := *)
   (*   (⌜True⌝)%I. *)
 
   Fixpoint xsLink (τi : D) (xsᵢ xsₛ : list val) : iProp Σ :=
@@ -98,12 +102,45 @@ Section Queue_refinement.
   Definition invariant τi hd sHd ℓlock: iProp Σ :=
     (∃ ℓhd ℓ' xsᵢ xsₛ,
         ⌜hd = Loc ℓhd⌝ ∗ isMSQueue τi ℓhd xsᵢ
-                  ∗ ⌜sHd = Loc ℓ'⌝ ∗ isStackList ℓ' xsₛ
+                  ∗ ⌜sHd = Loc ℓ'⌝ ∗ isCGQueue ℓ' xsₛ
                                ∗ ℓlock ↦ₛ (#♭v false)
                                ∗ xsLink τi xsᵢ xsₛ
                                ∗ ⌜length xsᵢ = length xsₛ⌝
     )%I.
 
+  Lemma steps_CG_dequeue_cons E j K x xs ℓ ℓlock :
+    nclose specN ⊆ E →
+    spec_ctx ∗ j ⤇ fill K (App (CG_dequeue (Loc ℓ) (Loc ℓlock)) Unit)
+             ∗ isCGQueue ℓ (x :: xs)
+             ∗ ℓlock ↦ₛ (#♭v false)
+             ⊢ |={E}=> j ⤇ fill K (InjR (of_val x))
+                         ∗ isCGQueue ℓ (xs)
+                         ∗ ℓlock ↦ₛ (#♭v false).
+  Proof.
+    iIntros (HNE) "(#spec & Hj & isQueue & lofal)".
+    rewrite /isCGQueue /CG_dequeue. simpl.
+    iMod (steps_with_lock _ _ _ _ _ (ℓ ↦ₛ FoldV (InjRV (PairV x _)))%I
+                          _ (InjRV x) UnitV
+            with "[$Hj $isQueue $lofal]") as "Hj"; eauto.
+    iIntros (K') "(#Hspec & isQueue & Hj)".
+    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
+    iMod (step_load _ _ (UnfoldCtx :: CaseCtx _ _ :: K')  with "[Hj $isQueue]")
+      as "[Hj isQueue]"; eauto.
+    simpl.
+    iMod (do_step_pure _ _ (CaseCtx _ _ :: K') with "[$Hj]") as "Hj"; eauto.
+    simpl.
+    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
+    simpl.
+    iMod (do_step_pure _ _ (StoreRCtx (LocV _) :: SeqCtx _ :: K') with "[$Hj]") as "Hj"; eauto.
+    simpl.
+    iMod (step_store _ _ (SeqCtx _ :: K') with "[$Hj $isQueue]") as "[Hj isQueue]"; eauto.
+    { rewrite /= !to_of_val //. }
+    simpl.
+    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
+    iMod (do_step_pure _ _ (InjRCtx :: K') with "[$Hj]") as "Hj"; eauto.
+    iModIntro. iFrame.
+  Qed.
+
   Lemma MS_CG_counter_refinement :
     [] ⊨ MS_queue ≤log≤ CG_queue :
       (TForall (TProd
@@ -245,7 +282,7 @@ Section Queue_refinement.
         iApply (wp_load with "hdPts"). iNext. iIntros "hdPts".
         simpl.
         rename ℓq into ℓq'.
-        iInv queueN as (ℓq ℓ'2 xs2 xs'2) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
+        iInv queueN as (ℓq ℓ'2 xs2 xsₛ2) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
         (* clear. *)
         iDestruct "isMSQ" as (ℓsentinel2 v2 ℓhdPt2 ℓhd2 q2 p2)
                                "(qPts & sentinelPts' & hdPts2 & isNodeList)".
@@ -268,23 +305,46 @@ Section Queue_refinement.
           with the same element. *)
           destruct xs2 as [|x2' xs2']; simpl.
           { iDestruct (mapsto_agree with "isNodeList hdPts'") as %[=->]. }
-          iDestruct "isNodeList" as (ℓtail ℓnext) "[hdPts'' isNodeList']".
+          destruct xsₛ2 as [|xₛ2' xsₛ2']; simpl.
+          { inversion H4. }
+          iDestruct "isNodeList" as (ℓtail ℓnext) "[hdPts'' isNodeList]".
           iAssert (⌜x = x2'⌝)%I as %<-.
           { iDestruct (mapsto_agree with "hdPts' hdPts''") as %[=<-]. done. }
-          (* We must now reestablish the invariant. *)
-          iMod ("Hclose" with "[qPts lofal Hlink Hsq isNodeList']") as "_".
+          iDestruct "Hlink" as "[Hτi Hlink]".
+          (* We step through the specificaion code. *)
+          iMod (steps_CG_dequeue_cons with "[$Hspec $Hj $Hsq $lofal]") as "(Hj & Hsq & lofal)".
+          { solve_ndisj. }
+          (* FIXME: I think the brackets can be removed here. *)
+          (* We are now ready to reestablish the invariant. *)
+          iMod ("Hclose" with "[qPts lofal Hlink Hsq isNodeList hdPts'']") as "_".
           { iNext.
             rewrite /invariant.
-            iExists _, _, xs', xsₛ'.
+            iExists _, _, xs2', xsₛ2'.
             iFrame.
             iSplit; auto.
+            iSplitL "qPts hdPts'' isNodeList".
+            { iExists _, _, _ ,_, _, _.
+              iFrame. }
             iSplit; auto.
-            rewrite /isMSQueue.
-            iExists _, _, _ ,_, _, _.
-            iFrame.
           }
-        *
-          iApply (wp_load with "qPts"). iNext. iIntros "qPts".
+          (* Step over the remainder of the code. *)
+          iModIntro. simpl.
+          iApply wp_pure_step_later; auto. iNext.
+          iApply (wp_bind (fill [CaseCtx _ _; InjRCtx])).
+          iApply wp_pure_step_later; auto. iNext.
+          iApply wp_value. simpl.
+          iApply (wp_bind (fill [InjRCtx])).
+          iApply wp_pure_step_later; auto. iNext. simpl.
+          iApply wp_value.
+          iApply wp_value.
+          iExists (InjRV _).
+          iFrame.
+          iRight.
+          iExists (_, _).
+          iFrame.
+          auto.
+        * (* The queue no longer points to the same sentinel *)
+          (* iApply (wp_load with "qPts"). iNext. iIntros "qPts". *)
           admit.
     - (* enqueue *)
       iIntros ([v1 v2]) "!> #Hrel".