stubs for wait/notify axiomatic

Author: conrad-watt

document/core/exec/relaxed.rst

@@ -101,6 +101,7 @@ Consistency
 .. math::
    \frac{
      \begin{array}[b]{@{}l@{}}
+       \vdash_{\reg} \trace \suspensionsconsistentwith \\
        \forall \evt_R \in \readingact_{\reg}(\trace), \exists \evt_W^\ast,
          \trace \vdash_{\reg} \evt_R \readseachfrom \evt_W^\ast \\
        \forall \evt_I, \evt \in \trace, \,
@@ -186,6 +187,15 @@ Consistency
      \vdash_{\reg} \evt_R \notear \evt_W^\ast
    }
 
+.. math::
+   \frac{
+     TODO
+   }{
+     \vdash_{\reg} \trace \suspensionsconsistentwith \\
+   }
+
+.. todo:: pull out the trace events which denote wait/wake actions as a timestamped list, check queue behaviour
+
 
 .. [#cite-oopsla2019]
    The semantics of the relaxed memory model is derived from the following article:

document/core/util/macros.def

@@ -1143,6 +1143,7 @@
 
 .. |consistent| mathdef:: \xref{exec/relaxed}{relaxed-consistent}{\mathrel{\mbox{consistent}}}
 .. |consistentwith| mathdef:: \xref{exec/relaxed}{relaxed-consistent}{\mathrel{\mbox{consistent-with}}}
+.. |suspensionsconsistentwith| mathdef:: \xref{exec/relaxed}{relaxed-consistent}{\mathrel{\mbox{suspensions-consistent-with}}}
 .. |readseachfrom| mathdef:: \xref{exec/relaxed}{relaxed-consistent}{\mathrel{\mbox{reads-each-from}}}
 .. |readsfrom| mathdef:: \xref{exec/relaxed}{relaxed-consistent}{\mathrel{\mbox{reads-from}}}
 .. |notear| mathdef:: \xref{exec/relaxed}{relaxed-consistent}{\mathrel{\mbox{no-tear}}}