$$
\newcommand{\RR}{\mathbb{R}}
\newcommand{\GG}{\mathbb{G}}
\newcommand{\PP}{\mathbb{P}}
\newcommand{\PS}{\mathcal{P}}
\newcommand{\SS}{\mathbb{S}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\CC}{\mathbb{C}}
\newcommand{\HH}{\mathbb{H}}
\newcommand{\ones}{\mathbb{1\hspace{-0.4em}1}}
\newcommand{\alg}[1]{\mathfrak{#1}}
\newcommand{\mat}[1]{ \begin{pmatrix} #1 \end{pmatrix} }
\renewcommand{\bar}{\overline}
\renewcommand{\hat}{\widehat}
\renewcommand{\tilde}{\widetilde}
\newcommand{\inv}[1]{ {#1}^{-1} }
\newcommand{\eqdef}{\overset{\text{def}}=}
\newcommand{\block}[1]{\left(#1\right)}
\newcommand{\set}[1]{\left\{#1\right\}}
\newcommand{\abs}[1]{\left|#1\right|}
\newcommand{\trace}[1]{\mathrm{tr}\block{#1}}
\newcommand{\norm}[1]{ \left\| #1 \right\| }
\newcommand{\argmin}[1]{ \underset{#1}{\mathrm{argmin}} }
\newcommand{\argmax}[1]{ \underset{#1}{\mathrm{argmax}} }
\newcommand{\st}{\ \mathrm{s.t.}\ }
\newcommand{\sign}[1]{\mathrm{sign}\block{#1}}
\newcommand{\half}{\frac{1}{2}}
\newcommand{\inner}[1]{\langle #1 \rangle}
\newcommand{\dd}{\mathrm{d}}
\newcommand{\ddd}[2]{\frac{\partial #1}{\partial #2} }
\newcommand{\db}{\dd^b}
\newcommand{\ds}{\dd^s}
\newcommand{\dL}{\dd_L}
\newcommand{\dR}{\dd_R}
\newcommand{\Ad}{\mathrm{Ad}}
\newcommand{\ad}{\mathrm{ad}}
\newcommand{\LL}{\mathcal{L}}
\newcommand{\Krylov}{\mathcal{K}}
\newcommand{\Span}[1]{\mathrm{Span}\block{#1}}
\newcommand{\diag}{\mathrm{diag}}
\newcommand{\tr}{\mathrm{tr}}
\newcommand{\sinc}{\mathrm{sinc}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\Ob}[1]{\mathrm{Ob}\block{\cat{#1}}}
\newcommand{\Hom}[1]{\mathrm{Hom}\block{\cat{#1}}}
\newcommand{\op}[1]{\cat{#1}^{op}}
\newcommand{\hom}[2]{\cat{#1}\block{#2}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\Set}{\mathbb{Set}}
\newcommand{\Cat}{\mathbb{Cat}}
\newcommand{\Hask}{\mathbb{Hask}}
\newcommand{\lim}{\mathrm{lim}\ }
\newcommand{\funcat}[1]{\left[\cat{#1}\right]}
\newcommand{\natsq}[6]{
\begin{matrix}
& #2\block{#4} & \overset{#2\block{#6}}\longrightarrow & #2\block{#5} & \\
{#1}_{#4} \hspace{-1.5em} &\downarrow & & \downarrow & \hspace{-1.5em} {#1}_{#5}\\
& #3\block{#4} & \underset{#3\block{#6}}\longrightarrow & #3\block{#5} & \\
\end{matrix}
}
\newcommand{\comtri}[6]{
\begin{matrix}
#1 & \overset{#4}\longrightarrow & #2 & \\
#6 \hspace{-1em} & \searrow & \downarrow & \hspace{-1em} #5 \\
& & #3 &
\end{matrix}
}
\newcommand{\natism}[6]{
\begin{matrix}
& #2\block{#4} & \overset{#2\block{#6}}\longrightarrow & #2\block{#5} & \\
{#1}_{#4} \hspace{-1.5em} &\downarrow \uparrow & & \downarrow \uparrow & \hspace{-1.5em} {#1}_{#5}\\
& #3\block{#4} & \underset{#3\block{#6}}\longrightarrow & #3\block{#5} & \\
\end{matrix}
}
\newcommand{\cone}[1]{\mathcal{#1}}
$$
Concurrent ML
- optimization: split optimistic and pessimistic phases to skip
waiting
- optimistic
- non-blockingly check queue for waiting items
- complete transaction if found
- otherwise, pessimistic:
- suspend execution until someone else completes the transaction,
which will resume us
- publish ourselves as waiting in queue
- (could be done in reverse order with proper locking)
- but this introduces a possible deadlock if not careful:
- nobody is waiting in queue during the optimisic phase on both
sides, so both sides suspend hence nobody will resume the other (oh noes!)
- so we need to recheck after publishing ourselves as waiting,
before actually suspending
- if waiting items found:
- unpublish ourselves
- complete transaction
- else: suspend
- but now re-checking is concurrent with other side’s optimistic phase
and re-checking. that is, while we re-check:
- the other side may optimistically complete our transaction (C1)
- the other side may attempt to complete our transaction during its own
re-check (C2)
so we need some way of publishing that we’re rechecking
(symmetrically, detect that the other side is rechecking), and act
accordingly:
- the other side will not attempt to optimistically complete a
transaction currently being rechecked, so C1 cannot happen
- the other side will not consider a transaction currently being
rechecked during its own recheck phase, so C2 cannot
happen. instead, we’ll wait (spin) until recheck is over.
to this end we introduce the following states:
W: waiting (initial state, when published)C: claimed (when re-checking)S: synched (when complete)
this side will be A, the other side will be B. after publishing,
the following transitions are possible on side A:
W -> S (B completed during its optimistic phase)W -> C (A claimed)C -> W (A rolled back)C -> S (A completed during recheck, after claiming)
recheck
- if empty queue: wait
- else try to claim our side
A: W -> C
- otherwise
A: S: optimistically completed by other side
- unpublish our side
- complete transaction
- otherwise
A: C: impossible
- success: try to
B: W -> S the other side (queue head)
- success:
- complete our side
A: C -> S
- unpublish our side
- resume other side
- complete transaction
- otherwise
B: S: somebody else completed the other side
- rollback B: C -> W
- otherwise
B: C: somebody else is already claiming the other side
optimistic phase
- walk the queue until
cas(W->S)
pessimistic phase
- publish ourselves as
W (our state may change soon after)
- must now recheck queue for waiting states (otherwise potential deadlock)
- claim our tx
W -> C (otherwise someone else could complete us
while we complete someone else)
- success: our state may no longer change until we decide it to
- if empty queue: suspend
- else
cas(W->S) on queue head
- success:
- pop
- complete tx
- unpublish ourselves/mark as
S
- otherwise:
- otherwise:
S: someone else completed us, hence popped us
C: someone else is claiming this tx, spin
invariants
- we only ever pop
S states
e-mail comments/suggestions