diff --git a/_CoqProject b/_CoqProject
index c03b2e2b60c556cb12f90154d5edf63677a55baa..40b8f4c2427315a9c93ef79f8e2293e301700f56 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -66,6 +66,7 @@ theories/typing/lib/refcell/ref.v
theories/typing/lib/rwlock/rwlock.v
theories/typing/lib/rwlock/rwlockreadguard.v
theories/typing/lib/rwlock/rwlockwriteguard.v
+theories/typing/lib/rwlock/rwlock_code.v
theories/typing/examples/get_x.v
theories/typing/examples/rebor.v
theories/typing/examples/unbox.v
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 1f3d82f33571f3890fef68c3d4b542cc18e537ac..145efd265caf5bd351e3bc8428b1733fb38be2ed 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -142,6 +142,21 @@ Section rwlock_inv.
apply Qcplus_le_mono_r, Qp_ge_0.
Qed.
+ Lemma rwown_update_write γs :
+ let st' : rwlock_st := Some (inl ()) in
+ rwown γs (main_st None) -∗ rwown γs (sub_st None)
+ ==∗ rwown γs (main_st st') ∗ rwown γs (sub_st st') ∗ rwown γs writing_st.
+ Proof.
+ iIntros (st') "m s".
+ rewrite bi.sep_assoc -rwown_st_global_main_sub -embed_sep -own_op pair_op right_id.
+ iDestruct (rwown_st_global_main_sub with "[$m $s]") as "ms".
+ iMod (own_update (A:=rwlockR) with "ms") as "$"; [|done].
+ apply prod_update; simpl; [|by apply rwown_agree_update].
+ apply auth_update_alloc.
+ rewrite (_: Some (Cinl (Excl ())) = Some (Cinl (Excl ())) ⋅ ε);
+ [by apply op_local_update_discrete|by rewrite right_id_L].
+ Qed.
+
(* GPS protocol definitions *)
Definition rwlock_interp
(γs: gname) (α : lft) (tyO: vProp) (tyS: lft → vProp)
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 844b24f17cc8fa22e377a576c30f1f88c40cee09..da353f3f4394408c0166dff6294a6cd830d40d12 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -8,6 +8,20 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwritegu
From gpfsl.gps Require Import middleware.
Set Default Proof Using "Type".
+(** SYNCHRONIZATION CONDITIONS of rwlock *)
+(* ---> stands for Release-Acquire synchronization.
+ write_unlock ---> read_lock
+ read_unlock ---> read_lock
+ read_unlock ---> write_lock
+
+ This leads to the following C11 implementation:
+ - write_unlock uses a release write
+ - read_lock uses an acquire CAS
+ - write_lock uses an acquire CAS
+ - read_unlock uses a release CAS
+ TODO: check if read_unlock can be a relaxed CAS, due to the release sequence
+ or read-only accesses? *)
+
Section rwlock_functions.
Context `{typeG Σ, rwlockG Σ}.
@@ -332,37 +346,75 @@ Section rwlock_functions.
iIntros (x' tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
- iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
+ iDestruct "Hx'" as (β) "#[Hαβ Hinv]".
+ iDestruct "Hinv" as (γ γs tyO tyS) "((EqO & EqS & PP) & Hinv)".
+ iDestruct "PP" as (vP) "PP".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". done.
- wp_bind (CAS _ _ _).
- iMod (at_bor_acc_tok with "LFT Hinv Hβtok") as "[INV Hclose'']"; try done.
- iDestruct "INV" as (st) "(Hlx & >Hownst & Hst)". destruct st.
- - iApply (wp_cas_int_fail with "Hlx"). by destruct c as [|[[]]|].
- iNext. iIntros "Hlx".
- iMod ("Hclose''" with "[Hlx Hownst Hst]") as "Hβtok"; first by iExists _; iFrame.
+ wp_bind (CAS _ _ _ _ _ _).
+ iMod (at_bor_acc with "LFT Hinv Hβtok") as (Vb) "[INV Hclose'']"; try done.
+ iDestruct (rwlock_proto_inv_split with "INV") as "[mst INV]".
+ iDestruct (bi.later_exist_2 with "mst") as ">mst".
+ set Q : () → vProp Σ :=
+ (λ _, (∃ st, rwown γs (main_st st) ∗ rwown γs (sub_st st)) ∗
+ &{β}tyO ∗ rwown γs writing_st)%I.
+ set R : () → lit → vProp Σ := (λ _ _, True)%I.
+ set P : vProp Σ := ((∃ st, rwown γs (main_st st)))%I.
+ iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
+ iApply (GPS_PPRaw_CAS_int_simple (rwlock_interp γs β tyO tyS) _ _ _ _ _
+ 0 #(-1) () P Q R _ _ Vb with "[$PP $INV mst rTrue]");
+ [solve_ndisj|by left|done|by right|by left|iSplitL ""; last iSplitL ""|..].
+ { iIntros "!> !>" (???). by iApply rwlock_interp_comparable. }
+ { iIntros "!> !>" (???). by iApply rwlock_interp_duplicable. }
+ { simpl. iSplitL ""; last first.
+ { rewrite -{2}(bi.True_sep' P).
+ iApply (rel_sep_objectively with "[$rTrue mst]"). iModIntro. by iFrame. }
+ iNext. rewrite -(bi.True_sep' (∀ _ : (), _)%I).
+ iApply (rel_sep_objectively with "[$rTrue]"). iModIntro.
+ iIntros ([] _). iSplit; [|by iIntros (?) "_ _"].
+ iDestruct 1 as (st) "mst".
+ iDestruct 1 as (st') "[Eqst INT]". iDestruct "Eqst" as %Eqst.
+ destruct st' as [[[]|[[ν q] n]]|]; [by inversion Eqst..|].
+ iDestruct "INT" as "[sst Hst]".
+ iDestruct 1 as (?) "[_ #Share]". iExists (). iSplitL ""; [done|].
+ iDestruct (rwown_main_sub_agree with "mst sst") as %Eqst2. subst st.
+ set st': rwlock_st := Some (inl ()).
+ iMod (rwown_update_write γs with "mst sst") as "(mst'&sst'&wst)".
+ iModIntro. iFrame "Hst wst". iSplitR ""; [iExists _; by iFrame|].
+ iSplitL ""; iExists st'; [done|by iFrame "Share"]. }
+
+ iNext. simpl.
+ iIntros (b v' [])
+ "(INV & _ &[([%%] & _ & mst & Hβ & wst) | ([% Neq] & _ & _ & P)])".
+ - subst b v'. iDestruct "mst" as (st2) "[mst sst]".
+ iMod ("Hclose''" with "[mst INV]") as "Hβtok".
+ { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists st2. }
iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iModIntro. wp_case.
- iApply (type_type _ _ _
- [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]
- with "[] LFT HE Hna HL Hk"); first last.
- { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
- iApply (type_sum_unit (option $ rwlockwriteguard α ty));
- [solve_typing..|]; first last.
- rewrite /option /=. iApply type_jump; solve_typing.
- - iApply (wp_cas_int_suc with "Hlx"). iIntros "!> Hlx".
- iMod (own_update with "Hownst") as "[Hownst ?]".
- { by eapply auth_update_alloc, (op_local_update_discrete _ _ writing_st). }
- iMod ("Hclose''" with "[Hlx Hownst]") as "Hβtok". { iExists _. iFrame. }
- iModIntro. wp_case. iMod ("Hclose'" with "Hβtok") as "Hα".
- iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _
[ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2);
#lx ◁ rwlockwriteguard α ty]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
- tctx_hasty_val' //. iFrame. iExists _, _. iFrame "∗#". }
+ tctx_hasty_val' //. iFrame "Hx Hr".
+ iExists γs, β. iSplitL "Hβ"; [by iApply (bor_iff with "[$EqO] Hβ")|].
+ iFrame "Hαβ wst". iSplitL "sst"; [by iExists st2|].
+ iExists _,_,_. iFrame "EqO EqS Hinv". by iExists _. }
iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
simpl. iApply type_jump; solve_typing.
+ - subst b.
+ iDestruct (rel_exist with "P") as (st') "mst".
+ iDestruct (rel_embed_elim with "mst") as "mst".
+ iMod ("Hclose''" with "[INV mst]") as "Hβtok".
+ { iIntros "Vb'". iDestruct ("INV" with "Vb'") as "$". by iExists _. }
+ iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
+ iModIntro. wp_case.
+ iApply (type_type _ _ _
+ [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]
+ with "[] LFT HE Hna HL Hk"); first last.
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+ iApply (type_sum_unit (option $ rwlockwriteguard α ty));
+ [solve_typing..|]; first last.
+ rewrite /option /=. iApply type_jump; solve_typing.
Qed.
End rwlock_functions.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index ad3d3ff839ea5f2ab39151fb81240a2723d15ea3..daa5c4e64c45ccfcb7daa1e6f327cb52105b9996 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -23,7 +23,7 @@ Section rwlockwriteguard.
match vl return _ with
| [ #(LitLoc l) ] =>
∃ γs β, &{β}((l +ₗ 1) ↦∗: ty.(ty_own) tid) ∗
- α ⊑ β ∗ rwown γs writing_st ∗
+ α ⊑ β ∗ rwown γs writing_st ∗ (∃ st, rwown γs (sub_st st)) ∗
(∃ γ tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty ∗
&at{β,rwlockN}(rwlock_proto_inv l γ γs β tyO tyS))
| _ => False
@@ -84,8 +84,8 @@ Section rwlockwriteguard.
iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [done|iSplit; iAlways].
- iIntros (tid [|[[]|][]]) "H"; try done.
- iDestruct "H" as (γs β) "(Hb & #H⊑ & Hown & Hinv)".
- iExists γs, β. iFrame "Hown". iSplit; last iSplit.
+ iDestruct "H" as (γs β) "(Hb & #H⊑ & Hown & Hsst & Hinv)".
+ iExists γs, β. iFrame "Hown Hsst". iSplit; last iSplit.
+ iApply bor_iff; last done.
iIntros "!>!#". iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".