diff --git a/_CoqProject b/_CoqProject index c03b2e2b60c556cb12f90154d5edf63677a55baa..bd1908a6ca9c62e83da7c9d78f77f576df4bacbe 100644 --- a/_CoqProject +++ b/_CoqProject @@ -63,9 +63,6 @@ theories/typing/lib/refcell/ref_code.v theories/typing/lib/refcell/refmut_code.v theories/typing/lib/refcell/refmut.v 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/examples/get_x.v theories/typing/examples/rebor.v theories/typing/examples/unbox.v diff --git a/theories/lang/lock.v b/theories/lang/lock.v index 7fea40904b31b8ff2037b083432c4b68dc5c4588..15f6c449e0b7c73c78feca4b9463e117523ac817 100644 --- a/theories/lang/lock.v +++ b/theories/lang/lock.v @@ -7,7 +7,9 @@ Set Default Proof Using "Type". Definition mklock_unlocked : val := λ: ["l"], "l" <- #false. Definition mklock_locked : val := λ: ["l"], "l" <- #true. -Definition try_acquire : val := λ: ["l"], CAS "l" #false #true AcqRel Relaxed. +(* If the CAS fails, it's a relaxed-read. + If the CAS succeeds, it's a acq-read and relaxed-write *) +Definition try_acquire : val := λ: ["l"], CAS "l" #false #true Relaxed AcqRel Relaxed. Definition acquire : val := rec: "acquire" ["l"] := if: try_acquire ["l"] then #☠ else "acquire" ["l"]. Definition release : val := λ: ["l"], "l" <-ʳᵉˡ #false. @@ -135,9 +137,9 @@ Section proof. wp_rec. iMod ("Hproto" with "HP") as (γ R0 Vb) "(#[Eq lc] & inv & Hclose)". iDestruct "lc" as (?) "lc". iMod (rel_True_intro True%I tid with "[//]") as "rTrue". - iApply (GPS_PPRaw_CAS_simple (lock_interp R0) _ _ _ _ + iApply (GPS_PPRaw_CAS_int_simple (lock_interp R0) _ _ _ _ _ (Z_of_bool false) #true () (λ _, R0)%I (λ _ _, True)%I - with "[$lc $inv rTrue]"); [done|by right|by left|..]. + with "[$lc $inv rTrue]");[done|by left|done|by right|by left|..]. { iSplitL ""; [|iSplitL ""]; [iNext; iModIntro..|]. - iIntros (?? _). by iApply lock_interp_comparable. - by iIntros (??)"_ #$".