New ghost state for mutex spec & implementation; give up user ghost state.

.gitignore

@@ -17,3 +17,4 @@ _RocqProject
 
 # Only at the root, since it comes from enabling `dune.disabled` locally
 /dune
+*.bbl

papers/cpp-mutex/stdcpp.tex

@@ -419,11 +419,11 @@ \subsection{\lstinline{unique_lock}}
 
 %how much of this detail is useful? There are a lot of variations.
 \[\begin{array}{c}
-\{p \mapsto R(q, m) \ast \dolock{p}{m}{K}\}\\ \texttt{unique\_lock(p)}\\ \{\ulock(\mathsf{Some}\ (\mathsf{false}, p, q, m))\} \vspace{1em}\\%constructor notation?
-\{u \mapsto \ulock(m)\ast \neg \mathsf{held}(m) \ast \dolock{\mathsf{ptr}(m)}{\mathsf{m}(m)}{K}\}\\ {u\texttt{.lock()}} \\ \{m \mapsto \ulock(m[\mathsf{held} := \mathsf{true}]) \ast K\}  \vspace{1em}\\
-    \{u \mapsto \ulock(m)\ast \mathsf{held}(m) \ast \dounlock{\mathsf{ptr}(m)}{\mathsf{m}(m)}{K}\}\\ {u\texttt{.unlock}()}\\
+\{p \mapsto R(q, m) \ast \dolock{p}{m}{K}\}\\ \texttt{unique\_lock(p)}\\ \{u.\ u \mapsto \ulock(\mathsf{Some}\ (\mathsf{false}, p, q, m))\} \vspace{1em}\\%constructor notation?
+\{u \mapsto \ulock(m)\ast \neg \mathsf{held}(m) \ast \dolock{\mathsf{ptr}(m)}{\mathsf{m}(m)}{K}\}\\ {\texttt{u.lock()}} \\ \{m \mapsto \ulock(m[\mathsf{held} := \mathsf{true}]) \ast K\}  \vspace{1em}\\
+    \{u \mapsto \ulock(m)\ast \mathsf{held}(m) \ast \dounlock{\mathsf{ptr}(m)}{\mathsf{m}(m)}{K}\}\\ {\texttt{u.unlock}()}\\
     \{m \mapsto \ulock(m[\mathsf{held} := \mathsf{false}]) \ast K\}  \vspace{1em} \\
-\{u \mapsto \ulock() \ast (\text{if } \mathsf{held}(m) \text{ then } \dounlock{\mathsf{ptr}(m)}{\mathsf{m}(m)}{K}\} \text{ else } K)\}\\ \sim u()\\ \{K \ast \text{if } m \text{ then } \mathsf{ptr}(m) \mapsto R(\mathsf{q}(m), \mathsf{m}(m)) \text { else } \mathsf{emp}\} %destructor notation, Some/None notation
+\{u \mapsto \ulock() \ast (\text{if } \mathsf{held}(m) \text{ then } \dounlock{\mathsf{ptr}(m)}{\mathsf{m}(m)}{K}\} \text{ else } K)\}\\ \texttt{u.}\!\!\sim\!\texttt{unique\_lock}()\\ \{K \ast \text{if } m \text{ then } \mathsf{ptr}(m) \mapsto R(\mathsf{q}(m), \mathsf{m}(m)) \text { else } \mathsf{emp}\} %destructor notation, Some/None notation
 \end{array}\]
 %verify the code from cppreference or a similar example?
 
@@ -449,15 +449,82 @@ \subsection{\lstinline{unique_lock}}
 As discussed in Section~\ref{basic-lockable}, the \lstinline{BasicLockable} requirement does not explicitly require that \lstinline{lock} lead to mutual exclusion, and indeed recursive mutexes can be \lstinline{lock}ed multiple times without being \lstinline{unlock}ed. This interacts in an interesting and useful way with \lstinline{unique_lock}'s acquisition tracking (the $\mathsf{held}$ predicate in our specifications): each \lstinline{unique_lock} can only acquire its mutex at most once, but we can construct multiple \lstinline{unique_lock}s around a single recursive mutex, each of which manages a single acquisition. %Is this equally true of lock_guard? We could call unlock once manually to illustrate the point.
 The code in Figure~\ref{unique-recursive} shows how this can be used. When \lstinline{answer} is called, it acquires the recursive mutex \lstinline{m} by constructing a \lstinline{unique_lock} around it; it then calls \lstinline{inc}, which constructs another \lstinline{unique_lock} that acquires \lstinline{m} a second time. When each method returns, its \lstinline{unique_lock} is destroyed and \lstinline{m} is released once, so that \lstinline{m} is no longer locked after \lstinline{answer} returns. Our specifications can be used to verify this program. %proof outline?
 
-\section{Case Studies?}
-\input{ring_buffer.tex}
+\section{Case Study: Mutex Encapsulation}
+%\input{ring_buffer.tex}
 %TODO: find or make some interesting examples
 
+We have seen that enforcing the requirements of C++ mutexes requires the management of thread-specific permission predicates that must be transferred between threads and locks. We have demonstrated that this is possible in simple examples of each mutex type, but we also want to know that our approach scales to programs with multiple mutex-carrying objects. %rephrase
+There are at least two possible pitfalls. First, it might be difficult for a thread to acquire two different mutexes, because we need to manually prove that the second mutex is not the same as the first. Second and more subtly, thread-specific predicates might leak through layers of abstraction. Our mutex specifications must include predicates like $\notlocked{\gamma}{t}$ that explicitly mention thread IDs, but a data structure that uses a mutex internally should not need to expose thread IDs in its interface; it should be possible to share the data structure among threads exactly as one would a non-mutex-based implementation, without extra registration steps. In this section, we verify a case study showing that we avoid both these pitfalls, suggesting that our mutex specifications can indeed be used for modular verification.
+
+\begin{figure}[htb]
+\begin{lstlisting}
+class Account {
+private:
+  unsigned long balance;
+  std::recursive_mutex mut; // protects balance
+
+public:
+  explicit Account(unsigned long initial_balance) : balance(initial_balance) {}
+
+  void incr_balance(unsigned long i) {
+    std::lock_guard<std::recursive_mutex> lg(mut);
+    balance += i;
+  }
+
+  void transfer_to(Account target, unsigned long i) {
+    std::lock_guard<std::recursive_mutex> lg(mut);
+    balance -= i;
+    target.incr_balance(i);
+  }
+}
+
+int main() {
+  Account from{4};
+  Account to{2};
+  from.transfer_to(to, 3);
+}
+\end{lstlisting}
+\caption{The code of our case study}
+\label{transfer}
+\end{figure}
+
+
+The code of our case study is shown in Figure~\ref{transfer}. Each object of class \lstinline{Account} has a \lstinline{balance} protected by a mutex (in this code we use a \lstinline{recursive_mutex}, but any form of mutex would work). %make generic?
+The \lstinline{transfer_to} method decrements the receiver's %terminology?
+balance and increments the target object's balance, acquiring both mutexes in the process. Our questions are then:
+\begin{enumerate}
+\item How do we prove that we can acquire \lstinline{target}'s mutex, given that we already hold the receiver's mutex?
+\item Can we use a representation predicate for \lstinline{Account} that is freely transferable between threads and does not take a thread ID as a parameter?
+\end{enumerate}
+
+%how much do we need to explain namespaces?
+
+For question 2, recall that our specifications for \lstinline{recursive_mutex} are:
+\[\begin{array}{c}
+\{\currentthread{t} \ast m \mapsto_q \rmutex{\gamma}{P}\ast\acquirable{\gamma}{t}{n}{P}{a}\}\\ {\texttt{m.lock()}} \\ \{m \mapsto_q \rmutex{\gamma}{P}\ast \exists a'.\ \mathsf{acquire}(n, a, a') \ast \acquirable{\gamma}{t}{n+1}{P}{a'}\}  \vspace{1em}\\
+    \{\currentthread{t} \ast m \mapsto_q \rmutex{\gamma}{P}\ast\acquirable{\gamma}{t}{n+1}{P}{a}\}\\ {\texttt{m.unlock}()}\\
+    \{m \mapsto_q \rmutex{\gamma}{P}\ast\acquirable{\gamma}{t}{n}{P}{a}\}
+\end{array}\]
+The $\mathsf{holds}$ predicate takes a thread $t$ that must match the current thread, and we must have it at line 15 %confirm
+in order to acquire \lstinline{mut}. On the other hand, \lstinline{transfer_to} is a function that can be called by any thread that has access to the two accounts involved, and should have a specification like
+\[ \{ a \mapsto_q \mathsf{account}{\gamma_a} \ast b \mapsto_q \mathsf{account}{\gamma_b} \}\ \texttt{a.transfer\_to(b, n)}\ \{ a \mapsto_q \mathsf{account}{\gamma_a} \ast b \mapsto_q \mathsf{account}{\gamma_b} \}\]
+In particular, if $\mathsf{account}$ takes a thread $t$ as an argument, then we will not be able to freely transfer ownership of it between threads (since it would only be usable by that thread $t$). The mutex permission library allows us to isolate this thread-local information. 
+
+If the precondition of \lstinline{transfer_to} includes $\mathsf{holds}$, then it will also need to mention the thread $t$, and so will not be freely 
+
+The representation predicate for \lstinline{Account} is defined as
+\[p \mapsto_q \mathsf{account}(\gamma) \triangleq p.\texttt{mut} \mapsto \rmutex{\gamma}{\lambda n.\ p.\texttt{balance} \mapsto n} \ast \mathsf{token}_\gamma(q)
+\]
+Ownership of an \lstinline{Account} is simply ownership of the mutex protecting the \lstinline{balance} field, plus ownership of the $\mathsf{token}$ that tracks whether the lock is held. In particular, it makes no mention of the $\mathsf{holds}$ predicate that appears in the precondition of the \lstinline{recursive_mutex} specifications (and explicitly takes a thread $t$ as an argument). Then, how does 
+
 \section{BRiCk Formalization}
+note that BRiCk itself is an axiomatic semantics
 
 \section{Conclusion and Future Work}
 ...
 
+%the client problem: all preconditions need not_locked, can't be transferred between threads, so if we include it in an abstract predicate that predicate can't be transferred either (even if it uses locks in a way that would never allow double acquire)
+
 condition variables, futures, shared pointers, ...
 
 verified Pthread?

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.
 
@@ -48,6 +49,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/dune.inc

@@ -227,6 +227,18 @@
   	 (with-stderr-to inc_string_cpp.v.stderr (run cpp2v -v %{input} -o inc_string_cpp.v --no-elaborate --templates=inc_string_cpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_string.cpp))
 )
+(subdir thread
+ (rule
+  (targets thread_hpp.v.stderr thread_hpp.v thread_hpp_templates.v)
+  (alias test_ast)
+  (deps
+   (:input thread.hpp)
+   (env_var CPP2V_DOCKER_ENABLED)
+   (glob_files_rec ../*.hpp))
+  (action
+  	 (with-stderr-to thread_hpp.v.stderr (run cpp2v -v %{input} -o thread_hpp.v --no-elaborate --templates=thread_hpp_templates.v  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps thread.hpp))
+)
 (subdir vector
  (rule
   (targets inc_vector_cpp.v.stderr inc_vector_cpp.v inc_vector_cpp_templates.v)