diff --git a/_CoqProject b/_CoqProject index e11d05278fdf979e417560538971829fed6eb1c2..bcd7c44e3edb75bf71114b63d0fbe87bed0f2381 100644 --- a/_CoqProject +++ b/_CoqProject @@ -54,6 +54,8 @@ theories/typing/lib/cell.v theories/typing/lib/spawn.v theories/typing/lib/rc/rc.v theories/typing/lib/rc/weak.v +theories/typing/lib/mutex/mutex.v +theories/typing/lib/mutex/mutexguard.v theories/typing/lib/refcell/refcell.v theories/typing/lib/refcell/ref.v theories/typing/lib/refcell/refmut.v diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v index b85d05f1599b9fd90224774969d47837ad8ba8f7..adcdcffbd5056639c4f7a519a1a2103abc916b73 100644 --- a/theories/lang/lib/lock.v +++ b/theories/lang/lib/lock.v @@ -45,21 +45,20 @@ Section proof. Qed. (** The main proofs. *) - Lemma lock_proto_create (E : coPset) (R : iProp Σ) l (b : bool) : - l ↦ #b -∗ (if b then True else ▷ R) ={E}=∗ ∃ γ, ▷ lock_proto γ l R. + Lemma lock_proto_create (R : iProp Σ) l (b : bool) : + l ↦ #b -∗ (if b then True else ▷ R) ==∗ ∃ γ, ▷ lock_proto γ l R. Proof. iIntros "Hl HR". iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done. iExists _, _. iFrame "Hl". destruct b; first done. by iFrame. Qed. - Lemma lock_proto_destroy E γ l R : - ↑N ⊆ E → - ▷ lock_proto γ l R ={E}=∗ ∃ (b : bool), l ↦ #b ∗ if b then True else ▷ R. + Lemma lock_proto_destroy γ l R : + lock_proto γ l R -∗ ∃ (b : bool), l ↦ #b ∗ if b then True else R. Proof. - iIntros (?) "Hlck". iDestruct "Hlck" as (b) "[>Hl HR]". + iIntros "Hlck". iDestruct "Hlck" as (b) "[Hl HR]". iExists b. iFrame "Hl". destruct b; first done. - iDestruct "HR" as "[_ $]". done. + iDestruct "HR" as "[_ $]". Qed. (* At this point, it'd be really nice to have some sugar for symmetric diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v new file mode 100644 index 0000000000000000000000000000000000000000..23fb26f041e561e56d9fd785551f4a09260c58c2 --- /dev/null +++ b/theories/typing/lib/mutex/mutex.v @@ -0,0 +1,90 @@ +From Coq.QArith Require Import Qcanon. +From iris.proofmode Require Import tactics. +From iris.algebra Require Import auth csum frac agree. +From iris.base_logic Require Import big_op. +From lrust.lang.lib Require Import memcpy lock. +From lrust.lifetime Require Import na_borrow. +From lrust.typing Require Export type. +From lrust.typing Require Import typing option. +Set Default Proof Using "Type". + +Definition mutexN := lrustN .@ "mutex". + +(* This type is an experiment in defining a Rust type on top of a non-typesysten-specific + interface, like the one provided by lang.lib.lock. + It turns out that we need an accessor-based spec for this purpose, so that + we can put the protocol into shared borrows. Cancellable invariants + don't work because their cancelling view shift has a non-empty mask, + and it would have to be executed in the consequence view shift of + a borrow. +*) + +Section mutex. + Context `{!typeG Σ, !lockG Σ}. + + (* + pub struct Mutex<T: ?Sized> { + // Note that this mutex is in a *box*, not inlined into the struct itself. + // Once a native mutex has been used once, its address can never change (it + // can't be moved). This mutex type can be safely moved at any time, so to + // ensure that the native mutex is used correctly we box the inner lock to + // give it a constant address. + inner: Box<sys::Mutex>, + poison: poison::Flag, + data: UnsafeCell<T>, + } + *) + + Program Definition mutex (ty : type) := + {| ty_size := 1 + ty.(ty_size); + ty_own tid vl := + match vl return _ with + | #(LitInt z) :: vl' => + ⌜∃ b, z = Z_of_bool b⌝ ∗ ty.(ty_own) tid vl' + | _ => False end; + ty_shr κ tid l := + ∃ γ κ', + &shr{κ, mutexN} (lock_proto γ l (&{κ'} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗ κ ⊑ κ' + |}%I. + Next Obligation. + iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq. + iIntros "[_ %] !% /=". congruence. + Qed. + Next Obligation. + iIntros (ty E κ l tid q ?) "#LFT Hbor Htok". + iMod (bor_acc_cons with "LFT Hbor Htok") as "[H Hclose]"; first done. + iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]". + rewrite heap_mapsto_vec_cons. iDestruct "H↦" as ">[Hl H↦]". + iDestruct "H" as "[>EQ Hown]". iDestruct "EQ" as %[b ->]. + (* We need to turn the ohne borrow into two, so we close it -- and then + we open one of them again. *) + iMod ("Hclose" $! ((∃ b, l ↦ #(Z_of_bool b)) ∗ (shift_loc l 1 ↦∗: ty_own ty tid))%I + with "[] [Hl H↦ Hown]") as "[Hbor Htok]". + { clear. iNext. iIntros "[Hl Hown] !>". iNext. iDestruct "Hl" as (b) "Hl". + iDestruct "Hown" as (vl) "[H↦ Hown]". iExists (#(Z_of_bool b) :: vl). + rewrite heap_mapsto_vec_cons. iFrame. iPureIntro. eauto. } + { iNext. iSplitL "Hl"; first by eauto. + iExists vl. iFrame. } + clear b vl. iMod (bor_sep with "LFT Hbor") as "[Hl Hbor]"; first done. + iMod (bor_acc_cons with "LFT Hl Htok") as "[>Hl Hclose]"; first done. + iDestruct "Hl" as (b) "Hl". + iMod (lock_proto_create with "Hl [Hbor]") as (γ) "Hproto". + { destruct b; last by iExact "Hbor". done. } + iMod ("Hclose" with "[] Hproto") as "[Hl Htok]". + { clear b. iIntros "!> Hproto !>". iDestruct (lock_proto_destroy with "Hproto") as (b) "[Hl _]". + iNext. eauto with iFrame. } + iFrame "Htok". iExists γ, κ. + iMod (bor_share with "Hl") as "$"; [solve_ndisj..|]. + iApply lft_incl_refl. + Qed. + Next Obligation. + iIntros (ty κ κ' tid l) "#Hincl H". + iDestruct "H" as (γ κ'') "(#Hlck & #Hlft)". + iExists _, _. iSplit; first by iApply shr_bor_shorten. + iApply lft_incl_trans; done. + Qed. + + Global Instance mutex_wf ty `{!TyWf ty} : TyWf (mutex ty) := + { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }. + +End mutex. diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v new file mode 100644 index 0000000000000000000000000000000000000000..034ed18c3972978e23effa6e0ab8ac2d51623fed --- /dev/null +++ b/theories/typing/lib/mutex/mutexguard.v @@ -0,0 +1,82 @@ +From Coq.QArith Require Import Qcanon. +From iris.proofmode Require Import tactics. +From iris.algebra Require Import auth csum frac agree. +From iris.base_logic Require Import big_op. +From lrust.lang.lib Require Import memcpy lock. +From lrust.lifetime Require Import na_borrow. +From lrust.typing Require Export type. +From lrust.typing Require Import typing util option mutex. +Set Default Proof Using "Type". + +(* This type is an experiment in defining a Rust type on top of a non-typesysten-specific + interface, like the one provided by lang.lib.lock. + It turns out that we need an accessor-based spec for this purpose, so that + we can put the protocol into shared borrows. Cancellable invariants + don't work because their cancelling view shift has a non-empty mask, + and it would have to be executed in the consequence view shift of + a borrow. +*) + +Section mguard. + Context `{!typeG Σ, !lockG Σ}. + + (* + pub struct MutexGuard<'a, T: ?Sized + 'a> { + // funny underscores due to how Deref/DerefMut currently work (they + // disregard field privacy). + __lock: &'a Mutex<T>, + __poison: poison::Guard, + } + *) + + Program Definition mutex_guard (α : lft) (ty : type) := + {| ty_size := 1; + ty_own tid vl := + match vl return _ with + | [ #(LitLoc l) ] => + ∃ γ β, locked γ ∗ α ⊑ β ∗ + &shr{α, mutexN} (lock_proto γ l (&{β} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗ + &{β} (shift_loc l 1 ↦∗: ty.(ty_own) tid) + | _ => False end; + ty_shr κ tid l := + ∃ (l':loc), &frac{κ}(λ q', l ↦{q'} #l') ∗ + □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α⊓κ] + ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (α⊓κ) tid (shift_loc l' 1) ∗ q.[α⊓κ] + |}%I. + Next Obligation. by iIntros (? ty tid [|[[]|][]]) "H". Qed. + (* This is to a large extend copy-pasted from RWLock's write guard. *) + Next Obligation. + iIntros (α ty E κ l tid q HE) "#LFT Hb Htok". + iMod (bor_exists with "LFT Hb") as (vl) "Hb"; first done. + iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done. + iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done. + destruct vl as [|[[|l'|]|][]]; + try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]". + setoid_rewrite heap_mapsto_vec_singleton. + iMod (bor_exists with "LFT Hb") as (γ) "Hb"; first done. + iMod (bor_exists with "LFT Hb") as (β) "Hb"; first done. + iMod (bor_sep with "LFT Hb") as "[Hlcked H]"; first done. + iMod (bor_sep with "LFT H") as "[Hαβ H]"; first done. + iMod (bor_sep with "LFT H") as "[_ H]"; first done. + iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]"; first done. + iExists _. iFrame "H↦". iApply delay_sharing_nested; try done. + (* FIXME: "iApply lft_intersect_mono" only preserves the later on the last + goal, as does "iApply (lft_intersect_mono with ">")". *) + iNext. iApply lft_intersect_mono. done. iApply lft_incl_refl. + Qed. + Next Obligation. + iIntros (??????) "#? H". iDestruct "H" as (l') "[#Hf #H]". + iExists _. iSplit. + - by iApply frac_bor_shorten. + - iIntros "!# * % Htok". + iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj. + { iApply lft_intersect_mono. iApply lft_incl_refl. done. } + iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext. + iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$". + iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done. + Qed. + + Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) := + { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }. + +End mguard. diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v index db17b3e5830be1ea7c2944aa7cf6055eda0c95d5..a75c30b74c9169d2ee33bcb6955d4539396e96d0 100644 --- a/theories/typing/lib/rwlock/rwlock.v +++ b/theories/typing/lib/rwlock/rwlock.v @@ -149,7 +149,7 @@ Section rwlock. iExists _, _. iFrame. iApply lft_incl_trans; auto. Qed. - Global Instance join_handle_wf ty `{!TyWf ty} : TyWf (rwlock ty) := + Global Instance rwlock_wf ty `{!TyWf ty} : TyWf (rwlock ty) := { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }. Global Instance rwlock_type_ne : TypeNonExpansive rwlock.