diff --git a/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v b/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v index 8a0268c..96ca3b1 100644 --- a/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v +++ b/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v @@ -34,7 +34,7 @@ Definition P `{Σ : cpp_logic, σ : genv} (this : ptr) : TT -t> mpred := sl.lock Definition CR - `{Σ : cpp_logic, σ : genv, HasOwn (iPropI _) recursive_mutex.cmraR} + `{Σ : cpp_logic, σ : genv, HasOwn (iPropI _) recursive_mutex.cmraR, !recursive_mutex.lockedG Σ} (γ : recursive_mutex.rmutex_gname) (q : cQp.t) : Rep := structR "C" q ** _field "C::mut" |-> recursive_mutex.R γ.(recursive_mutex.lock_gname) q ** @@ -49,6 +49,7 @@ Section recursive_mutex. Context `{Σ : cpp_logic, σ : genv}. Context {HAS_THREADS : HasStdThreads Σ}. Context {has_rmutex : HasOwn (iPropI _) recursive_mutex.cmraR}. + Context `{!recursive_mutex.lockedG Σ}. Lemma acquireable_update_equiv {TT : tele} γ th f t1 t2 P : acquire t1 t2 -> @@ -66,6 +67,7 @@ Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. Context {HAS_THREADS : HasStdThreads Σ}. Context {has_rmutex : HasOwn (iPropI _) recursive_mutex.cmraR}. + Context `{!recursive_mutex.lockedG Σ}. #[global] Instance: LearnEq2 CR'. Proof. solve_learnable. Qed. diff --git a/rocq-brick-libstdcpp/proof/mutex/spec.v b/rocq-brick-libstdcpp/proof/mutex/spec.v index 283336f..667765e 100644 --- a/rocq-brick-libstdcpp/proof/mutex/spec.v +++ b/rocq-brick-libstdcpp/proof/mutex/spec.v @@ -14,25 +14,12 @@ Section with_cpp. (** Fractional ownership of a <> guarding the predicate <

>. *) Parameter R : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv}, gname -> cQp.t -> mpred -> Rep. #[only(cfractional,cfracvalid,ascfractional,timeless)] derive R. - (* - #[global] Declare Instance mutex_rep_typed : Typed3 "std::mutex" mutex_rep. - #[global] Declare Instance mutex_rep_cfrac : forall γ, CFractional1 (mutex_rep γ). - #[global] Declare Instance mutex_rep_ascfrac : forall γ, AsCFractional2 (mutex_rep γ). - #[global] Declare Instance mutex_rep_cfracvalid : forall γ, CFracValid2 (mutex_rep γ). - #[global] Declare Instance mutex_rep_timeless : Timeless3 mutex_rep. - *) #[global] Declare Instance mutex_rep_typed : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv}, Typed3 "std::mutex" R. (* TODO: index this by the specific mutex! Either via a mutex_gname or by making this a Rep *) (* TODO: why is this separate from [mutex_rep] *) Parameter mutex_token : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv}, gname -> cQp.t -> mpred. #[only(cfractional,cfracvalid,ascfractional,timeless)] derive mutex_token. - (* - #[global] Declare Instance mutex_token_cfrac : CFractional1 mutex_token. - #[global] Declare Instance mutex_token_ascfrac : AsCFractional1 mutex_token. - #[global] Declare Instance mutex_token_cfracvalid : CFracValid1 mutex_token. - #[global] Declare Instance mutex_token_timeless : Timeless2 mutex_token. - *) #[global] Declare Instance mutex_rep_learnable : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv}, Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) R). @@ -57,10 +44,6 @@ Section with_cpp. *) Parameter mutex_locked : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv}, gname -> thread_idT -> mpred. #[only(timeless,exclusive)] derive mutex_locked. - (* - Declare Instance mutex_locked_timeless : Timeless2 mutex_locked. - Declare Instance mutex_locked_excl g : Exclusive1 (mutex_locked g). - *) Context `{MOD : inc_hpp.source ⊧ σ}. Context {HAS_THREADS : HasStdThreads Σ}. @@ -103,10 +86,42 @@ End mutex. Module recursive_mutex. (** <> <> owns the mutex <<γ>> <> times. *) - Parameter locked : ∀ `{Σ : cpp_logic}, gname -> thread_idT -> nat -> mpred. - #[global] Declare Instance - locked_WeaklyObjective `{Σ : cpp_logic} γ thr n : - WeaklyObjective (PROP := iPropI _) (locked γ thr n). + #[projections(primitive=no)] + Class lockedG `{Σ : cpp_logic} := { + }. + #[global] Arguments lockedG {_ _} Σ : assert. + + Parameter locked : + ∀ `{Σ : cpp_logic, !lockedG Σ} + (γ : gname) (th : thread_idT) (n : nat), mpred. + + Parameter used_threads : + ∀ `{Σ : cpp_logic, !lockedG Σ, !HasStdThreads Σ} + (γ : gname) (s : gset thread_idT), mpred. + + #[only(timeless)] derive locked. + #[only(timeless)] derive used_threads. + + Section locked_with_cpp. + Context `{Σ : cpp_logic}. + Context `{!lockedG Σ}. + Context `{!HasStdThreads Σ}. + + Axiom use_thread : ∀ th g s, + th ∉ s -> + current_thread th ** used_threads g s |-- + |==> used_threads g (s ∪ {[ th ]}) ** locked g th 0. + + #[global] Declare Instance + locked_WeaklyObjective γ thr n : + WeaklyObjective (PROP := iPropI _) (locked γ thr n). + + Axiom locked_excl_same_thread : forall g th n m, + locked g th n ** locked g th m |-- False. + Axiom locked_excl_different_thread : forall g th th' n m, + locked g th n ** locked g th' m |-- [| n = 0 \/ m = 0 |] ** True. + + End locked_with_cpp. (* the mask of recursive_mutex *) Definition mask := nroot .@@ "std" .@@ "recursive_mutex". @@ -119,7 +134,9 @@ Module recursive_mutex. Canonical Structure cmraR := (excl_authR (prodO natO thread_idTO)). sl.lock - Definition inv_rmutex `{Σ : cpp_logic} `{!HasOwn (iPropI _) cmraR} (g : rmutex_gname) (P : mpred) : mpred := + Definition inv_rmutex + `{Σ : cpp_logic} `{!lockedG Σ} `{!HasOwn (iPropI _) cmraR} + (g : rmutex_gname) (P : mpred) : mpred := inv rmutex_namespace (Exists n th, own g.(level_gname) (●E (n, th)) ** match n with @@ -135,8 +152,6 @@ Module recursive_mutex. | Held (n : nat) (xs : TT) (* acquired [n + 1] times with quantifiers [xs] *). #[global] Arguments acquire_state _ : clear implicits. - Parameter used_threads : ∀ `{Σ : cpp_logic}, gname -> gset thread_idT -> mpred. - sl.lock Definition acquire {TT} (a a' : acquire_state TT) : Prop := match a with @@ -167,7 +182,9 @@ Module recursive_mutex. end. sl.lock - Definition acquireable `{Σ : cpp_logic, !HasStdThreads Σ, !HasOwn (iPropI _) cmraR} (g : rmutex_gname) (th : thread_idT) {TT: tele} (t : acquire_state TT) (P : TT -t> mpred) : mpred := + Definition acquireable + `{Σ : cpp_logic, !lockedG Σ, !HasStdThreads Σ, !HasOwn (iPropI _) cmraR} + (g : rmutex_gname) (th : thread_idT) {TT: tele} (t : acquire_state TT) (P : TT -t> mpred) : mpred := current_thread th ** match t with | NotHeld => locked g.(lock_gname) th 0 @@ -177,13 +194,8 @@ Module recursive_mutex. Section with_cpp. Context `{Σ : cpp_logic}. - #[global] Declare Instance locked_timeless : Timeless3 locked. - Axiom locked_excl_same_thread : forall g th n m, - locked g th n ** locked g th m |-- False. - Axiom locked_excl_different_thread : forall g th th' n m, - locked g th n ** locked g th' m |-- [| n = 0 \/ m = 0 |] ** True. - Context `{!HasOwn (iPropI _) cmraR, !HasStdThreads Σ}. + Context `{!lockedG Σ}. #[global] Instance acquireable_learn γ th TT : LearnEq2 (acquireable γ th (TT := TT)). Proof. solve_learnable. Qed. @@ -192,10 +204,6 @@ Module recursive_mutex. `{Observe (current_thread th) (acquireable g th (TT := TT) t P)}. Proof. rewrite acquireable.unlock; apply _. Qed. - Axiom use_thread : forall th g m, - th ∉ m -> - current_thread th ** used_threads g m |-- |==> used_threads g (m ∪ {[ th ]}) ** locked g th 0. - Lemma use_thread_acquirable {TT} th g m P : th ∉ m -> current_thread th ** used_threads g.(lock_gname) m |-- |==> @@ -212,6 +220,7 @@ Module recursive_mutex. Section with_cpp. Context `{Σ : cpp_logic} `{MOD : source ⊧ σ}. Context {HAS_THREADS : HasStdThreads Σ}. + Context `{!lockedG Σ}. (* NOTE: Invariant used to protect resource [r] inv (r \\// exists th n, locked th (S n)) *)