Link Search Menu Expand Document
\( % cbs-katex.sty % \newcommand{\STYLE}[2]{\htmlClass{cbs-#1}{#2}} \newcommand{\DECL}[3]{\htmlId{#1:#2}{#3}} \newcommand{\REF}[3]{\href{###1:#2}{#3}} \newcommand{\HYPER}[5]{\href{#1/#2/index.html###3:#4}{#5}} % \SHADE{MATH} can be defined to produce a shaded background to highlight % inline MATH in running text: \newcommand{\SHADE}[1]{#1} % \KEY{TEXT}, \STRING{TEXT}, \ATOM{TEXT}, \LEX{TEXT} can be used in math mode: \newcommand{\KEY}[1]{\textsf{\textit{\STYLE{Key}{#1}}}} \newcommand{\STRING}[1]{\textsf{``\texttt{#1}''}} \newcommand{\ATOM}[1]{\textsf{`\texttt{#1}'}} \newcommand{\LEX}[1]{\textsf{\STYLE{Key}{`}\texttt{#1}\STYLE{Key}{'}}} % The following commands produce ASCII characters that are treated specially by LaTeX: \newcommand{\HASH}{\char`\#} \newcommand{\DOLLAR}{\char`\$} \newcommand{\PERCENT}{\char`\%} \newcommand{\AMPERSAND}{\char`\&} \newcommand{\APOSTROPHE}{\char`\'} \newcommand{\BACKSLASH}{\char`\\} \newcommand{\CARET}{\char`\^} \newcommand{\UNDERSCORE}{\char`\_} \newcommand{\GRAVE}{\char`\`} \newcommand{\LEFTBRACE}{\char`\{} \newcommand{\RIGHTBRACE}{\char`\}} \newcommand{\TILDE}{\textasciitilde} % {\char`\~} % \NAME{name} highlights the name; % \NAMEDECL{name} declares Name.name as the target of links to name; % \NAMEREF{name} links name to the target Name.name in the current file; % \NAMEHYPER{url}{file}{name} links name to Name.name at url/file/file.pdf. % Similarly for \VAR{partvariable}, \SYN{syntaxname}, \SEM{semanticsName}, % and \SECT{sectionnumber} % The kerns in \SUB and \VAR avoid overlaps with primes: \newcommand{\SUB}[1]{_{\kern-2mu\STYLE{PartVariable}{\textsf{#1}}}} % PLAIN \newcommand{\VAR}[1]{\STYLE{PartVariable}{\textsf{\textit{#1}\kern2mu}}} \newcommand{\NAME}[1]{\STYLE{Name}{\textsf{#1}}} \newcommand{\SYN}[1]{\STYLE{SyntaxName}{\textsf{#1}}} \newcommand{\SEM}[1]{\STYLE{SemanticsName}{\textsf{#1}}} \newcommand{\SECT}[1]{\STYLE{SectionNumber}{\textsf{#1}}} % DECL \newcommand{\VARDECL}[1]{\DECL{PartVariable}{#1}{\VAR{#1}}} \newcommand{\NAMEDECL}[1]{\DECL{Name}{#1}{\NAME{#1}}} \newcommand{\SYNDECL}[1]{\DECL{SyntaxName}{#1}{\SYN{#1}}} \newcommand{\SEMDECL}[1]{\DECL{SemanticsName}{#1}{\SEM{#1}}} \newcommand{\SECTDECL}[1]{\DECL{SectionNumber}{#1}{\textsf{#1}}} % REF \newcommand{\VARREF}[1]{\REF{PartVariable}{#1}{\VAR{#1}}} \newcommand{\NAMEREF}[1]{\REF{Name}{#1}{\NAME{#1}}} \newcommand{\SYNREF}[1]{\REF{SyntaxName}{#1}{\SYN{#1}}} \newcommand{\SEMREF}[1]{\REF{SemanticsName}{#1}{\SEM{#1}}} \newcommand{\SECTREF}[1]{\REF{SectionNumber}{#1}{\SECT{#1}}} % HYPER \newcommand{\VARHYPER}[3]{\HYPER{#1}{#2}{PartVariable}{#3}{\VAR{#3}}} \newcommand{\NAMEHYPER}[3]{\HYPER{#1}{#2}{Name}{#3}{\NAME{#3}}} \newcommand{\SYNHYPER}[3]{\HYPER{#1}{#2}{SyntaxName}{#3}{\SYN{#3}}} \newcommand{\SEMHYPER}[3]{\HYPER{#1}{#2}{SemanticsName}{#3}{\SEM{#3}}} \newcommand{\SECTHYPER}[3]{\HYPER{#1}{#2}{SectionNumber}{#3}{\SECT{#3}}} % \LEFTPHRASE MATH \RIGHTPHRASE produces [[ MATH ]] with proper brackets: \newcommand{\LEFTPHRASE}{\llbracket} \newcommand{\RIGHTPHRASE}{\rrbracket} % \LEFTGROUP MATH \RIGHTGROUP produces ( MATH ) where the parentheses are % highlighted the same as keywords: \newcommand{\LEFTGROUP}{\STYLE{Key}{(}} \newcommand{\RIGHTGROUP}{\STYLE{Key}{)}} % MATH\PLUS produces a superscript + % MATH\STAR produces a superscript * % MATH\QUERY produces a superscript ? \newcommand{\PLUS}{{}^{\texttt{+}}} \newcommand{\STAR}{{}^{\texttt{*}}} \newcommand{\QUERY}{{}^{\texttt{?}}} % \RULE{& PREMISE \\ & ...}{& FORMULA ... \\ & ...} produces an inference rule % with separately aligned premises and conclusion % PREMISE % ... % ----------- % FORMULA ... % ... \newcommand{\RULE}[2] {\frac{\begin{aligned}#1\end{aligned}}{\begin{aligned}#2\end{aligned}}} % \AXIOM{& FORMULA ... \\ & ...} produces an aligned formula % % FORMULA ... % ... \newcommand{\AXIOM}[1]{\begin{aligned}#1\end{aligned}} % \TO TYPE produces => TYPE \newcommand{\TO}{\mathop{\Rightarrow}} % TERM \TRANS TERM produces TERM ---> TERM \newcommand{\TRANS}{\longrightarrow} % TERM \xrightarrow{LABEL} TERM puts the label above the long arrow % \)

Unstable-Funcons-beta : Notifications.cbs | PLAIN | PDF

OUTLINE

Notifications

\[\begin{align*} [ \ \textsf{Barriers } \ & \textsf{} \\ \KEY{Funcon} \quad & \NAMEREF{barrier-create} \\ \KEY{Funcon} \quad & \NAMEREF{barrier-sync} \\ \KEY{Funcon} \quad & \NAMEREF{barrier-sync-else-wait} \\ \textsf{Conditions } \ & \textsf{} \\ \KEY{Funcon} \quad & \NAMEREF{condition-create} \\ \KEY{Funcon} \quad & \NAMEREF{condition-wait} \\ \KEY{Funcon} \quad & \NAMEREF{condition-wait-with-lock} \\ \KEY{Funcon} \quad & \NAMEREF{condition-notify-all} \\ \KEY{Funcon} \quad & \NAMEREF{condition-notify-first} \\ \textsf{Rendezvous } \ & \textsf{} \\ \KEY{Funcon} \quad & \NAMEREF{rendezvous-create} \\ \KEY{Funcon} \quad & \NAMEREF{rendezvous-sync} \\ \KEY{Funcon} \quad & \NAMEREF{rendezvous-sync-else-wait} \ ] \end{align*}\]

Threads may synchronise by waiting for notifications. In contrast to locks, notifications are ephemeral, and do not get held and released.

Barriers

A barrier notifies all requesting threads when a specified number of requests for it have been made. Subsequent requests give immediate notification.

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{barrier-create}( \VAR{N} : \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{pos-ints}) : \TO \NAME{syncs} \\&\quad \leadsto \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{give} ( \\&\quad\quad\quad\quad \NAME{sync-create} ( \\&\quad\quad\quad\quad\quad \NAME{sync-feature-create} \ \NAME{sync-waiting-list}, \\&\quad\quad\quad\quad\quad \NAME{sync-feature-create} \ \NAME{sync-count} ), \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assign} ( \NAME{sync-feature} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given}, \NAME{sync-count} ), \VAR{N} ), \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ) ) \end{align*}\]

When the barrier is already open, requests to pass it are granted immediately. When the barrier is closed, and only one more thread needs to arrive, granting a request for it opens the barrier and resumes all the threads wiating for it; otherwise the request fails.

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{barrier-sync}( \VAR{SY} : \NAME{syncs}) : \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-type} \\&\quad \leadsto \NAMEHYPER{../..}{Multithreading}{thread-atomic} \ \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{give} ( \\&\quad\quad\quad\quad \NAME{sync-feature} ( \VAR{SY}, \NAME{sync-count} ), \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{else} ( \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{check-true} \ \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned} \ \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given}, 0 ), \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{check-true} \ \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned} \ \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given}, 1 ), \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assign} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given}, 0 ), \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../..}{Multithreading}{thread-resume} \ \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{list-elements} \\&\quad\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned} \ \NAME{sync-feature} ( \VAR{SY}, \NAME{sync-waiting-list} ), \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assign} ( \NAME{sync-feature} ( \VAR{SY}, \NAME{sync-waiting-list} ), [ \ ] ) ) ) ) \end{align*}\]

When the request fails, the current thread is added to the waiting list, and suspended until the request can be granted:

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{barrier-sync-else-wait}( \VAR{SY} : \NAME{syncs}) : \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-type} \\&\quad \leadsto \NAMEHYPER{../..}{Multithreading}{thread-atomic} \ \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{else} ( \\&\quad\quad\quad\quad \NAMEREF{barrier-sync} ( \VAR{SY} ), \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \\&\quad\quad\quad\quad\quad \NAME{sync-waiting-list-add} ( \VAR{SY}, \NAMEHYPER{../..}{Multithreading}{current-thread} ), \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assign} ( \\&\quad\quad\quad\quad\quad\quad \NAME{sync-feature} ( \VAR{SY}, \NAME{sync-count} ), \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \ \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{nat-pred} \ \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned} \ \NAME{sync-feature} ( \VAR{SY}, \NAME{sync-count} ) ), \\&\quad\quad\quad\quad\quad \NAMEHYPER{../..}{Multithreading}{thread-suspend} \ \NAMEHYPER{../..}{Multithreading}{current-thread} ) ) \end{align*}\]
Conditions

A condition is used to represent whether some property holds or not. Threads may request to be notified when another thread makes the property hold.

A condition may notify either one or all of its requesting threads. When it has to notify one thread but more than one request for notification has been made, the choice of thread may be determined by the scheduler. When it has to notify more than one thread, the property associated with the condition may have been invalidated by the time the executions of some of them are resumed, and threads may need to iterate requests for notifications.

In practice, a condition is generally associated with an exclusive lock. When a thread awaiting the condition is notified, it requests the exclusive lock and tests whether the required property holds; if it does not, the thread releases the exclusive lock, and atomically reverts to requesting the notification.

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{condition-create} : \TO \NAME{syncs} \\&\quad \leadsto \NAME{sync-create} ( \\&\quad\quad\quad\quad \NAME{sync-feature-create} \ \NAME{sync-waiting-list} ) \end{align*}\]

A condition request always adds the current thread to the waiting list, and suspends it until the request can be granted. (In practice, it takes also an associated exclusive lock as a further argument, assumed to be held by the current thread, and releases it at the same time as suspending the thread.)

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{condition-wait}( \VAR{SY} : \NAME{syncs}) : \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-type} \\&\quad \leadsto \NAMEHYPER{../..}{Multithreading}{thread-atomic} \ \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \\&\quad\quad\quad\quad \NAME{sync-waiting-list-add} ( \VAR{SY}, \NAMEHYPER{../..}{Multithreading}{current-thread} ), \\&\quad\quad\quad\quad \NAMEHYPER{../..}{Multithreading}{thread-suspend} \ \NAMEHYPER{../..}{Multithreading}{current-thread} ) \end{align*}\]

In practice, a condition request usually takes also an associated exclusive lock as a further argument, assumed to be held by the current thread, releases it together with suspending the thread, and waits for the lock when resumed:

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{condition-wait-with-lock}( \VAR{SY} : \NAME{syncs}, \VAR{L} : \NAME{syncs}) : \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-type} \\&\quad \leadsto \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \\&\quad\quad\quad\quad \NAMEHYPER{../..}{Multithreading}{thread-atomic} \ \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \\&\quad\quad\quad\quad\quad \NAMEHYPER{../.}{Locks}{exclusive-lock-release} ( \VAR{L} ), \\&\quad\quad\quad\quad\quad \NAME{sync-waiting-list-add} ( \VAR{SY}, \NAMEHYPER{../..}{Multithreading}{current-thread} ), \\&\quad\quad\quad\quad\quad \NAMEHYPER{../..}{Multithreading}{thread-suspend} \ \NAMEHYPER{../..}{Multithreading}{current-thread} ), \\&\quad\quad\quad\quad \NAMEHYPER{../.}{Locks}{exclusive-lock-sync-else-wait} ( \VAR{L} ) ) \end{align*}\]

Threads that are waiting for the condition are notified simply by resuming them. To notify them all:

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{condition-notify-all}( \VAR{SY} : \NAME{syncs}) : \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-type} \\&\quad \leadsto \NAMEHYPER{../..}{Multithreading}{thread-atomic} \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \\&\quad\quad\quad\quad\quad \NAMEHYPER{../..}{Multithreading}{thread-resume} \ \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{list-elements} \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned} \ \NAME{sync-feature} ( \VAR{SY}, \NAME{sync-waiting-list} ), \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assign} ( \NAME{sync-feature} ( \VAR{SY}, \NAME{sync-waiting-list} ), [ \ ] ) ) \end{align*}\]

To notify just one of the waiting threads:

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{condition-notify-first}( \VAR{SY} : \NAME{syncs}) : \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-type} \\&\quad \leadsto \NAMEHYPER{../..}{Multithreading}{thread-atomic} \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{give} ( \\&\quad\quad\quad\quad\quad \NAME{sync-waiting-list-head-remove} ( \VAR{SY} ), \\&\quad\quad\quad\quad\quad \NAMEHYPER{../..}{Multithreading}{thread-resume} \ \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ) \end{align*}\]
Rendezvous

A rendezvous notifies all requesting threads as soon as a specified number \(\SHADE{\VAR{N}}\) of them have made matching requests for it. The rendezvous can store any number of non-matching requests. If a request that completes a rendezvous matches different sets of \(\SHADE{\VAR{N-1}}\) pending requests, the ‘lexicographically’ earliest set of requests is selected; for a binary rendezvous, this is the first matching request in the stored list.

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{rendezvous-create}( \VAR{N} : \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{pos-ints}) : \TO \NAME{syncs} \\&\quad \leadsto \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{give} ( \\&\quad\quad\quad\quad \NAME{sync-create} ( \\&\quad\quad\quad\quad\quad \NAME{sync-feature-create} \ \NAME{sync-waiting-list}, \\&\quad\quad\quad\quad\quad \NAME{sync-feature-create} \ \NAME{sync-count} ), \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assign} ( \NAME{sync-feature} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given}, \NAME{sync-count} ), \VAR{N} ), \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ) ) \end{align*}\]

Each rendezvous request includes a pattern, and the corresponding notifications give environments obtained by matching the patterns against the same unified value. When the pattern in each request is simply a value, a rendezvous notifies all the requesting threads as soon as the specified number of requests with the same value have been made. When the pattern in one request is a value, a pattern in another request may bind an identifier to that value, giving one-way data flow.

A rendezvous request may also include a set of additional threads which are all required to participate in the rendezvous. When a pair of matching binary rendezvous requests each specify the other thread as the only required participant, the rendezvous is restricted to that pair of threads. When one of the sets is empty, the rendezvous may involve any other thread.

In this simplified version, rendezvous are always binary, patterns in requests are ground values, and sets of required threads are omitted.

When a rendezvous is available, granting a request for it removes the first matching element from the waiting list, and resumes its thread; otherwise the request fails.

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{rendezvous-sync}( \VAR{SY} : \NAME{syncs}, \VAR{V} : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{ground-values}) : \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-type} \\&\quad \leadsto \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{give} ( \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned} \ \NAME{sync-feature} ( \VAR{SY}, \NAME{sync-waiting-list} ), \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{check-true} \ \NAMEREF{is-rendezvous-match} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given}, \VAR{V} ), \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assign} ( \\&\quad\quad\quad\quad\quad\quad \NAME{sync-feature} ( \VAR{SY}, \NAME{sync-waiting-list} ), \\&\quad\quad\quad\quad\quad\quad \NAMEREF{rendezvous-first-match-drop} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given}, \VAR{V} ) ), \\&\quad\quad\quad\quad\quad \NAMEHYPER{../..}{Multithreading}{thread-resume} \\&\quad\quad\quad\quad\quad\quad \NAMEREF{rendezvous-first-match-thread} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given}, \VAR{V} ) ) ) \end{align*}\]

When the request fails, a tuple of the value and the current thread is added to the waiting list, and the thread suspended until the request can be granted:

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{rendezvous-sync-else-wait}( \VAR{SY} : \NAME{syncs}, \VAR{V} : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{ground-values}) : \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-type} \\&\quad \leadsto \NAMEHYPER{../..}{Multithreading}{thread-atomic} \ \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{else} ( \\&\quad\quad\quad\quad \NAMEREF{rendezvous-sync} ( \VAR{SY}, \VAR{V} ), \\&\quad\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \\&\quad\quad\quad\quad\quad \NAME{sync-waiting-list-add} ( \VAR{SY}, \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple} ( \VAR{V}, \NAMEHYPER{../..}{Multithreading}{current-thread} ) ), \\&\quad\quad\quad\quad\quad \NAMEHYPER{../..}{Multithreading}{thread-suspend} \ \NAMEHYPER{../..}{Multithreading}{current-thread} ) ) \end{align*}\]

The remaining rendezvous funcons are all auxiliary:

\[\begin{align*} \KEY{Auxiliary Type} \quad & \NAMEDECL{rendezvous-waits} \leadsto \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuples} ( \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{ground-values}, \NAMEHYPER{../..}{Multithreading}{thread-ids} ) \end{align*}\]

The funcon \(\SHADE{\NAMEREF{is-rendezvous-match} ( \VAR{L}, \VAR{V} )}\) returns whether the list \(\SHADE{\VAR{L}}\) contains \(\SHADE{\NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple} ( \VAR{V}, \VAR{TI} )}\) for some \(\SHADE{\VAR{TI}}\):

\[\begin{align*} \KEY{Auxiliary Funcon} \quad & \NAMEDECL{is-rendezvous-match}( \_ : \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{lists} ( \NAMEREF{rendezvous-waits} ), \_ : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{ground-values}) : \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{booleans} \end{align*}\] \[\begin{align*} \KEY{Rule} \quad & \NAMEREF{is-rendezvous-match} ( [ \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple} ( \VAR{V}', \VAR{TI} ), \VAR{P}\STAR ], \VAR{V} : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values} ) \leadsto \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else} ( \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal} ( \VAR{V}', \VAR{V} ), \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{true}, \NAMEREF{is-rendezvous-match} ( [ \VAR{P}\STAR ], \VAR{V} ) ) \\ \KEY{Rule} \quad & \NAMEREF{is-rendezvous-match} ( [ \ ], \VAR{V} : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values} ) \leadsto \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{false} \end{align*}\]

The funcon \(\SHADE{\NAMEREF{rendezvous-first-match-thread} ( \VAR{L}, \VAR{V} )}\) returns the thread-id of the first element of \(\SHADE{\VAR{L}}\) with value \(\SHADE{\VAR{V}}\):

\[\begin{align*} \KEY{Auxiliary Funcon} \quad & \NAMEDECL{rendezvous-first-match-thread}( \_ : \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{lists} ( \NAMEREF{rendezvous-waits} ), \_ : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values}) \\&\quad : \TO \NAMEHYPER{../..}{Multithreading}{thread-ids} \end{align*}\] \[\begin{align*} \KEY{Rule} \quad & \NAMEREF{rendezvous-first-match-thread} ( [ \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple} ( \VAR{V}', \VAR{TI} ), \VAR{P}\STAR ], \VAR{V} : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values} ) \leadsto \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else} ( \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal} ( \VAR{V}', \VAR{V} ), \VAR{TI}, \NAMEREF{rendezvous-first-match-thread} ( [ \VAR{P}\STAR ], \VAR{V} ) ) \\ \KEY{Rule} \quad & \NAMEREF{rendezvous-first-match-thread} ( [ \ ], \VAR{V} : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values} ) \leadsto \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{fail} \end{align*}\]

The funcon \(\SHADE{\NAMEREF{rendezvous-first-match-drop} ( \VAR{L}, \VAR{V} )}\) returns the list \(\SHADE{\VAR{L}}\) omitting the first element with value \(\SHADE{\VAR{V}}\):

\[\begin{align*} \KEY{Auxiliary Funcon} \quad & \NAMEDECL{rendezvous-first-match-drop}( \_ : \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{lists} ( \NAMEREF{rendezvous-waits} ), \_ : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values}) \\&\quad : \TO \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{lists} ( \NAMEREF{rendezvous-waits} ) \end{align*}\] \[\begin{align*} \KEY{Rule} \quad & \NAMEREF{rendezvous-first-match-drop} ( [ \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple} ( \VAR{V}', \VAR{TI} ), \VAR{P}\STAR ], \VAR{V} : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values} ) \leadsto \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else} ( \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{is-equal} ( \VAR{V}', \VAR{V} ), \\&\quad\quad [ \VAR{P}\STAR ], \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Lists}{cons} ( \NAMEHYPER{../../../../../Funcons-beta/Values/Composite}{Tuples}{tuple} ( \VAR{V}', \VAR{TI} ), \NAMEREF{rendezvous-first-match-drop} ( [ \VAR{P}\STAR ], \VAR{V} ) ) ) \\ \KEY{Rule} \quad & \NAMEREF{rendezvous-first-match-drop} ( [ \ ], \VAR{V} : \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values} ) \leadsto \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{fail} \end{align*}\]

A series of rendezvous between the same two threads is called an extended rendezvous. After the completion of each rendezvous in the series, one of the threads may immediately request the next, allowing the other thread to execute some code before synchronising. A simple rendezvous is restricted to synchronisation, and does not involve ordinary computation steps.