Link Search Menu Expand Document
CBS-beta
\( % 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 : Synchronising.cbs | PLAIN | PDF

OUTLINE

Thread synchronisation

\[\begin{align*} [ \ \textsf{Syncs } \ & \textsf{} \\ \KEY{Datatype} \quad & \NAMEREF{syncs} \\ \KEY{Funcon} \quad & \NAMEREF{sync-create} \\ \KEY{Funcon} \quad & \NAMEREF{sync-feature} \\ \KEY{Funcon} \quad & \NAMEREF{is-sync-feature} \\ \textsf{Sync} \ & \textsf{features} \\ \KEY{Datatype} \quad & \NAMEREF{sync-features} \\ \KEY{Funcon} \quad & \NAMEREF{sync-waiting-list} \\ \KEY{Funcon} \quad & \NAMEREF{sync-held} \\ \KEY{Funcon} \quad & \NAMEREF{sync-holder} \\ \KEY{Funcon} \quad & \NAMEREF{sync-count} \\ \KEY{Funcon} \quad & \NAMEREF{sync-feature-create} \ ] \end{align*}\]

Thread synchronisation can be supported in many different ways: semaphores, exclusive and shared locks, conditions, barriers, rendezvous, spin-locks, etc. They generally involve the execution of one or more threads being blocked while they wait for some synchronisation request to be granted by a synchroniser due to a step by some unblocked thread. Blocking may involve thread suspension or repeated requests.

In general, the effect of granting a sync needs to be atomic, to preclude preemption. However, the execution of the thread that caused the request to be granted might continue without yielding, thereby delaying the resumed execution of the requesting thread. Synchronisation ensures that the executions of two or more threads are at particular points at the same time, but it does not require their next steps to be simultaneous.

Syncs are mutable structures that map sync features to variables (some fields may be constant values). Inspecting and updating sync features should be atomic, in case threads are preemptible.

Syncs

A sync is formed from its features:

\[\begin{align*} \KEY{Datatype} \quad \NAMEDECL{syncs} \ ::= \ & \NAMEDECL{sync}( \_ : \NAMEREF{sync-feature-maps}) \end{align*}\]

\(\SHADE{\NAMEREF{sync-create} ( \VAR{M}\PLUS )}\) checks that the specified features are distinct. (It could also check required feature constraints.)

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{sync-create}( \VAR{M}\PLUS : \NAMEREF{sync-feature-maps}\PLUS) : \TO \NAMEREF{syncs} \\&\quad \leadsto \NAMEREF{sync} \ \NAMEHYPER{../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \ \NAMEHYPER{../../../../Funcons-beta/Values/Composite}{Maps}{map-unite} \ \VAR{M}\PLUS \end{align*}\]

\(\SHADE{\NAMEREF{sync-feature} ( \VAR{SY}, \VAR{SF} )}\) selects the feature \(\SHADE{\VAR{SF}}\) from \(\SHADE{\VAR{SY}}\):

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{sync-feature}( \_ : \NAMEREF{syncs}, \_ : \NAMEREF{sync-features}) : \TO \NAMEHYPER{../../../../Funcons-beta/Values}{Value-Types}{values} \\ \KEY{Rule} \quad & \NAMEREF{sync-feature} ( \NAMEREF{sync} ( \VAR{SFM} : \NAMEREF{sync-feature-maps} ), \VAR{SF} : \NAMEREF{sync-features} ) \leadsto \\&\quad \NAMEHYPER{../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \ \NAMEHYPER{../../../../Funcons-beta/Values/Composite}{Maps}{map-lookup} ( \VAR{SFM}, \VAR{SF} ) \end{align*}\]

\(\SHADE{\NAMEREF{is-sync-feature} ( \VAR{SY}, \VAR{SF} )}\) tests whether \(\SHADE{\VAR{SY}}\) has the feature \(\SHADE{\VAR{SF}}\):

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{is-sync-feature}( \_ : \NAMEREF{syncs}, \_ : \NAMEREF{sync-features}) : \TO \NAMEHYPER{../../../../Funcons-beta/Values}{Value-Types}{values} \\ \KEY{Rule} \quad & \NAMEREF{is-sync-feature} ( \NAMEREF{sync} ( \VAR{SFM} : \NAMEREF{sync-feature-maps} ), \VAR{SF} : \NAMEREF{sync-features} ) \leadsto \\&\quad \NAMEHYPER{../../../../Funcons-beta/Values/Composite}{Sets}{is-in-set} ( \VAR{SF}, \NAMEHYPER{../../../../Funcons-beta/Values/Composite}{Maps}{dom} \ \VAR{SFM} ) \end{align*}\]

Sync features

Combinations of the following features support various kinds of locks and notifications.

\[\begin{align*} \KEY{Datatype} \quad \NAMEDECL{sync-features} \ ::= \ & \NAMEDECL{sync-waiting-list} \\ \ \mid \ & \ \NAMEDECL{sync-held} \\ \ \mid \ & \ \NAMEDECL{sync-holder} \\ \ \mid \ & \ \NAMEDECL{sync-count} \end{align*}\] \[\begin{align*} \KEY{Auxiliary Type} \quad & \NAMEDECL{sync-feature-maps} \leadsto \NAMEHYPER{../../../../Funcons-beta/Values/Composite}{Maps}{maps} ( \NAMEREF{sync-features}, \NAMEHYPER{../../../../Funcons-beta/Values}{Value-Types}{values} ) \end{align*}\]

A field for each feature is created independently:

\[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{sync-feature-create}( \_ : \NAMEREF{sync-features}) : \TO \NAMEREF{sync-feature-maps} \end{align*}\]

\(\SHADE{\NAMEREF{sync-waiting-list}}\) stores pending requests in the order of receipt, together with the requesting thread-ids:

\[\begin{align*} \KEY{Rule} \quad & \NAMEREF{sync-feature-create} \ \NAMEREF{sync-waiting-list} \leadsto \\&\quad \{ \NAMEREF{sync-waiting-list} \mapsto \\&\quad\quad\quad \NAMEHYPER{../../../../Funcons-beta/Computations/Normal}{Storing}{allocate-initialised-variable} ( \NAMEHYPER{../../../../Funcons-beta/Values/Composite}{Lists}{lists} ( \NAMEHYPER{../../../../Funcons-beta/Values}{Value-Types}{values} ), [ \ ] ) \} \end{align*}\]

\(\SHADE{\NAMEREF{sync-held}}\) stores whether a lock is currently held:

\[\begin{align*} \KEY{Rule} \quad & \NAMEREF{sync-feature-create} \ \NAMEREF{sync-held} \leadsto \\&\quad \{ \NAMEREF{sync-held} \mapsto \\&\quad\quad\quad \NAMEHYPER{../../../../Funcons-beta/Computations/Normal}{Storing}{allocate-initialised-variable} ( \NAMEHYPER{../../../../Funcons-beta/Values/Primitive}{Booleans}{booleans}, \NAMEHYPER{../../../../Funcons-beta/Values/Primitive}{Booleans}{false} ) \} \end{align*}\]

\(\SHADE{\NAMEREF{sync-holder}}\) stores the current holder of a lock, if any:

\[\begin{align*} \KEY{Rule} \quad & \NAMEREF{sync-feature-create} \ \NAMEREF{sync-holder} \leadsto \\&\quad \{ \NAMEREF{sync-holder} \mapsto \\&\quad\quad\quad \NAMEHYPER{../../../../Funcons-beta/Computations/Normal}{Storing}{allocate-variable} ( \NAMEHYPER{../.}{Multithreading}{thread-ids} ) \} \end{align*}\]

\(\SHADE{\NAMEREF{sync-count}}\) stores a counter. Different kinds of locks and notifications use the counter in different ways, e.g., shared locks use it for the number of threads currently holding the lock:

\[\begin{align*} \KEY{Rule} \quad & \NAMEREF{sync-feature-create} \ \NAMEREF{sync-count} \leadsto \\&\quad \{ \NAMEREF{sync-count} \mapsto \\&\quad\quad\quad \NAMEHYPER{../../../../Funcons-beta/Computations/Normal}{Storing}{allocate-initialised-variable} ( \NAMEHYPER{../../../../Funcons-beta/Values/Primitive}{Integers}{nats}, 0 ) \} \end{align*}\]

\(\SHADE{\NAMEREF{sync-waiting-list-add} ( \VAR{SY}, \VAR{V} )}\) adds \(\SHADE{\VAR{V}}\) to the waiting-list of \(\SHADE{\VAR{SY}}\):

\[\begin{align*} \KEY{Auxiliary Funcon} \quad & \NAMEDECL{sync-waiting-list-add}( \VAR{SY} : \NAMEREF{syncs}, \VAR{V} : \NAMEHYPER{../../../../Funcons-beta/Values}{Value-Types}{values}) : \TO \NAMEHYPER{../../../../Funcons-beta/Values/Primitive}{Null}{null-type} \\&\quad \leadsto \NAMEHYPER{../../../../Funcons-beta/Computations/Normal}{Storing}{assign} ( \\&\quad\quad\quad\quad \NAMEREF{sync-feature} ( \VAR{SY}, \NAMEREF{sync-waiting-list} ), \\&\quad\quad\quad\quad \NAMEHYPER{../../../../Funcons-beta/Values/Composite}{Lists}{list-append} ( \NAMEHYPER{../../../../Funcons-beta/Computations/Normal}{Storing}{assigned} \ \NAMEREF{sync-feature} ( \VAR{SY}, \NAMEREF{sync-waiting-list} ), [ \VAR{V} ] ) ) \end{align*}\]

\(\SHADE{\NAMEREF{sync-waiting-list-head-remove} ( \VAR{SY} )}\) removes the first value from the waiting-list of \(\SHADE{\VAR{SY}}\):

\[\begin{align*} \KEY{Auxiliary Funcon} \quad & \NAMEDECL{sync-waiting-list-head-remove}( \VAR{SY} : \NAMEREF{syncs}) : \TO \NAMEHYPER{../../../../Funcons-beta/Values}{Value-Types}{values} \\&\quad \leadsto \NAMEHYPER{../../../../Funcons-beta/Computations/Normal}{Giving}{give} ( \\&\quad\quad\quad\quad \NAMEHYPER{../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \ \NAMEHYPER{../../../../Funcons-beta/Values/Composite}{Lists}{list-head} \ \NAMEHYPER{../../../../Funcons-beta/Computations/Normal}{Storing}{assigned} \ \NAMEREF{sync-feature} ( \VAR{SY}, \NAMEREF{sync-waiting-list} ), \\&\quad\quad\quad\quad \NAMEHYPER{../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../Funcons-beta/Computations/Normal}{Storing}{assign} ( \\&\quad\quad\quad\quad\quad\quad \NAMEREF{sync-feature} ( \VAR{SY}, \NAMEREF{sync-waiting-list} ), \\&\quad\quad\quad\quad\quad\quad \NAMEHYPER{../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \ \NAMEHYPER{../../../../Funcons-beta/Values/Composite}{Lists}{list-tail} \ \NAMEHYPER{../../../../Funcons-beta/Computations/Normal}{Storing}{assigned} \ \NAMEREF{sync-feature} ( \VAR{SY}, \NAMEREF{sync-waiting-list} ) ), \\&\quad\quad\quad\quad\quad \NAMEHYPER{../../../../Funcons-beta/Computations/Normal}{Giving}{given} ) ) \end{align*}\]

Various kinds of locks and notifications are represented by sync feature maps, together with funcons that (atomically) inspect and update them accordngly.

From the PLanCompS Project CBS-beta issues… Suggest an improvement…

← ↑

Table of contents