Proof of a custom mutex implementation.

rocq-brick-libstdcpp/proof/atomic/pred.v

@@ -5,6 +5,7 @@
  * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details.
  *)
 Require Import skylabs.auto.cpp.spec.
+Require Import skylabs.bi.weakly_objective.
 Require Import skylabs.cpp.spec.concepts.
 Require skylabs.brick.libstdcpp.atomic.inc_int_cpp.
 
@@ -45,6 +46,8 @@ Module Type ATOMIC_PREDS.
     #[global] Declare Instance R_frac_valid : CFracValid1 R.
     #[global] Declare Instance R_agree : Cbn (Learn (any ==> learn_eq ==> learn_hints.fin) R).
     #[global] Declare Instance R_type : Typed2 (class_name ty) R.
+    #[global] Declare Instance R_weakly_objective q x p :
+      WeaklyObjective (R q x p).
   End R_props.
 
 End ATOMIC_PREDS.

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

@@ -3,12 +3,14 @@ Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
 Require Import skylabs.brick.libstdcpp.mutex.spec.lock_guard.
 
 Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
+Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
 
 Import linearity.
 
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
   Context {HAS_THREADS : HasStdThreads Σ}.
+  Context `{!lock_ghost.lockG Σ}.
 
   Import lock_guard.
 
@@ -17,9 +19,6 @@ Section with_cpp.
       Cbn (Learn (learn_eq ==> learn_eq ==> learn_eq ==> fin_at) mutex.R).
   Proof. solve_learnable. Qed.
 
-  #[global] Instance UNSAFE_token_learn : Cbn (Learn (req_eq ==> learn_eq ==> learn_hints.fin) mutex.token).
-  Proof. solve_learnable. Qed.
-
   #[local] Hint Resolve fractional.UNSAFE_read_prim_learn : sl_opacity.
 
   Lemma ctor_ok : verify[source] ctor_spec.

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

@@ -6,11 +6,13 @@ Require Import skylabs.brick.libstdcpp.mutex.spec.prelude.
 Require Import skylabs.brick.libstdcpp.mutex.spec.unique_lock.
 Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
 Require Import skylabs.brick.libstdcpp.lib.tactics.
+Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
 
 NES.Begin unique_lock.
   Section with_cpp.
     Context `{Σ : cpp_logic} {σ : genv}.
     Context `{HAS_THREADS : !HasStdThreads Σ}.
+    Context `{!lock_ghost.lockG Σ}.
 
     Import R_unfold.
 
@@ -43,10 +45,9 @@ NES.Begin unique_lock.
         "std::unique_lock<std::mutex>::unique_lock(std::mutex&)".
     Proof.
       verify_spec; go.
-      iExists K.
+      iExists K, q.
       (* Time Succeed solve [setoid_rewrite cQp.scale_mut; setoid_rewrite (right_id_L 1%Qp Qp.mul); ego with br_erefl]. *)
 
-      iExists _, q.
       rewrite cQp.scale_mut (right_id_L 1%Qp Qp.mul).
       go with br_erefl.
     Qed.

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

@@ -3,6 +3,7 @@ Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
 Require Export skylabs.brick.libstdcpp.runtime.pred.
 
 Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
+Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
 
 
 Import linearity.
@@ -47,6 +48,7 @@ Module lock_guard.
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
   Context {HAS_THREADS : HasStdThreads Σ}.
+  Context `{!lock_ghost.lockG Σ}.
 
   #[global] Instance R_learn :
     Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) lock_guard.R) :=
@@ -87,20 +89,20 @@ Section with_cpp.
     \arg{mp} "m" (Vptr mp)
     \persist{thr} current_thread thr
     \pre{g q P} mp |-> mutex.R g q$m P
-    \pre mutex.token g q
+    \pre lock_ghost.user g thr
     \post
       this |-> R (mp, g, q) 1$m P **
-      P ** mutex.locked g thr q
+      P ** mutex.locked g thr
     ).
 
   cpp.spec "std::lock_guard<std::mutex>::~lock_guard()" as dtor_spec from source with (
     \this this
     \pre{mp g q P} this |-> R (mp, g, q) 1$m P
     \persist{thr} current_thread thr
-    \pre mutex.locked g thr q
+    \pre mutex.locked g thr
     \pre ▷P
     \post
-      mutex.token g q **
+      lock_ghost.user g thr **
       mp |-> mutex.R g q$m P
   ).
 
@@ -124,4 +126,3 @@ Section with_cpp.
 
 End with_cpp.
 End lock_guard.
-

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

@@ -12,6 +12,8 @@ Require Export skylabs.brick.libstdcpp.runtime.pred.
 
 Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
 Require Import skylabs.brick.libstdcpp.mutex.requirements.
+Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
+Export skylabs.brick.libstdcpp.lib.lock_ghost(lockG).
 
 Import linearity.
 
@@ -28,20 +30,13 @@ Section with_cpp.
   #[global] Declare Instance R_learnable : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv},
       Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) R).
 
-  (** Owning [mutex_token γ 1] proves that the mutex is not locked, and
-  therefore can be safely destroyed: the standard specifies that calling
-  [std::mutex::~mutex()] while holding the lock results in undefined behavior.
-  *)
-  Parameter token : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv}, gname -> Qp -> mpred.
-  #[only(fractional,fracvalid,asfractional,timeless)] derive token.
-
   Section with_RepFor.
     Import rep.RepFor.
     Import RepScheme.
 
     #[global] Instance repfor `{!HasStdThreads Σ} {σ : genv} :
       rep.RepFor.C "std::mutex" [ArgType.Constant _; ArgType.CFrac; ArgType.Constant _]
-        (funI γ q P => R γ q P ∗ pureR (token γ q)) := {}.
+        (funI γ q P => R γ q P) := {}.
   End with_RepFor.
 
 
@@ -65,69 +60,78 @@ Section with_cpp.
     >>
    *)
   Parameter locked : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv},
-      gname -> thread_idT -> Qp -> mpred.
+      gname -> thread_idT -> mpred.
   #[only(timeless)] derive locked.
 
-  (** locked takes a [Qp] but _cannot_ be split. *)
   #[only(exclusive)] derive locked.
 
+  Context `{!lockG Σ}.
+
+  Abbreviation used_threads γ s :=
+    (lock_ghost.used_threads γ s).
+
+  Abbreviation users γ ths :=
+    (lock_ghost.users γ ths).
+
+  Abbreviation user γ th := (users γ {[ th ]}).
+
   Context `{MOD : source ⊧ σ}.
   Context {HAS_THREADS : HasStdThreads Σ}.
 
-  #[global] Instance locked_learn : Cbn (Learn (req_eq ==> learn_eq ==> learn_eq ==> learn_hints.fin) locked).
+  #[global] Instance locked_learn : Cbn (Learn (req_eq ==> learn_eq ==> learn_hints.fin) locked).
   Proof. solve_learnable. Qed.
 
 
   cpp.spec "std::mutex::mutex()" as ctor_spec with (
     \this this
     \pre{P} ▷P
-    \post Exists g, this |-> R g 1$m P ** token g 1).
+    \post Exists g, this |-> R g 1$m P ** used_threads g ∅).
 
   cpp.spec "std::mutex::~mutex()" as dtor_spec with (
     \this this
-    \pre{g P} this |-> R g 1$m P ** token g 1
+    \pre{g P} this |-> R g 1$m P ** used_threads g ∅
     \post P).
 
   (* "Inline" version of these specs. *)
   cpp.spec "std::mutex::lock()" as lock_spec_alt with (
     \this this
     \prepost{q P g} this |-> R g q P
     \persist{thr} current_thread thr
-    \pre{q'} token g q'
-    \post P ** locked g thr q').
+    \pre user g thr
+    \post P ** locked g thr).
 
   Definition do_lock (lk : gname * mpred) (K: mpred) : mpred :=
     let g := lk.1 in
     let P := lk.2 in
-    ∃ q thr, current_thread thr ∗ token g q ∗
+    ∃ thr, current_thread thr ∗ user g thr ∗
     (* TODO readd *)
     (* ▷ *)
-    (locked g thr q ** P -* K).
+    (locked g thr ** P -* K).
   #[global] Arguments do_lock /.
 
   cpp.spec "std::mutex::unlock()" as unlock_spec_alt with (
     \this this
     \prepost{q P g} this |-> R g q P
     \persist{thr} current_thread thr
-    \pre{q'} locked g thr q'
+    \pre locked g thr
     \pre ▷P
-    \post token g q').
+    \post user g thr).
 
   Definition do_unlock (lk : gname * mpred) (Q : mpred) : mpred :=
     let g := lk.1 in
     let P := lk.2 in
-    Exists q thr, current_thread thr ** locked g thr q ** ▷P **
+    Exists thr, current_thread thr ** locked g thr ** ▷P **
     (* TODO readd *)
     (* ▷ *)
-    (token g q -* Q).
+    (user g thr -* Q).
   #[global] Arguments do_unlock /.
 
   cpp.spec "std::mutex::try_lock()" as try_lock_spec_alt with (
     \this this
     \prepost{q P g} this |-> R g q P
     \persist{th} current_thread th
-    \pre{q'} token g q'
-    \post{b}[Vbool b] if b then P ** locked g th q' else token g q').
+    \pre user g th
+    \post{b}[Vbool b] if b then P ** locked g th else user g th).
 
   (* Obtain same specs from (Basic)Lockable. *)
   (** <<std::mutex>> implements [BasicLockable] *)
@@ -146,9 +150,9 @@ Section with_cpp.
   Definition do_try_lock (lk : gname * mpred) (Q : bool -> mpred) : mpred :=
     let g := lk.1 in
     let P := lk.2 in
-    ∃ q thr, current_thread thr ∗ token g q ∗
+    ∃ thr, current_thread thr ∗ user g thr ∗
     ∀ b : bool,
-    (if b then P ** locked g thr q else token g q) -∗ Q b.
+    (if b then P ** locked g thr else user g thr) -∗ Q b.
   #[global] Arguments do_try_lock /.
 
   #[global,program] Instance mutex_lockable : Lockable (T:=T) "std::mutex" (λ q γP, R γP.1 q γP.2) :=
@@ -173,4 +177,3 @@ Section with_cpp.
   Qed.
 End with_cpp.
 End mutex.
-

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

@@ -3,6 +3,7 @@ Require Import skylabs.brick.libstdcpp.mutex.inc_hpp.
 
 Require Export skylabs.brick.libstdcpp.runtime.pred.
 Require Import skylabs.brick.libstdcpp.mutex.spec.mutex.
+Require Import skylabs.brick.libstdcpp.lib.lock_ghost.
 
 Module scoped_lock.
   Section with_cpp.
@@ -17,6 +18,7 @@ Module scoped_lock.
     Section with_threads.
       Context {σ : genv}.
       Context `{HAS_THREADS : !HasStdThreads Σ}.
+      Context `{!lock_ghost.lockG Σ}.
 
       #[global] Instance: LearnEqF1 R := ltac:(solve_learnable).
 
@@ -25,17 +27,17 @@ Module scoped_lock.
       (* "std::scoped_lock<std::mutex, std::mutex>::scoped_lock(std::mutex&, std::mutex&)" *)
       as ctor_spec from source with (
         \this this
+        \persist{thr} current_thread thr
         \arg{mp1} "" (Vptr mp1)
         \pre{g1 q1 P1} mp1 |-> mutex.R g1 q1$m P1
-        \pre mutex.token g1 q1
+        \pre lock_ghost.user g1 thr
         \arg{mp2} "" (Vptr mp2)
         \pre{g2 q2 P2} mp2 |-> mutex.R g2 q2$m P2
-        \pre mutex.token g2 q2
-        \persist{thr} current_thread thr
+        \pre lock_ghost.user g2 thr
         \post
           this |-> R 1$m [ (mp1, g1, q1, P1); (mp2, g2, q2, P2)] **
-          P1 ** mutex.locked g1 thr q1 **
-          P2 ** mutex.locked g2 thr q2
+          P1 ** mutex.locked g1 thr **
+          P2 ** mutex.locked g2 thr
       ).
 
       cpp.spec "std::scoped_lock<...<std::mutex, std::mutex>>::~scoped_lock()"
@@ -50,11 +52,11 @@ Module scoped_lock.
           this |-> R 1$m [ (mp1, g1, q1, P1); (mp2, g2, q2, P2)]
         \pre |> P1
         \pre |> P2
-        \pre mutex.locked g1 thr q1
-        \pre mutex.locked g2 thr q2
+        \pre mutex.locked g1 thr
+        \pre mutex.locked g2 thr
         \post
-          mp1 |-> mutex.R g1 q1$m P1 ** mutex.token g1 q1 **
-          mp2 |-> mutex.R g2 q2$m P2 ** mutex.token g2 q2
+          mp1 |-> mutex.R g1 q1$m P1 ** lock_ghost.user g1 thr **
+          mp2 |-> mutex.R g2 q2$m P2 ** lock_ghost.user g2 thr
       ).
     End with_threads.
   End with_cpp.

rocq-brick-libstdcpp/test/mutex/custom_mutex.hpp

@@ -16,13 +16,14 @@ std::mutex protocol:
 - can't be destroyed while held.
 */
 class MyMutex {
-  std::atomic<bool> m_lock{false};
+  // std::atomic<bool> m_lock{false};
+  std::atomic<int> m_lock{0};
 
   std::thread::id m_owner{};
 
   // "Actual locking"
   void do_lock() {
-    while (m_lock.exchange(true)) {
+    while (m_lock.exchange(1)) {
       // Yielding helps scheduling, and makes this loop obviously not UB
       // (under https://eel.is/c++draft/intro.progress#1.2).
       // Calling exchange might qualify under
@@ -32,10 +33,12 @@ class MyMutex {
   }
 
   void do_unlock() {
-    m_lock = false;
+    m_lock = 0;
   }
 public:
 
+  MyMutex() {}
+
   void lock() {
     std::thread::id this_id{std::this_thread::get_id()};
 
@@ -60,7 +63,7 @@ class MyMutex {
   }
 
   ~MyMutex() {
-    assert(!m_lock);
+    assert(m_lock == 0);
     assert(m_owner == std::thread::id()); //unowned
   }
 };