Update rendered version of dissertation after rendering fixes
This commit is contained in:
Tony Garnock-Jones
parent
a8f69d9d43
commit
1bc47458bf
File diff suppressed because one or more lines are too long
|
|
@ -388,7 +388,7 @@
|
|||
<blockquote id="x_2_7_0_0_17">
|
||||
<p id="x_2_7_0_0_3">A <b>syndicate</b> is a self-organizing group of individuals, companies, corporations or entities formed to transact some specific business, to pursue or promote a shared interest.</p>
|
||||
<p class="align-right" id="x_2_7_0_0_4">— Wikipedia<label class="footnote-number" for="fn_2_19">19</label></p>
|
||||
<p id="x_2_7_0_0_5"><b><div class="error">UNKNOWN: ERROR:'(() ("inset" "Newpage clearpage"))</div></b></p>
|
||||
<p id="x_2_7_0_0_5"><b></b></p>
|
||||
<p id="x_2_7_0_0_10"><b>Syndicate</b>, n.
|
||||
<blockquote id="x_2_7_0_0_9">
|
||||
<p id="x_2_7_0_0_8">1. A group of individuals or organizations combined to promote a common interest.
|
||||
|
|
@ -2073,7 +2073,7 @@ box: taking on new-value 2
|
|||
(define timer-id (gensym 'sleep))
|
||||
(until (message (timer-expired timer-id _))
|
||||
(on-start (send! (set-timer timer-id (* sec 1000.0) 'relative)))))
|
||||
</code></pre></div><p id="x_6_5_0_0_61">An important consideration when programming with <tt>react/suspend</tt> and its derivatives is that the world may change during the time that an event-handler is “blocked”. For example, the following actor has no guarantee that the two messages it prints display the same value:<div class="error">UNKNOWN: ERROR:'(() ("inset" "Newpage pagebreak"))</div></p>
|
||||
</code></pre></div><p id="x_6_5_0_0_61">An important consideration when programming with <tt>react/suspend</tt> and its derivatives is that the world may change during the time that an event-handler is “blocked”. For example, the following actor has no guarantee that the two messages it prints display the same value:</p>
|
||||
<div class="verbatim" id="x_6_5_0_0_63">
|
||||
<pre class="verbatim" id="x_6_5_0_0_62"><code>(message-struct request-printout ())
|
||||
(message-struct increment-counter ())
|
||||
|
|
@ -2406,7 +2406,7 @@ T' & \textrm{if }(s\mapsto T')\in M\\
|
|||
T & \textrm{otherwise}
|
||||
\end{cases}
|
||||
\end{align*}
|
||||
</div><span class="plain-layout-boundary"></span><figcaption><span class="counter figure"><span>39</span></span><span class="figcaption-text"><span class="lyx-argument">The <span class="lyx-mathjax mathjax-inline">$\mathit{combine}$</span> function on assertion tries<span class="plain-layout-boundary"></span></span><a class="label-anchor" href="#fig:combine-function"></a>The <span class="lyx-mathjax mathjax-inline">$\mathit{combine}$</span> function for performing set operations on assertion tries.<span class="plain-layout-boundary"></span></span></figcaption><span class="plain-layout-boundary"></span></figure><p id="x_7_1_7_0_5">Algorithms for computing set union, intersection, and difference on well-formed tries carrying various kinds of data in their <span class="lyx-mathjax mathjax-inline">$\OK{}$</span> nodes can be formulated as specializations of a general <span class="lyx-mathjax mathjax-inline">$\COMBINEname$</span> function (figure <a class="cross-reference" href="#fig:combine-function">39</a>).</p><p id="x_7_1_7_0_6">We are careful to specify that <span class="lyx-mathjax mathjax-inline">$\COMBINEname$</span> may only be used with well-formed tries. This has an important consequence for the operation of the algorithm: during traversal of the two input tries, if one of the tries is an <span class="lyx-mathjax mathjax-inline">$\OK{}$</span> node, then at the same moment, the other trie is either an <span class="lyx-mathjax mathjax-inline">$\OK{}$</span> or an <span class="lyx-mathjax mathjax-inline">$\MT$</span> node. Since the function <span class="lyx-mathjax mathjax-inline">$f$</span> is called only when one or both of the tries is <span class="lyx-mathjax mathjax-inline">$\OK{}$</span>, we know that <span class="lyx-mathjax mathjax-inline">$f$</span> need only handle <span class="lyx-mathjax mathjax-inline">$\OK{}$</span> and <span class="lyx-mathjax mathjax-inline">$\MT$</span> inputs, leaving treatment of <span class="lyx-mathjax mathjax-inline">$\BRname$</span> nodes entirely to the <span class="lyx-mathjax mathjax-inline">$\COMBINEname$</span>/<span class="lyx-mathjax mathjax-inline">$\FOLDKEYS$</span> functions. The effect of <span class="lyx-mathjax mathjax-inline">$\COMBINEname$</span> is to walk the interior nodes of the tries it is given, delegating processing of leaf nodes to the <span class="lyx-mathjax mathjax-inline">$f$</span> passed in. In addition, <span class="lyx-mathjax mathjax-inline">$\COMBINEname$</span> itself produces a well-formed output, given a well-formed input and an <span class="lyx-mathjax mathjax-inline">$f$</span> that answers only <span class="lyx-mathjax mathjax-inline">$\OK{}$</span> or <span class="lyx-mathjax mathjax-inline">$\MT$</span> nodes.<div class="error">UNKNOWN: ERROR:'(() ("inset" "Newpage pagebreak"))</div></p><p id="x_7_1_7_0_7">The three set operations on <span class="lyx-mathjax mathjax-inline">$\SETTRIE$</span> instances are:</p><p id="x_7_1_7_0_12">
|
||||
</div><span class="plain-layout-boundary"></span><figcaption><span class="counter figure"><span>39</span></span><span class="figcaption-text"><span class="lyx-argument">The <span class="lyx-mathjax mathjax-inline">$\mathit{combine}$</span> function on assertion tries<span class="plain-layout-boundary"></span></span><a class="label-anchor" href="#fig:combine-function"></a>The <span class="lyx-mathjax mathjax-inline">$\mathit{combine}$</span> function for performing set operations on assertion tries.<span class="plain-layout-boundary"></span></span></figcaption><span class="plain-layout-boundary"></span></figure><p id="x_7_1_7_0_5">Algorithms for computing set union, intersection, and difference on well-formed tries carrying various kinds of data in their <span class="lyx-mathjax mathjax-inline">$\OK{}$</span> nodes can be formulated as specializations of a general <span class="lyx-mathjax mathjax-inline">$\COMBINEname$</span> function (figure <a class="cross-reference" href="#fig:combine-function">39</a>).</p><p id="x_7_1_7_0_6">We are careful to specify that <span class="lyx-mathjax mathjax-inline">$\COMBINEname$</span> may only be used with well-formed tries. This has an important consequence for the operation of the algorithm: during traversal of the two input tries, if one of the tries is an <span class="lyx-mathjax mathjax-inline">$\OK{}$</span> node, then at the same moment, the other trie is either an <span class="lyx-mathjax mathjax-inline">$\OK{}$</span> or an <span class="lyx-mathjax mathjax-inline">$\MT$</span> node. Since the function <span class="lyx-mathjax mathjax-inline">$f$</span> is called only when one or both of the tries is <span class="lyx-mathjax mathjax-inline">$\OK{}$</span>, we know that <span class="lyx-mathjax mathjax-inline">$f$</span> need only handle <span class="lyx-mathjax mathjax-inline">$\OK{}$</span> and <span class="lyx-mathjax mathjax-inline">$\MT$</span> inputs, leaving treatment of <span class="lyx-mathjax mathjax-inline">$\BRname$</span> nodes entirely to the <span class="lyx-mathjax mathjax-inline">$\COMBINEname$</span>/<span class="lyx-mathjax mathjax-inline">$\FOLDKEYS$</span> functions. The effect of <span class="lyx-mathjax mathjax-inline">$\COMBINEname$</span> is to walk the interior nodes of the tries it is given, delegating processing of leaf nodes to the <span class="lyx-mathjax mathjax-inline">$f$</span> passed in. In addition, <span class="lyx-mathjax mathjax-inline">$\COMBINEname$</span> itself produces a well-formed output, given a well-formed input and an <span class="lyx-mathjax mathjax-inline">$f$</span> that answers only <span class="lyx-mathjax mathjax-inline">$\OK{}$</span> or <span class="lyx-mathjax mathjax-inline">$\MT$</span> nodes.</p><p id="x_7_1_7_0_7">The three set operations on <span class="lyx-mathjax mathjax-inline">$\SETTRIE$</span> instances are:</p><p id="x_7_1_7_0_12">
|
||||
<div class="lyx-mathjax mathjax-display" id="x_7_1_7_0_8">\begin{align*}
|
||||
T_{1}\cup T_{2} & =\COMBINE{f_{\mathit{un}}}{id}{id}{T_{1}}{T_{2}}\\
|
||||
T_{1}\cap T_{2} & =\COMBINE{f_{\mathit{int}}}{(\lambda x.\MT)}{(\lambda x.\MT)}{T_{1}}{T_{2}}\\
|
||||
|
|
@ -2666,7 +2666,7 @@ k'([w,\dots],T') & =\TTAKE n{T'}{[v,\dots,(w,\dots)]}k
|
|||
</code></pre></div></div></tt><span class="plain-layout-boundary"></span></td></tr></table></div></tt></p><span class="plain-layout-boundary"></span><figcaption><span class="counter figure"><span>49</span></span><span class="figcaption-text"><span class="lyx-argument">Interfaces to imperative Racket dataflow library<span class="plain-layout-boundary"></span></span><a class="label-anchor" href="#fig:Interface-to-dataflow"></a>Runtime- and programmer-level interfaces to imperative Racket dataflow library<span class="plain-layout-boundary"></span></span></figcaption><span class="plain-layout-boundary"></span></figure><p id="x_7_3_3_0_20">Figure <a class="cross-reference" href="#fig:Interface-to-dataflow">49</a> sketches the interface to the Racket implementation of the dataflow library; full source code for the library is shown in appendix <a class="cross-reference" href="#APPENDIX:DATAFLOW">D</a>. The JavaScript implementation is similar. The <tt>current-dataflow-subject-id</tt> parameter records the identity of the currently-evaluating endpoint. Whenever a field is read, the runtime invokes <tt>dataflow-record-observation!</tt> with the identity of the field, thus recording a connection between the executing endpoint and the observed field. Whenever a field is updated, the runtime calls <tt>dataflow-record-damage!</tt>. Later in the behavior function of the actor, the runtime calls <tt>dataflow-repair-damage!</tt> with a <em>repair </em>procedure which, given an endpoint, calls its assertion-set recomputation procedure, collecting the results into a patch action which updates the overall assertion set of the actor in the dataspace. The synthetic endpoints generated by <tt>begin/dataflow</tt> are simply a special case, where the side-effects of the assertion-set procedure are the interesting part of the computation.</p><p id="x_7_3_3_0_21">As time goes by and fields change state, the precise set of fields that a given endpoint computation depends upon may change. The <tt>dataflow-repair-damage!</tt> procedure takes care to call <tt>dataflow-forget-subject!</tt> for each endpoint, just before invoking its repair procedure for that endpoint, in order to clear its previous memory of the endpoint's dependencies. The repair procedure, during its execution, records the currently-relevant set of dependencies for the endpoint. Finally, when an endpoint is removed from an actor as part of the facet shutdown process, <tt>dataflow-forget-subject!</tt> is used to remove obsolete dependency information for each removed endpoint.</p>
|
||||
<div class="footnote" id="fn_7_83"><span class="counter footnote-counter"><span>83</span></span><a href="http://knockoutjs.com/">http://knockoutjs.com/</a><span class="plain-layout-boundary"></span></div>
|
||||
<div class="footnote" id="fn_7_84"><span class="counter footnote-counter"><span>84</span></span><a href="https://docs.meteor.com/api/tracker.html">https://docs.meteor.com/api/tracker.html</a><span class="plain-layout-boundary"></span></div><p id="x_7_3_3_0_22">The simple “dataflow” system described here is neither a “sibling” of nor a “cousin” to reactive programming in the sense of <span class="citation citet"><a class="citation" id="cite-168" href="#bib-Bainomugisha2013"><span>Bainomugisha et al.<span class="parens"> (</span>2013<span class="parens">)</span></span></a></span>, or even dataflow in the sense of <span class="citation citet"><a class="citation" id="cite-169" href="#bib-Whiting1994"><span>Whiting and Pascoe<span class="parens"> (</span>1994<span class="parens">)</span></span></a></span>; rather, it is most similar to the simple <em>dependency tracking</em> approach to object-oriented reactive programming described by <span class="citation citet"><a class="citation" id="cite-170" href="#bib-Salvaneschi2014"><span>Salvaneschi and Mezini<span class="parens"> (</span>2014<span class="parens">)</span></span></a> <span class="citation-after">section 2.3</span></span>, and was in fact directly inspired by the dependency tracking of JavaScript frameworks like Knockout<label class="footnote-number" for="fn_7_83">83</label> <span class="citation citep">(<a class="citation" id="cite-171" href="#bib-Sanderson2010">Sanderson 2010</a>)</span> and Meteor.<label class="footnote-number" for="fn_7_84">84</label></p>
|
||||
<h4 id="x_7_4_0_0_1"><a name="toc_7.4"></a><span class="counter section"><span>7.4</span></span><span class="heading-text section"><a class="label-anchor" href="#sec:Programming-tools"></a><a name="sec:Programming-tools"></a>Programming tools</span></h4><p id="x_7_4_0_0_2">Because the prototype implementations of <span class="small-caps">Syndicate</span> are closely connected to the underlying formal models, the programmer is able to use concepts from the model in understanding the behavior of programs. Furthermore, points exist in the code implementing dataspace actors that correspond closely to the reduction rules given in chapter <a class="cross-reference" href="#CHAP:COMPUTATIONAL-MODEL-I:DATASPACES">4</a>, and each invocation of a dataspace's actor behavior function itself corresponds roughly to use of the <span class="lyx-mathjax mathjax-inline">$\RSchedule$</span> rule. This gives us an opportunity to record <em>trace events</em> capturing the behavior of the program in terms of the formal model. In turn, these events enable visualization of program execution.<div class="error">UNKNOWN: ERROR:'(() ("inset" "Newpage pagebreak"))</div></p><p id="x_7_4_0_0_3">The lifecycle of an action can trigger multiple trace log entries from the moment of its production to the moment the dataspace events it causes are delivered:</p>
|
||||
<h4 id="x_7_4_0_0_1"><a name="toc_7.4"></a><span class="counter section"><span>7.4</span></span><span class="heading-text section"><a class="label-anchor" href="#sec:Programming-tools"></a><a name="sec:Programming-tools"></a>Programming tools</span></h4><p id="x_7_4_0_0_2">Because the prototype implementations of <span class="small-caps">Syndicate</span> are closely connected to the underlying formal models, the programmer is able to use concepts from the model in understanding the behavior of programs. Furthermore, points exist in the code implementing dataspace actors that correspond closely to the reduction rules given in chapter <a class="cross-reference" href="#CHAP:COMPUTATIONAL-MODEL-I:DATASPACES">4</a>, and each invocation of a dataspace's actor behavior function itself corresponds roughly to use of the <span class="lyx-mathjax mathjax-inline">$\RSchedule$</span> rule. This gives us an opportunity to record <em>trace events</em> capturing the behavior of the program in terms of the formal model. In turn, these events enable visualization of program execution.</p><p id="x_7_4_0_0_3">The lifecycle of an action can trigger multiple trace log entries from the moment of its production to the moment the dataspace events it causes are delivered:</p>
|
||||
<ol id="x_7_4_0_0_9"><li id="x_7_4_0_0_4"><a class="label-anchor" href="#enu:action-produced"></a><a name="enu:action-produced"></a>an entry for the production of the action as a result from a behavior function;</li><li id="x_7_4_0_0_5"><a class="label-anchor" href="#enu:action-enqueued"></a><a name="enu:action-enqueued"></a>an entry for the moment the action is enqueued in the dataspace's pending-actions queue;</li><li id="x_7_4_0_0_6"><a class="label-anchor" href="#enu:action-interpreted"></a><a name="enu:action-interpreted"></a>an entry for its interpretation by the dataspace, which is the same moment that its effects are applied to the state of the dataspace, and the moment any resulting dataspace events are produced;</li><li id="x_7_4_0_0_7"><a class="label-anchor" href="#enu:event-enqueued"></a><a name="enu:event-enqueued"></a>an entry for the moment such events are enqueued for delivery to an actor; and</li><li id="x_7_4_0_0_8"><a class="label-anchor" href="#enu:event-delivered"></a><a name="enu:event-delivered"></a>an entry recording the final delivery of such events as input arguments to a behavior function.</li></ol><p id="x_7_4_0_0_10">Different <span class="small-caps">Syndicate</span> implementation strategies may combine some of these log entries together. For example, the prototype dataspace implementations combine entries <a class="cross-reference" href="#enu:action-produced">1</a> and <a class="cross-reference" href="#enu:action-enqueued">2</a> and entries <a class="cross-reference" href="#enu:event-enqueued">4</a> and <a class="cross-reference" href="#enu:event-delivered">5</a>. A hypothetical distributed implementation of <span class="small-caps">Syndicate</span> would likely maintain an observable distinction between all of the stages.</p><p id="x_7_4_0_0_11">Thus far, I have implemented three consumers of generated trace log entries. The first is a console-based logging facility which simply displays each entry as colorized text on the standard error file descriptor. The remainder of this section is devoted to discussion of the other two: an offline renderer of sequence diagrams and a live display of program activity.</p>
|
||||
<h5 id="x_7_4_1_0_1"><a name="toc_7.4.1"></a><span class="counter subsection"><span>7.4.1</span></span><span class="heading-text subsection"><a class="label-anchor" href="#subsec:Sequence-diagrams"></a><a name="subsec:Sequence-diagrams"></a>Sequence diagrams</span></h5>
|
||||
<figure id="x_7_4_1_0_3"><a name="fig:program-to-trace"></a>
|
||||
|
|
@ -2768,7 +2768,7 @@ k'([w,\dots],T') & =\TTAKE n{T'}{[v,\dots,(w,\dots)]}k
|
|||
(stop-when (message (delete-cell id))))))
|
||||
</code></pre></p><p id="x_8_3_0_0_19">The definition of an actor implementing Cell (lines 3–7) is embedded within the definition of the Cell Factory. Each time the Cell Factory receives a <tt>create-cell</tt> message (line 2), it spawns a new Cell instance (line 3), with a computed name incorporating the new cell's ID. Each Cell has a single <tt>value</tt> field (line 4), which is continuously published into the dataspace (line 5). Whenever an <tt>update-cell</tt> message is received, <tt>value</tt> is updated (line 6); recall that <span class="small-caps">Syndicate/rkt</span> fields are modeled as functions (see section <a class="cross-reference" href="#sec:rkt-Core-forms">6.4</a>). The Cell terminates itself when it receives an appropriately-addressed <tt>delete-cell</tt> message (line 7).</p></p><span class="halmos"></span></div><p id="x_8_3_0_0_22">Writers simply issue their requests by <tt>send!</tt>ing <tt>update-cell</tt> and <tt>delete-cell</tt> messages; Readers construct endpoints monitoring <tt>cell</tt> assertions.</p>
|
||||
<div class="theorem-like numbered example" id="x_8_3_0_0_27">
|
||||
<p id="x_8_3_0_0_26"><span class="counter numbered example"><span>8.7</span></span><a class="label-anchor" href="#example:rkt-mutable-cell-monitor"></a><a name="example:rkt-mutable-cell-monitor"></a>The following procedure spawns a simple actor that monitors the changing value of a cell:<div class="error">UNKNOWN: ERROR:'(() ("inset" "Newpage pagebreak"))</div><p id="x_8_3_0_0_24">
|
||||
<p id="x_8_3_0_0_26"><span class="counter numbered example"><span>8.7</span></span><a class="label-anchor" href="#example:rkt-mutable-cell-monitor"></a><a name="example:rkt-mutable-cell-monitor"></a>The following procedure spawns a simple actor that monitors the changing value of a cell:<p id="x_8_3_0_0_24">
|
||||
<pre class="listing" id="x_8_3_0_0_23"><code>(define (spawn-cell-monitor id)
|
||||
(spawn #:name (list 'cell-monitor id)
|
||||
(on (asserted (cell id $value))
|
||||
|
|
@ -3066,22 +3066,7 @@ ancestor(A, B) :- parent(A, C), ancestor(C, B).
|
|||
(printf "Socket is ready and will forward datagrams.\n")))
|
||||
</code></pre></p></p><span class="halmos"></span></div><p id="x_8_5_6_0_43">The UDP socket protocol was designed originally for our implementation of Network Calculus, which explains its awkward use of advertisement in place of a more straightforward <tt>udp-socket-ready</tt> assertion or similar. While the protocol of <em>interest</em> (protocol <a class="cross-reference" href="#protocol:interest">8.2</a>) is essential to the dataspace model, the protocol of <em>advertisement</em> appears to have much more limited applicability.</p><p id="x_8_5_6_0_44">Despite this limited applicability, the general interpretation of the protocol remains of interest. Taking <tt>(advertise </tt><span class="lyx-mathjax mathjax-inline">$c$</span><tt>)</tt> to mean “eventually <span class="lyx-mathjax mathjax-inline">$c$</span>” or “possibly <span class="lyx-mathjax mathjax-inline">$c$</span>” suggests a connection with the modal logic <span class="lyx-mathjax mathjax-inline">$\diamond$</span> operator <span class="citation citep">(<a class="citation" id="cite-186" href="#bib-Manna1991">Manna and Pnueli 1991</a>; <a class="citation" id="cite-187" href="#bib-VanDitmarsch">van Ditmarsch, van der Hoek and Kooi 2017</a>)</span>. We have seen that <tt>(during</tt> <em>P </em><tt>(assert </tt><em>E</em><tt>))</tt> reads as <span class="lyx-mathjax mathjax-inline">$P\implies E$</span>; perhaps it is, in truth, closer to some interpretation of <span class="lyx-mathjax mathjax-inline">$\square(P\implies E)$</span>. It remains future work to explore this connection further.</p><p id="x_8_5_6_0_45">Finally, while advertisement has limited use within domain-specific protocols, it is of great benefit in the setting of publish/subscribe middleware, where it is used to optimize message routing overlays <span class="citation citep">(<a class="citation" id="cite-188" href="#bib-Carzaniga2000">Carzaniga, Rosenblum and Wolf 2000</a>; <a class="citation" id="cite-189" href="#bib-Pietzuch2002">Pietzuch and Bacon 2002</a>; <a class="citation" id="cite-190" href="#bib-Jayaram2011">Jayaram and Eugster 2011</a>; <a class="citation" id="cite-191" href="#bib-Martins2010">Martins and Duarte 2010</a>; <a class="citation" id="cite-192" href="#bib-Eugster2003">Eugster et al. 2003</a>)</span>. Automatic, conservative overapproximation of the assertions an actor may produce could lead to efficiency gains in <span class="small-caps">Syndicate</span> implementations, which may become particularly useful in any attempt to scale the design to distributed systems.</p>
|
||||
<h4 id="x_8_6_0_0_1"><a name="toc_8.6"></a><span class="counter section"><span>8.6</span></span><span class="heading-text section"><a class="label-anchor" href="#sec:Dependency-resolution-and-Startup"></a><a name="sec:Dependency-resolution-and-Startup"></a>Dependency resolution and lazy startup: Service presence</span></h4>
|
||||
<div class="footnote" id="fn_8_95"><span class="counter footnote-counter"><span>95</span></span>At least, this is the ideal.<span class="plain-layout-boundary"></span></div><p id="x_8_6_0_0_2">Unix systems start up their system service programs in an order which guarantees that the dependencies of each program are all ready before that program is started.<label class="footnote-number" for="fn_8_95">95</label> Many current Unix distributions manually schedule the system startup process. Because it is a complex process, such manually-arranged boot sequences tend to be strictly sequential. Other distributions are starting to use tools like <tt>make</tt> both to automatically compute a suitable startup ordering and to automatically parallelize system startup.</p><p id="x_8_6_0_0_3">With <span class="small-caps">Syndicate</span>, we can both ensure correct ordering and automatically parallelize<div class="error">UNKNOWN: ERROR:'(()
|
||||
("inset"
|
||||
"Note Note"
|
||||
"status open"
|
||||
(layout-group
|
||||
"Plain Layout"
|
||||
("layout"
|
||||
"Plain Layout"
|
||||
(foot
|
||||
(layout-group
|
||||
"Plain Layout"
|
||||
("layout"
|
||||
"Plain Layout"
|
||||
"Absent true parallelism, the best we can do is expose latent "
|
||||
(emph "concurrency")
|
||||
" in a startup schedule.")))))))</div> system startup where possible, by taking advantage of <em>service presence</em> information <span class="citation citep">(<a class="citation" id="cite-193" href="#bib-Konieczny2009">Konieczny et al. 2009</a>)</span>. Programs offer their services via endpoints; clients of these services interpret the presence of these endpoints as service availability and react, offering up their own services in turn when a service they depend upon becomes available.</p><p id="x_8_6_0_0_4">Service availability must, at some level, be expressed in a concrete style, with endpoints interacting with their environment in terms of the actual messages of the protocols supported by the service. However, availability may also be expressed at a more abstract level. Consumers of a service may detect service presence by directly observing the presence of endpoints engaging in a protocol of interest, or by observing the presence of assertions describing the service more abstractly. The former corresponds to a kind of <em>structural</em> presence indicator, while the latter corresponds to a form of <em>nominal</em> service presence.</p>
|
||||
<div class="footnote" id="fn_8_95"><span class="counter footnote-counter"><span>95</span></span>At least, this is the ideal.<span class="plain-layout-boundary"></span></div><p id="x_8_6_0_0_2">Unix systems start up their system service programs in an order which guarantees that the dependencies of each program are all ready before that program is started.<label class="footnote-number" for="fn_8_95">95</label> Many current Unix distributions manually schedule the system startup process. Because it is a complex process, such manually-arranged boot sequences tend to be strictly sequential. Other distributions are starting to use tools like <tt>make</tt> both to automatically compute a suitable startup ordering and to automatically parallelize system startup.</p><p id="x_8_6_0_0_3">With <span class="small-caps">Syndicate</span>, we can both ensure correct ordering and automatically parallelize system startup where possible, by taking advantage of <em>service presence</em> information <span class="citation citep">(<a class="citation" id="cite-193" href="#bib-Konieczny2009">Konieczny et al. 2009</a>)</span>. Programs offer their services via endpoints; clients of these services interpret the presence of these endpoints as service availability and react, offering up their own services in turn when a service they depend upon becomes available.</p><p id="x_8_6_0_0_4">Service availability must, at some level, be expressed in a concrete style, with endpoints interacting with their environment in terms of the actual messages of the protocols supported by the service. However, availability may also be expressed at a more abstract level. Consumers of a service may detect service presence by directly observing the presence of endpoints engaging in a protocol of interest, or by observing the presence of assertions describing the service more abstractly. The former corresponds to a kind of <em>structural</em> presence indicator, while the latter corresponds to a form of <em>nominal</em> service presence.</p>
|
||||
<figure id="x_8_6_0_0_6"><a name="fig:Service-dependency-resolution"></a>
|
||||
<pre class="listing" id="x_8_6_0_0_5"><code>(assertion-struct service-ready (name))
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue