Merge pull request #37 from SkyLabsAI/paolo/add-lockedG

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

Author: pgiarrusso-sl

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.

rocq-brick-libstdcpp/proof/mutex/spec.v

@@ -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).
 
@@ -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.
 
   (** <<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".
@@ -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)) *)