todo sweep

Author: conrad-watt

document/core/appendix/properties.rst

@@ -630,9 +630,6 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
      S; C \vdashadmininstr \PERFORM~\act^\ast : [] \to []
    }
 
-.. todo::
-   add wf action condition if defined
-
 
 .. index:: ! store extension, store
 .. _extend:
@@ -760,8 +757,11 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S'
      \vdashmeminstextends \{\MITYPE~\X{mt}, \MIDATA~b_1^{n_1}\} \extendsto \{\MITYPE~\X{mt}, \MIDATA~b_2^{n_2}\}
    }
 
-.. todo::
-   fixme: memory type can change since min limit is updated with growth; add shared case
+.. math::
+   \frac{
+   }{
+     \vdashmeminstextends \{\MITYPE~\X{mt}\} \extendsto \{\MITYPE~\X{mt}\}
+   }
 
 
 .. index:: global instance, value, mutability

document/core/exec/instructions.rst

@@ -3351,8 +3351,6 @@ The rules are identical to :ref:`non-atomic stores <exec-store>`, except that :m
 :math:`\MEMORYATOMICNOTIFY~\memarg`
 ....................................
 
-.. todo:: bounds edge-case, memory length?
-
 9. Let :math:`N` be 32.
 
 1. Assert: due to :ref:`validation <valid-atomic.rmwn>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
@@ -4149,8 +4147,6 @@ During its execution, a host function call may do any of the following.
 - Terminate with a list of values that respects the host function's type annotation.
 - Terminate with a trap.
 
-.. todo:: better prose, evaluate alternative approach where host may directly emit shared memory events
-
 .. math::
    ~\\[-1ex]
    \begin{array}{l}

document/core/exec/modules.rst

@@ -87,8 +87,8 @@ The following auxiliary typing rules specify this typing relation relative to a
      S; (\ARD_{\SEQCST}~a.\LLEN~l) \vdashexternval \EVMEM~a : \ETMEM~(\{ \LMIN~l, \LMAX~y^? \}~\SHARED)
    }
 
-.. todo::
-   flag up the connection with the relaxed memory model
+.. note::
+   In the |SHARED| case, the associated :ref:`action <syntax-act>` is performed as part of :ref:`instantiation <exec-instantiation>`, in order to record in the :ref:`Relaxed Memory Model <relaxed>` that a sequentially consistent bounds check on the shared memory has occurred.
 
 
 .. index:: global type, global address, value type, mutability

document/core/exec/relaxed.rst

@@ -26,6 +26,10 @@ Preliminary Definitions
    \locact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?)     & = & \loc \\
    \locact(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?)     & = & \loc \\
    \locact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast)   & = & \loc \\
+   \locact(\AWAIT~\loc~\s64)     & = & \loc \\
+   \locact(\AWOKEN~\loc)     & = & \loc \\
+   \locact(\ATIMEOUT~\loc)   & = & \loc \\
+   \locact(\ANOTIFY~\loc~\u32~\u32)     & = & \loc \\
    &&\\
    \ordact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?)     & = & \ord \\
    \ordact(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?)     & = & \ord \\
@@ -64,13 +68,7 @@ Preliminary Definitions
      && (\iff~\locact(\act) = \locact(\act') = \reg[\u32])  \\
    \end{array}
 
-.. todo:: add loc for wait/woken/timeout/notify
-
-.. todo:: Double check notears
-
-.. todo:: Tidy up range
-
-.. todo:: add prose intuition?
+.. todo:: nicer formatting, add prose intuition?
 
 
 .. _relaxed-trace:

document/core/exec/runtime.rst

@@ -324,8 +324,6 @@ It also is an invariant that the length of the element vector never exceeds the
 Memory Instances
 ~~~~~~~~~~~~~~~~
 
-.. todo:: We used to update the memory type when a memory is grown. This does not work for shared memories. In fact, the "current" type of a shared memory is nondeterministic. We need to model that during instantiation somehow.
-
 A *memory instance* is the runtime representation of a linear :ref:`memory <syntax-mem>`.
 It records its original :ref:`memory type <syntax-memtype>`
 and takes one of two different shapes depending on whether that type is :ref:`shared <syntax-shared>` or not.
@@ -581,7 +579,7 @@ In order to express the reduction of :ref:`traps <trap>`, :ref:`calls <syntax-ca
      \INVOKE~\funcaddr \\ &&|&
      \LABEL_n\{\instr^\ast\}~\instr^\ast~\END \\ &&|&
      \FRAME_n\{\frame\}~\instr^\ast~\END \\ &&|&
-     \WAITX~\loc~n \\ &&|&
+     \WAITX~\loc~\s64 \\ &&|&
      \PERFORM~\act^\ast \\ &&|&
      \HOSTE~\resulttype \\
    \end{array}
@@ -598,9 +596,11 @@ The |LABEL| and |FRAME| instructions model :ref:`labels <syntax-label>` and :ref
 Moreover, the administrative syntax maintains the nesting structure of the original :ref:`structured control instruction <syntax-instr-control>` or :ref:`function body <syntax-func>` and their :ref:`instruction sequences <syntax-instr-seq>` with an |END| marker.
 That way, the end of the inner instruction sequence is known when part of an outer sequence.
 
-.. todo:: describe |WAITX| and |PERFORM| and |HOSTE|
+The |WAITX| instruction models a thread suspending further execution as the result of executing a |\MEMORYATOMICWAIT| instruction. If its :math:`\s64` argument is non-negative, execution may resume after at least :math:`\s64` nanoseconds. Otherwise, execution will only resume after :math:`\loc` is the target of a corresponding |\MEMORYATOMICNOTIFY| instruction.
+
+The |PERFORM| instruction is used to perform an :ref:`action <syntax-act>` at a precise point in execution. These actions are used by the :ref:`Relaxed Memory Model <relaxed>` to determine the behaviours that are observable in a concurrent execution.
 
-.. todo:: add allocation instructions
+The |HOSTE| instruction models the execution of the host environment.
 
 .. note::
    For example, the :ref:`reduction rule <exec-block>` for |BLOCK| is:
@@ -709,9 +709,6 @@ Each event is annotated with two :ref:`time stamps <syntax-time>`: the first rec
      \byte^\ast \\
    \end{array}
 
-.. todo:: ensure identity of wait + wake operations is preserved
-.. todo:: remove spawn from events in a typed way?
-
 The access of *mutable* shared state is performed through the |ARD|, |AWR|, and |ARMW| actions.
 Each action accesses an abstract *location*, which consists of an :ref:`address <syntax-addr>` of a :ref:`shared <syntax-shared>` :ref:`memory <syntax-meminst>` instance, a symbolic *field* name in the respective object (either |LLEN| for the size or |LDATA| for the vector of bytes), and an offset index into the field.
 
@@ -740,7 +737,7 @@ Conventions
 
 * A location may syntactically elide its :math:`[\u32]` offset in the case that it is 0.
 
-The following auxiliary definition is used to classify whether an access will *tear*.
+The following auxiliary definition is used to classify whether an access will *tear* - that is, whether it will observably decompose into bytewise accesses when it participates in a data race.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
@@ -749,9 +746,6 @@ The following auxiliary definition is used to classify whether an access will *t
    \tearing(\fN', N, \u32)  &=& \epsilon \\
    \end{array}
 
-
-.. todo:: better description of tearing
-
 Relations between time stamps are lifted to relations between events.
 
 .. math::
@@ -760,8 +754,6 @@ Relations between time stamps are lifted to relations between events.
    \act_1^\ast~\AT~\time_p~\time_1 & \prechb & \act_2^\ast~\AT~\time'_p~\time_2  &=& \time_1 & \prechb & \time_2 \\
    \end{array}
 
-.. todo:: define notational shorthands over actions and events (or better put that in relaxed.rst?)
-
 
 .. index:: ! configuration, ! thread, store, frame, instruction, module instruction
 .. _syntax-thread:
@@ -855,8 +847,6 @@ The following rule for global reduction describes the creation of a new thread b
    This time stamp is chosen non-deterministically in the rule.
    However, the second side condition ensures that the time :math:`h` of the last activity of the thread *happened before* :math:`h'`, thereby imposing *program order* for any events originating from the same thread.
 
-.. todo:: check init ordering
-
 
 Local Reduction
 ...............

document/core/util/macros.def

@@ -1186,9 +1186,9 @@
 .. |REFEXTERNADDR| mathdef:: \xref{exec/runtime}{syntax-ref.extern}{\K{ref{.}extern}}
 .. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}}
 .. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}}
-.. |WAITX| mathdef:: \xref{exec/runtime}{syntax-waitx}{\K{wait'}}
-.. |PERFORM| mathdef:: \xref{exec/runtime}{syntax-perform}{\K{perform}}
-.. |HOSTE| mathdef:: \xref{exec/runtime}{syntax-hoste}{\K{host}}
+.. |WAITX| mathdef:: \xref{exec/runtime}{syntax-instr-admin}{\K{wait'}}
+.. |PERFORM| mathdef:: \xref{exec/runtime}{syntax-instr-admin}{\K{perform}}
+.. |HOSTE| mathdef:: \xref{exec/runtime}{syntax-instr-admin}{\K{host}}
 
 
 .. Values & Results, non-terminals

document/threads-luxury-todos.md

@@ -0,0 +1,7 @@
+exec/instructions
+- host functions: better prose, evaluate alternative approach where host may directly emit shared memory events
+
+appendix/properties
+- perform validity: add wf action condition if defined
+
+Investigate switching init write to happen up to max length at initialisation