Continuation change, extract_proph_winner change

The continuation Q is moved to the top level in the Accepted state.

extract_proph_winner now only considers the first element in the list and does not restrict the first value.

theories/logatom/rdcss/rdcss.v

@@ -34,9 +34,9 @@ Definition new_rdcss : val := λ: "n", ref (InjL "n").
   complete(l_descr, l_n) :=
     let (l_m, m1, n1, n2, p) := !l_descr in
     (* data = (l_m, m1, n1, n2, p) *)
-    let p_ghost = NewProph in
+    let tid_ghost = NewProph in
     let n_new = (if !l_m = m1 then n1 else n2) in
-      Resolve (CmpXchg l_n (InjR l_descr) (ref (InjL n_new))) p p_ghost ; #().
+      Resolve (CmpXchg l_n (InjR l_descr) (ref (InjL n_new))) p tid_ghost ; #().
  *)
 Definition complete : val :=
   λ: "l_descr" "l_n",
@@ -47,9 +47,14 @@ Definition complete : val :=
     let: "n1"  := Snd (Fst (Fst ("data"))) in
     let: "n2"  := Snd (Fst ("data")) in
     let: "p"   := Snd ("data") in
-    let: "p_ghost" := NewProph in
+    (* Create a thread identifier using NewProph.
+       tid_ghost is not used as a traditional prophecy, i.e. it is never resolved.
+       The reason we use NewProph is so that we can use the erasure theorem to argue that
+       it has no effect on the code. 
+    *)
+    let: "tid_ghost" := NewProph in
     let: "n_new" := (if: !"l_m" = "m1" then "n2" else "n1") in
-    Resolve (CmpXchg "l_n" (InjR "l_descr") (InjL "n_new")) "p" "p_ghost" ;; #().
+    Resolve (CmpXchg "l_n" (InjR "l_descr") (InjL "n_new")) "p" "tid_ghost" ;; #().
 
 (*
   get(l_n) :=
@@ -158,7 +163,7 @@ Section rdcss.
 
   Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
     match pvs with
-    | ((_, #true)%V, LitV (LitProphecy p)) :: _  => Some p
+    | ((_, #true)%V, LitV (LitProphecy tid)) :: _  => Some tid
     | _                               => None
     end.
 
@@ -174,0+179,0 @@
 
   Definition own_token γ := (own γ (Excl ()))%I.
 
-  Definition pending_state P (n1 : val) (proph_winner : option proph_id) p_ghost_winner (γ_n γ_a: gname) :=
+  Definition pending_state P (n1 : val) (proph_winner : option proph_id) tid_ghost_winner (γ_n γ_a: gname) :=
     (P ∗
-     ⌜match proph_winner with None => True | Some p => p = p_ghost_winner end⌝ ∗
+     ⌜match proph_winner with None => True | Some p => p = tid_ghost_winner end⌝ ∗
      own γ_n (● Excl' n1) ∗
      own_token γ_a)%I.
 
   (* After the prophecy said we are going to win the race, we commit and run the AU,
      switching from [pending] to [accepted]. *)
-  Definition accepted_state Q (proph_winner : option proph_id) (p_ghost_winner : proph_id) :=
-    ((∃ vs, proph p_ghost_winner vs) ∗
+  Definition accepted_state Q (proph_winner : option proph_id) (tid_ghost_winner : proph_id) :=
+    ((∃ vs, proph tid_ghost_winner vs) ∗
      Q ∗
-     ⌜match proph_winner with None => True | Some p => p = p_ghost_winner end⌝)%I.
+     ⌜match proph_winner with None => True | Some tid => tid = tid_ghost_winner end⌝)%I.
 
   (* The same thread then wins the CmpXchg and moves from [accepted] to [done].
      Then, the [γ_t] token guards the transition to take out [Q].
      Remember that the thread winning the CmpXchg might be just helping.  The token
      is owned by the thread whose request this is.
-     In this state, [p_ghost_winner] serves as a token to make sure that
+     In this state, [tid_ghost_winner] serves as a token to make sure that
      only the CmpXchg winner can transition to here, and owning half of [l_descr] serves as a
      "location" token to ensure there is no ABA going on. Notice how [rdcss_inv]
      owns *more than* half of its [l_descr] in the Updating state,
      which means we know that the [l_descr] there and here cannot be the same. *)
-  Definition done_state Qn (l_descr : loc) (p_ghost_winner : proph_id) (γ_t γ_a: gname) :=
-    ((Qn ∨ own_token γ_t) ∗ (∃ vs, proph p_ghost_winner vs) ∗ (l_descr ↦{1/2} -) ∗ own_token γ_a)%I.
+  Definition done_state Qn (l_descr : loc) (tid_ghost_winner : proph_id) (γ_t γ_a: gname) :=
+    ((Qn ∨ own_token γ_t) ∗ (∃ vs, proph tid_ghost_winner vs) ∗ (l_descr ↦{1/2} -) ∗ own_token γ_a)%I.
 
   (* Invariant expressing the descriptor protocol.
      - We always need the [proph] in here so that failing threads coming late can
@@ -211,12 +216,12 @@ Section rdcss.
                     prophecy resources by only keeping half permission to the prophecy resource
                     in the invariant in [accepted] while the other half would be kept by the CmpXchg winner.
    *)
-  Definition descr_inv P Q (p : proph_id) n (l_n l_descr : loc) (p_ghost_winner : proph_id) γ_n γ_t γ_s γ_a: iProp Σ :=
+  Definition descr_inv P Q (p : proph_id) n (l_n l_descr : loc) (tid_ghost_winner : proph_id) γ_n γ_t γ_s γ_a: iProp Σ :=
     (∃ vs, proph p vs ∗
       (own γ_s (Cinl $ Excl ()) ∗
-       (l_n ↦{1/2} InjRV #l_descr ∗ ( pending_state P n (proph_extract_winner vs) p_ghost_winner γ_n γ_a
-        ∨ accepted_state (Q n) (proph_extract_winner vs) p_ghost_winner ))
-       ∨ own γ_s (Cinr $ to_agree ()) ∗ done_state (Q n) l_descr p_ghost_winner γ_t γ_a))%I.
+       (l_n ↦{1/2} InjRV #l_descr ∗ ( pending_state P n (proph_extract_winner vs) tid_ghost_winner γ_n γ_a
+        ∨ accepted_state (Q n) (proph_extract_winner vs) tid_ghost_winner ))
+       ∨ own γ_s (Cinr $ to_agree ()) ∗ done_state (Q n) l_descr tid_ghost_winner γ_t γ_a))%I.
 
   Local Hint Extern 0 (environments.envs_entails _ (descr_inv _ _ _ _ _ _ _ _ _ _ _)) => unfold descr_inv.
 
@@ -235,9 +240,9 @@ Section rdcss.
               [complete] fails always.*)
            l_n ↦{1/2} (InjLV n) ∗ own γ_n (● Excl' n)
         | Updating l_descr l_m m1 n1 n2 p =>
-           ∃ q P Q p_ghost_winner γ_t γ_s γ_a,
+           ∃ q P Q tid_ghost_winner γ_t γ_s γ_a,
              (* (InjRV #l_descr) = state_to_val (Updating l_descr l_m m1 n1 n2 p) *)
-             (* There are two pieces of per-[descr]-protocol ghost state:
+             (* There are three pieces of per-[descr]-protocol ghost state:
              - [γ_t] is a token owned by whoever created this protocol and used
                to get out the [Q] in the end.
              - [γ_s] reflects whether the protocol is [done] yet or not.
@@ -247,7 +252,7 @@ Section rdcss.
               be the [l_descr] of any [descr] protocol in the [done] state. *)
              ⌜val_is_unboxed m1⌝ ∗
              l_descr ↦{1/2 + q} (#l_m, m1, n1, n2, #p)%V ∗  
-             inv descrN (descr_inv P Q p n1 l_n l_descr p_ghost_winner γ_n γ_t γ_s γ_a) ∗
+             inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost_winner γ_n γ_t γ_s γ_a) ∗
              □ pau P Q γ_n l_m m1 n1 n2 ∗ is_gc_loc l_m
        end)%I.
 
@@ -280,8 +285,8 @@ Section rdcss.
 
   (** Once a [descr] protocol is [done] (as reflected by the [γ_s] token here),
       we can at any later point in time extract the [Q]. *)
-  Lemma state_done_extract_Q P Q p n l_n l_descr p_ghost γ_n γ_t γ_s γ_a :
-    inv descrN (descr_inv P Q p n l_n l_descr p_ghost γ_n γ_t γ_s γ_a) -∗
+  Lemma state_done_extract_Q P Q p n l_n l_descr tid_ghost γ_n γ_t γ_s γ_a :
+    inv descrN (descr_inv P Q p n l_n l_descr tid_ghost γ_n γ_t γ_s γ_a) -∗
     own γ_s (Cinr (to_agree ())) -∗
     □(own_token γ_t ={⊤}=∗ ▷ (Q n)).
   Proof.
@@ -303,13 +308,13 @@ Section rdcss.
 
   (** The part of [complete] for the succeeding thread that moves from [accepted] to [done] state *)
   Lemma complete_succeeding_thread_pending (γ_n γ_t γ_s γ_a: gname) l_n P Q p
-        (n1 n : val) (l_descr : loc) (p_ghost : proph_id) Φ :
+        (n1 n : val) (l_descr : loc) (tid_ghost : proph_id) Φ :
     inv rdcssN (rdcss_inv γ_n l_n) -∗
-    inv descrN (descr_inv P Q p n1 l_n l_descr p_ghost γ_n γ_t γ_s γ_a) -∗
+    inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost γ_n γ_t γ_s γ_a) -∗
     own_token γ_a -∗
     (□(own_token γ_t ={⊤}=∗ ▷ (Q n1)) -∗ Φ #()) -∗
     own γ_n (● Excl' n) -∗
-    WP Resolve (CmpXchg #l_n (InjRV #l_descr) (InjLV n)) #p #p_ghost ;; #() {{ v, Φ v }}.
+    WP Resolve (CmpXchg #l_n (InjRV #l_descr) (InjLV n)) #p #tid_ghost ;; #() {{ v, Φ v }}.
   Proof.
     iIntros "#InvC #InvS Token_a HQ Hn●". wp_bind (Resolve _ _ _)%E.
     iInv rdcssN as (s) "(>Hln & Hrest)".
@@ -331,7 +336,7 @@ Section rdcss.
     { simpl. iDestruct (mapsto_agree with "Hln Hln'") as %Heq. inversion Heq. }
     iDestruct (mapsto_agree with "Hln Hln'") as %[= ->].
     simpl.
-    iDestruct "Hrest" as (q P' Q' p_ghost' γ_t' γ_s' γ_a') "(_ & [>Hld >Hld'] & Hrest)".
+    iDestruct "Hrest" as (q P' Q' tid_ghost' γ_t' γ_s' γ_a') "(_ & [>Hld >Hld'] & Hrest)".
     (* We perform the CmpXchg. *)
     iCombine "Hln Hln'" as "Hln".
     wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_suc.
@@ -352,12 +357,12 @@ Section rdcss.
   Qed.
 
   (** The part of [complete] for the failing thread *)
-  Lemma complete_failing_thread γ_n γ_t γ_s γ_a l_n l_descr P Q p n1 n p_ghost_inv p_ghost Φ :
-    p_ghost_inv ≠ p_ghost →
+  Lemma complete_failing_thread γ_n γ_t γ_s γ_a l_n l_descr P Q p n1 n tid_ghost_inv tid_ghost Φ :
+    tid_ghost_inv ≠ tid_ghost →
     inv rdcssN (rdcss_inv γ_n l_n) -∗
-    inv descrN (descr_inv P Q p n1 l_n l_descr p_ghost_inv γ_n γ_t γ_s γ_a) -∗
+    inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost_inv γ_n γ_t γ_s γ_a) -∗
     (□(own_token γ_t ={⊤}=∗ ▷ (Q n1)) -∗ Φ #()) -∗
-    WP Resolve (CmpXchg #l_n (InjRV #l_descr) (InjLV n)) #p #p_ghost ;; #() {{ v, Φ v }}.
+    WP Resolve (CmpXchg #l_n (InjRV #l_descr) (InjLV n)) #p #tid_ghost ;; #() {{ v, Φ v }}.
   Proof.
     iIntros (Hnl) "#InvC #InvS HQ". wp_bind (Resolve _ _ _)%E.
     iInv rdcssN as (s) "(>Hln & Hrest)".
@@ -393,7 +398,7 @@ Section rdcss.
          of the [rdcss] instance?  Impossible, now we will own more than the whole descriptor location! *)
         iDestruct "Done" as "(_ & _ & >Hld & _)".
         iDestruct "Hld" as (v') "Hld".
-        iDestruct "Hrest" as (q P' Q' p_ghost' γ_t' γ_s' γ_a') "(_ & >[Hld' Hld''] & Hrest)".
+        iDestruct "Hrest" as (q P' Q' tid_ghost' γ_t' γ_s' γ_a') "(_ & >[Hld' Hld''] & Hrest)".
         iDestruct (mapsto_combine with "Hld Hld'") as "[Hld _]".
         rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hld Hld''") as "[]".
       + (* l_descr' ≠ l_descr: The CmpXchg fails. *)
@@ -411,11 +416,11 @@ Section rdcss.
      this request, then you get [Q].  But we also try to complete other
      thread's requests, which is why we cannot ask for the token
      as a precondition. *)
-  Lemma complete_spec (l_n l_m l_descr : loc) (m1 n1 n2 : val) (p : proph_id) γ_n γ_t γ_s γ_a p_ghost_inv P Q q:
+  Lemma complete_spec (l_n l_m l_descr : loc) (m1 n1 n2 : val) (p : proph_id) γ_n γ_t γ_s γ_a tid_ghost_inv P Q q:
     val_is_unboxed m1 →
     N ## gcN → 
     inv rdcssN (rdcss_inv γ_n l_n) -∗
-    inv descrN (descr_inv P Q p n1 l_n l_descr p_ghost_inv γ_n γ_t γ_s γ_a) -∗
+    inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost_inv γ_n γ_t γ_s γ_a) -∗
     □ pau P Q γ_n l_m m1 n1 n2 -∗
     is_gc_loc l_m -∗
     gc_inv -∗
@@ -427,12 +432,12 @@ Section rdcss.
     iModIntro. iIntros (Φ) "Hld HQ".  wp_lam. wp_let.
     wp_bind (! _)%E. wp_load. iClear "Hld". wp_pures.
     wp_apply wp_new_proph; first done.
-    iIntros (vs_ghost p_ghost) "Hp_ghost". wp_pures.
+    iIntros (vs_ghost tid_ghost) "Htid_ghost". wp_pures.
     wp_bind (! _)%E. 
     (* open outer invariant *)
     iInv rdcssN as (s) "(>Hln & Hrest)"=>//.
     (* two different proofs depending on whether we are succeeding thread *)
-    destruct (decide (p_ghost_inv = p_ghost)) as [-> | Hnl].
+    destruct (decide (tid_ghost_inv = tid_ghost)) as [-> | Hnl].
     - (* we are the succeeding thread *)
       (* we need to move from [pending] to [accepted]. *)
       iInv descrN as (vs) "(>Hp & [(>Hs & >Hln' & [Pending | Accepted]) | [#Hs Done]])".
@@ -457,7 +462,7 @@ Section rdcss.
         iMod ("Hclose" with "[Hn◯ Hgc_lm]") as "Q"; first by iFrame.
         iModIntro. iMod "Hgc_close" as "_".
         (* close descr inv *)
-        iModIntro. iSplitL "Q Hp_ghost Hp Hvs Hs Hln'".
+        iModIntro. iSplitL "Q Htid_ghost Hp Hvs Hs Hln'".
         { iModIntro. iNext. iExists _. iFrame "Hp". eauto 12 with iFrame. }
         (* close outer inv *)
         iModIntro. iSplitR "Token_a HQ Hn●".
@@ -470,13 +475,13 @@ Section rdcss.
           iApply (complete_succeeding_thread_pending
                     with "InvC InvS Token_a HQ Hn●").
       + (* Accepted: contradiction *)
-        iDestruct "Accepted" as "[>Hp_ghost_inv _]".
-        iDestruct "Hp_ghost_inv" as (p') "Hp_ghost_inv".
-        by iDestruct (proph_exclusive with "Hp_ghost Hp_ghost_inv") as %?.
+        iDestruct "Accepted" as "[>Htid_ghost_inv _]".
+        iDestruct "Htid_ghost_inv" as (p') "Htid_ghost_inv".
+        by iDestruct (proph_exclusive with "Htid_ghost Htid_ghost_inv") as %?.
       + (* Done: contradiction *)
-        iDestruct "Done" as "[QT >[Hp_ghost_inv _]]".
-        iDestruct "Hp_ghost_inv" as (p') "Hp_ghost_inv".
-        by iDestruct (proph_exclusive with "Hp_ghost Hp_ghost_inv") as %?.
+        iDestruct "Done" as "[QT >[Htid_ghost_inv _]]".
+        iDestruct "Htid_ghost_inv" as (p') "Htid_ghost_inv".
+        by iDestruct (proph_exclusive with "Htid_ghost Htid_ghost_inv") as %?.
     - (* we are the failing thread *)
       (* close invariant *)
       iMod (is_gc_access with "InvGC isGC") as (v) "[Hlm Hclose]"; first solve_ndisj.
@@ -565,7 +570,7 @@ Section rdcss.
       wp_cmpxchg_fail. 
       iModIntro.
       (* extract descr invariant *)
-      iDestruct "Hrest" as (q P Q p_ghost γ_t γ_s γ_a) "(#Hm1'_unbox & [Hld1 [Hld2 Hld3]] & #InvS & #P_AU & #P_GC)".
+      iDestruct "Hrest" as (q P Q tid_ghost γ_t γ_s γ_a) "(#Hm1'_unbox & [Hld1 [Hld2 Hld3]] & #InvS & #P_AU & #P_GC)".
       iDestruct "Hm1'_unbox" as %Hm1'_unbox.
       iSplitR "AU Hld2 Hld Hp".
       (* close invariant, retain some permission to l_descr', so it can be read later *)
@@ -618,7 +623,7 @@ Section rdcss.
         iNext. iExists (Quiescent au_n). iFrame.
       }
       wp_match. iApply "HΦ".
-    - iDestruct "Hrest" as (q P Q p_ghost γ_t γ_s γ_a) "(#Hm1_unbox & [Hld [Hld' Hld'']] & #InvS & #PAU & #GC)".
+    - iDestruct "Hrest" as (q P Q tid_ghost γ_t γ_s γ_a) "(#Hm1_unbox & [Hld [Hld' Hld'']] & #InvS & #PAU & #GC)".
       iDestruct "Hm1_unbox" as %Hm1_unbox.
       iModIntro. iSplitR "AU Hld'". {
         iNext. iExists (Updating l_descr l_m m1 n1 n2 p). eauto 15 with iFrame.