Section 6 lore

paper.tex

@@ -3754,7 +3754,60 @@ \subsection{TSO weak memory}
     \end{aligned}
 \end{equation}
 
-\TODO{this category has ``too many'' morphisms: \ms{pflush}-sandwich subcategory; Elgot lore?}
+One issue with this model is that our category currently has ``too many'' operations besides the
+ones we want: for example, it is a perfectly valid morphism to simply add an event into the buffer
+without any flushing. Of course, one thing we could do is consider the smallest Elgot subcategory
+generated by the atomic instructions we want to support, such as \(\ms{read}_x\), \(\ms{write}_x\),
+and \(\ms{fence}\), which can be a perfectly valid approach, but is somewhat unwieldy. Another
+approach, however, is to think about what ``valid'' morphisms might look like in general; this
+also has the benefit of letting us write down specifications that may not be trivially implementable
+in terms of actual instructions.
+
+There are many potential properties we might want ``valid'' morphisms to have; in general, the less
+valid morphisms we admit, the more equations we have to work with when reasoning. One simple
+property we might consider is that a ``valid'' morphism must have at least one execution in which
+the buffer is completely flushed, regardless of initial state. This is a perfectly reasonable
+property to impose, since it ensures that we do not encounter degenerate cases where, for example,
+the parallel composition of two processes has an empty trace  set even though both processes have a
+nonempty trace set (since neither empties the buffer). We might even want to go a little bit further
+and, representing the fact that a buffer flush can happen at any time between instructions, require
+that a nondeterministic buffer flush before or after an instruction does not change its semantics,
+i.e., that $\ms{pflush}_A ; f ; \ms{pflush}_B = f$. Unfortunately, this does \emph{not} hold for
+the identity, since
+\begin{equation}
+  \ms{pflush} ; \ms{id} ; \ms{pflush} = \ms{pflush} ; \ms{pflush} = \ms{pflush} \neq \ms{id}
+\end{equation}
+so this would not give us a subcategory. While one possible solution is to simply add the identity
+back in (and this would give us a valid subcategory), we have the issue that, for example, morphisms
+like the associator and unitor would still be excluded. Instead, we can take into account the fact
+that all $\ms{pflush}_A$ are idempotent and define a new category $\ms{PTSO}$ with objects sets and
+morphisms of the form
+\begin{equation}
+  \ms{PTSO}(A, B) = \{\ms{pflush}_A; f; \ms{pflush}_B \mid f \in \ms{Set}_{\ms{TSO}}(A, B)\} 
+\end{equation}
+In this category, $\ms{pflush}_A$ is the identity on $A$, since
+\begin{equation}
+  \begin{aligned}
+    \ms{pflush}_A ; \ms{pflush}_A; f; \ms{pflush}_B &= \ms{pflush}_A; f; \ms{pflush}_B \\
+    \ms{pflush}_A; f; \ms{pflush}_B; \ms{pflush}_B &= \ms{pflush}_A; f; \ms{pflush}_B
+  \end{aligned}
+\end{equation}
+This is especially useful since it frees us from needing to remember to sprinkle $\ms{pflush}$
+everywhere when specifying things (and, of course, when that level of control is desired, we can
+specify in $\ms{Set}_{\ms{TSO}}$, and map using the natural identity-on-objects functor $f \mapsto
+\ms{pflush};f;\ms{pflush}$)!
+
+It turns out that this is a general construction we can do, which gives us another useful way to
+build up \isotopessa{} models that can often be quite difficult to express as simply monads.
+In particular, we have the following definition
+\begin{definition}[Idempotent envelope category]
+  \todo{this, and name...}
+  \todo{coproduct preservation case}
+  \todo{Elgot preservation lore (should always be true if coproducts are preserved, I think)}
+  \todo{premonoidal preservation case, Freyd preservation case}
+\end{definition}
+This gives us our final categorical model for TSO weak memory, $\ms{PTSO} =
+\ms{Ide}(\ms{Set}_{\ms{TSO}}, \ms{pflush})$.
 
 \section{Discussion and Related Work}
 
@@ -3791,6 +3844,12 @@ \subsection{General Models}
   structure, this can let us build up many useful models.
 \end{itemize}
 
+\subsection{Compositional Concurrency}
+
+\begin{itemize}
+  \item \citet{vale-linearizability-24} uses Karoubi-envelope lore which reminds me of our
+  $\ms{pflush}$-sandwich
+\end{itemize}
 
 \subsection{Compositional Relaxed Memory Concurrency}
 

references.bib

@@ -1066,4 +1066,21 @@ @InProceedings{siddharth-24-peephole
   URN =		{urn:nbn:de:0030-drops-207372},
   doi =		{10.4230/LIPIcs.ITP.2024.9},
   annote =	{Keywords: compilers, semantics, mechanization, MLIR, SSA, regions, peephole rewrites}
-}
+}
+
+@article{vale-linearizability-24,
+  author       = {Arthur Oliveira Vale and
+                  Zhong Shao and
+                  Yixuan Chen},
+  title        = {A Compositional Theory of Linearizability},
+  journal      = {J. {ACM}},
+  volume       = {71},
+  number       = {2},
+  pages        = {14:1--14:107},
+  year         = {2024},
+  url          = {https://doi.org/10.1145/3643668},
+  doi          = {10.1145/3643668},
+  timestamp    = {Tue, 07 May 2024 20:24:59 +0200},
+  biburl       = {https://dblp.org/rec/journals/jacm/ValeSC24.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
+}