diff --git a/theories/logrel/F_mu_ref_conc/examples/queue/MS_queue.v b/theories/logrel/F_mu_ref_conc/examples/queue/MS_queue.v index c518aa45438333b33f5cbf082a1b3681f2f1d45b..e2279c0fb976256ba80af64c300b7431884d4311 100644 --- a/theories/logrel/F_mu_ref_conc/examples/queue/MS_queue.v +++ b/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. diff --git a/theories/logrel/F_mu_ref_conc/examples/queue/refinement.v b/theories/logrel/F_mu_ref_conc/examples/queue/refinement.v index 284802b8c571086f230a664d898387bc1d667893..3846aec6a27c9b9174f9cba9fca15e788b2c594b 100644 --- a/theories/logrel/F_mu_ref_conc/examples/queue/refinement.v +++ b/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 ι')