Skip to content

recursive_mutex: add and use lockedG typeclass to prepare for ghost state #37

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
pgiarrusso-sl merged 2 commits into from
Feb 5, 2026
Merged

recursive_mutex: add and use lockedG typeclass to prepare for ghost state #37

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5a828f1
Cleanup
pgiarrusso-sl Dec 24, 2025
199da53
Depend on lockedG everywhere, rearrange lemmas
pgiarrusso-sl Dec 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 **
Expand All @@ -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 ->
Expand All @@ -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.
Expand Down
79 changes: 44 additions & 35 deletions rocq-brick-libstdcpp/proof/mutex/spec.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,25 +14,12 @@ Section with_cpp.
(** Fractional ownership of a <<std::mutex>> guarding the predicate <<P>>. *)
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).

Expand All @@ -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 Σ}.
Expand Down Expand Up @@ -103,10 +86,42 @@ End mutex.
Module recursive_mutex.

(** <<locked γ th n>> <<th>> owns the mutex <<γ>> <<n>> 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".
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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.
Expand All @@ -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 |-- |==>
Expand All @@ -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)) *)
Expand Down