From 1bc47458bfb41bf81c9bf28e6860f1d5e3a7d6eb Mon Sep 17 00:00:00 2001 From: Tony Garnock-Jones Date: Fri, 2 Feb 2018 10:18:01 +0000 Subject: [PATCH] Update rendered version of dissertation after rendering fixes --- tonyg-dissertation/html/index.html | 27 +++++------------------ tonyg-dissertation/html/index.nomath.html | 27 +++++------------------ 2 files changed, 12 insertions(+), 42 deletions(-) diff --git a/tonyg-dissertation/html/index.html b/tonyg-dissertation/html/index.html index 37cf796..6a62337 100644 --- a/tonyg-dissertation/html/index.html +++ b/tonyg-dissertation/html/index.html @@ -511,7 +511,7 @@

A syndicate is a self-organizing group of individuals, companies, corporations or entities formed to transact some specific business, to pursue or promote a shared interest.

— Wikipedia

-

UNKNOWN: ERROR:'(() ("inset" "Newpage clearpage"))

+

Syndicate, n.

1. A group of individuals or organizations combined to promote a common interest. @@ -2214,7 +2214,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))))) -

An important consideration when programming with react/suspend 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:

UNKNOWN: ERROR:'(() ("inset" "Newpage pagebreak"))

+

An important consideration when programming with react/suspend 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:

(message-struct request-printout ())
 (message-struct increment-counter ())
@@ -2547,7 +2547,7 @@ T' & \textrm{if }(s\mapsto T')\in M\\
 T & \textrm{otherwise}
 \end{cases}
 \end{align*}">
-
39The function on assertion triesThe function for performing set operations on assertion tries.

Algorithms for computing set union, intersection, and difference on well-formed tries carrying various kinds of data in their nodes can be formulated as specializations of a general function (figure 39).

We are careful to specify that 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 node, then at the same moment, the other trie is either an or an node. Since the function is called only when one or both of the tries is , we know that need only handle and inputs, leaving treatment of nodes entirely to the / functions. The effect of is to walk the interior nodes of the tries it is given, delegating processing of leaf nodes to the passed in. In addition, itself produces a well-formed output, given a well-formed input and an that answers only or nodes.

UNKNOWN: ERROR:'(() ("inset" "Newpage pagebreak"))

The three set operations on instances are:

+

39The function on assertion triesThe function for performing set operations on assertion tries.

Algorithms for computing set union, intersection, and difference on well-formed tries carrying various kinds of data in their nodes can be formulated as specializations of a general function (figure 39).

We are careful to specify that 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 node, then at the same moment, the other trie is either an or an node. Since the function is called only when one or both of the tries is , we know that need only handle and inputs, leaving treatment of nodes entirely to the / functions. The effect of is to walk the interior nodes of the tries it is given, delegating processing of leaf nodes to the passed in. In addition, itself produces a well-formed output, given a well-formed input and an that answers only or nodes.

The three set operations on instances are:

49Interfaces to imperative Racket dataflow libraryRuntime- and programmer-level interfaces to imperative Racket dataflow library

Figure 49 sketches the interface to the Racket implementation of the dataflow library; full source code for the library is shown in appendix D. The JavaScript implementation is similar. The current-dataflow-subject-id parameter records the identity of the currently-evaluating endpoint. Whenever a field is read, the runtime invokes dataflow-record-observation! 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 dataflow-record-damage!. Later in the behavior function of the actor, the runtime calls dataflow-repair-damage! with a repair 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 begin/dataflow are simply a special case, where the side-effects of the assertion-set procedure are the interesting part of the computation.

As time goes by and fields change state, the precise set of fields that a given endpoint computation depends upon may change. The dataflow-repair-damage! procedure takes care to call dataflow-forget-subject! 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, dataflow-forget-subject! is used to remove obsolete dependency information for each removed endpoint.

The simple “dataflow” system described here is neither a “sibling” of nor a “cousin” to reactive programming in the sense of Bainomugisha et al. (2013), or even dataflow in the sense of Whiting and Pascoe (1994); rather, it is most similar to the simple dependency tracking approach to object-oriented reactive programming described by Salvaneschi and Mezini (2014) section 2.3, and was in fact directly inspired by the dependency tracking of JavaScript frameworks like Knockout (Sanderson 2010) and Meteor.

-

7.4Programming tools

Because the prototype implementations of Syndicate 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 4, and each invocation of a dataspace's actor behavior function itself corresponds roughly to use of the rule. This gives us an opportunity to record trace events capturing the behavior of the program in terms of the formal model. In turn, these events enable visualization of program execution.

UNKNOWN: ERROR:'(() ("inset" "Newpage pagebreak"))

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:

+

7.4Programming tools

Because the prototype implementations of Syndicate 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 4, and each invocation of a dataspace's actor behavior function itself corresponds roughly to use of the rule. This gives us an opportunity to record trace events capturing the behavior of the program in terms of the formal model. In turn, these events enable visualization of program execution.

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:

  1. an entry for the production of the action as a result from a behavior function;
  2. an entry for the moment the action is enqueued in the dataspace's pending-actions queue;
  3. 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;
  4. an entry for the moment such events are enqueued for delivery to an actor; and
  5. an entry recording the final delivery of such events as input arguments to a behavior function.

Different Syndicate implementation strategies may combine some of these log entries together. For example, the prototype dataspace implementations combine entries 1 and 2 and entries 4 and 5. A hypothetical distributed implementation of Syndicate would likely maintain an observable distinction between all of the stages.

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.

7.4.1Sequence diagrams
@@ -2909,7 +2909,7 @@ k'([w,\dots],T') & =\TTAKE n{T'}{[v,\dots,(w,\dots)]}k (stop-when (message (delete-cell id))))))

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 create-cell 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 value field (line 4), which is continuously published into the dataspace (line 5). Whenever an update-cell message is received, value is updated (line 6); recall that Syndicate/rkt fields are modeled as functions (see section 6.4). The Cell terminates itself when it receives an appropriately-addressed delete-cell message (line 7).

Writers simply issue their requests by send!ing update-cell and delete-cell messages; Readers construct endpoints monitoring cell assertions.

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 udp-socket-ready assertion or similar. While the protocol of interest (protocol 8.2) is essential to the dataspace model, the protocol of advertisement appears to have much more limited applicability.

Despite this limited applicability, the general interpretation of the protocol remains of interest. Taking (advertise ) to mean “eventually ” or “possibly ” suggests a connection with the modal logic operator (Manna and Pnueli 1991; van Ditmarsch, van der Hoek and Kooi 2017). We have seen that (during P (assert E)) reads as ; perhaps it is, in truth, closer to some interpretation of . It remains future work to explore this connection further.

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 (Carzaniga, Rosenblum and Wolf 2000; Pietzuch and Bacon 2002; Jayaram and Eugster 2011; Martins and Duarte 2010; Eugster et al. 2003). Automatic, conservative overapproximation of the assertions an actor may produce could lead to efficiency gains in Syndicate implementations, which may become particularly useful in any attempt to scale the design to distributed systems.

8.6Dependency resolution and lazy startup: Service presence

-
95At least, this is the ideal.

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. 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 make both to automatically compute a suitable startup ordering and to automatically parallelize system startup.

With Syndicate, we can both ensure correct ordering and automatically parallelize

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.")))))))
system startup where possible, by taking advantage of service presence information (Konieczny et al. 2009). 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.

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 structural presence indicator, while the latter corresponds to a form of nominal service presence.

+
95At least, this is the ideal.

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. 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 make both to automatically compute a suitable startup ordering and to automatically parallelize system startup.

With Syndicate, we can both ensure correct ordering and automatically parallelize system startup where possible, by taking advantage of service presence information (Konieczny et al. 2009). 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.

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 structural presence indicator, while the latter corresponds to a form of nominal service presence.

(assertion-struct service-ready (name))
 
diff --git a/tonyg-dissertation/html/index.nomath.html b/tonyg-dissertation/html/index.nomath.html
index 3681eea..a63f86e 100644
--- a/tonyg-dissertation/html/index.nomath.html
+++ b/tonyg-dissertation/html/index.nomath.html
@@ -388,7 +388,7 @@
 

 
A syndicate is a self-organizing group of individuals, companies, corporations or entities formed to transact some specific business, to pursue or promote a shared interest.

 
— Wikipedia

-
UNKNOWN: ERROR:'(() ("inset" "Newpage clearpage"))

+

 
Syndicate, n.
 

 
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)))))
-

An important consideration when programming with react/suspend 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:

UNKNOWN: ERROR:'(() ("inset" "Newpage pagebreak"))

+

An important consideration when programming with react/suspend 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:

(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*}
-
39The $\mathit{combine}$ function on assertion triesThe $\mathit{combine}$ function for performing set operations on assertion tries.

Algorithms for computing set union, intersection, and difference on well-formed tries carrying various kinds of data in their $\OK{}$ nodes can be formulated as specializations of a general $\COMBINEname$ function (figure 39).

We are careful to specify that $\COMBINEname$ 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 $\OK{}$ node, then at the same moment, the other trie is either an $\OK{}$ or an $\MT$ node. Since the function $f$ is called only when one or both of the tries is $\OK{}$, we know that $f$ need only handle $\OK{}$ and $\MT$ inputs, leaving treatment of $\BRname$ nodes entirely to the $\COMBINEname$/$\FOLDKEYS$ functions. The effect of $\COMBINEname$ is to walk the interior nodes of the tries it is given, delegating processing of leaf nodes to the $f$ passed in. In addition, $\COMBINEname$ itself produces a well-formed output, given a well-formed input and an $f$ that answers only $\OK{}$ or $\MT$ nodes.

UNKNOWN: ERROR:'(() ("inset" "Newpage pagebreak"))

The three set operations on $\SETTRIE$ instances are:

+

39The $\mathit{combine}$ function on assertion triesThe $\mathit{combine}$ function for performing set operations on assertion tries.

Algorithms for computing set union, intersection, and difference on well-formed tries carrying various kinds of data in their $\OK{}$ nodes can be formulated as specializations of a general $\COMBINEname$ function (figure 39).

We are careful to specify that $\COMBINEname$ 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 $\OK{}$ node, then at the same moment, the other trie is either an $\OK{}$ or an $\MT$ node. Since the function $f$ is called only when one or both of the tries is $\OK{}$, we know that $f$ need only handle $\OK{}$ and $\MT$ inputs, leaving treatment of $\BRname$ nodes entirely to the $\COMBINEname$/$\FOLDKEYS$ functions. The effect of $\COMBINEname$ is to walk the interior nodes of the tries it is given, delegating processing of leaf nodes to the $f$ passed in. In addition, $\COMBINEname$ itself produces a well-formed output, given a well-formed input and an $f$ that answers only $\OK{}$ or $\MT$ nodes.

The three set operations on $\SETTRIE$ instances are:

\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

49Interfaces to imperative Racket dataflow libraryRuntime- and programmer-level interfaces to imperative Racket dataflow library

Figure 49 sketches the interface to the Racket implementation of the dataflow library; full source code for the library is shown in appendix D. The JavaScript implementation is similar. The current-dataflow-subject-id parameter records the identity of the currently-evaluating endpoint. Whenever a field is read, the runtime invokes dataflow-record-observation! 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 dataflow-record-damage!. Later in the behavior function of the actor, the runtime calls dataflow-repair-damage! with a repair 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 begin/dataflow are simply a special case, where the side-effects of the assertion-set procedure are the interesting part of the computation.

As time goes by and fields change state, the precise set of fields that a given endpoint computation depends upon may change. The dataflow-repair-damage! procedure takes care to call dataflow-forget-subject! 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, dataflow-forget-subject! is used to remove obsolete dependency information for each removed endpoint.

The simple “dataflow” system described here is neither a “sibling” of nor a “cousin” to reactive programming in the sense of Bainomugisha et al. (2013), or even dataflow in the sense of Whiting and Pascoe (1994); rather, it is most similar to the simple dependency tracking approach to object-oriented reactive programming described by Salvaneschi and Mezini (2014) section 2.3, and was in fact directly inspired by the dependency tracking of JavaScript frameworks like Knockout (Sanderson 2010) and Meteor.

-

7.4Programming tools

Because the prototype implementations of Syndicate 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 4, and each invocation of a dataspace's actor behavior function itself corresponds roughly to use of the $\RSchedule$ rule. This gives us an opportunity to record trace events capturing the behavior of the program in terms of the formal model. In turn, these events enable visualization of program execution.

UNKNOWN: ERROR:'(() ("inset" "Newpage pagebreak"))

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:

+

7.4Programming tools

Because the prototype implementations of Syndicate 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 4, and each invocation of a dataspace's actor behavior function itself corresponds roughly to use of the $\RSchedule$ rule. This gives us an opportunity to record trace events capturing the behavior of the program in terms of the formal model. In turn, these events enable visualization of program execution.

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:

  1. an entry for the production of the action as a result from a behavior function;
  2. an entry for the moment the action is enqueued in the dataspace's pending-actions queue;
  3. 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;
  4. an entry for the moment such events are enqueued for delivery to an actor; and
  5. an entry recording the final delivery of such events as input arguments to a behavior function.

Different Syndicate implementation strategies may combine some of these log entries together. For example, the prototype dataspace implementations combine entries 1 and 2 and entries 4 and 5. A hypothetical distributed implementation of Syndicate would likely maintain an observable distinction between all of the stages.

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.

7.4.1Sequence diagrams
@@ -2768,7 +2768,7 @@ k'([w,\dots],T') & =\TTAKE n{T'}{[v,\dots,(w,\dots)]}k (stop-when (message (delete-cell id))))))

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 create-cell 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 value field (line 4), which is continuously published into the dataspace (line 5). Whenever an update-cell message is received, value is updated (line 6); recall that Syndicate/rkt fields are modeled as functions (see section 6.4). The Cell terminates itself when it receives an appropriately-addressed delete-cell message (line 7).

Writers simply issue their requests by send!ing update-cell and delete-cell messages; Readers construct endpoints monitoring cell assertions.

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 udp-socket-ready assertion or similar. While the protocol of interest (protocol 8.2) is essential to the dataspace model, the protocol of advertisement appears to have much more limited applicability.

Despite this limited applicability, the general interpretation of the protocol remains of interest. Taking (advertise $c$) to mean “eventually $c$” or “possibly $c$” suggests a connection with the modal logic $\diamond$ operator (Manna and Pnueli 1991; van Ditmarsch, van der Hoek and Kooi 2017). We have seen that (during P (assert E)) reads as $P\implies E$; perhaps it is, in truth, closer to some interpretation of $\square(P\implies E)$. It remains future work to explore this connection further.

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 (Carzaniga, Rosenblum and Wolf 2000; Pietzuch and Bacon 2002; Jayaram and Eugster 2011; Martins and Duarte 2010; Eugster et al. 2003). Automatic, conservative overapproximation of the assertions an actor may produce could lead to efficiency gains in Syndicate implementations, which may become particularly useful in any attempt to scale the design to distributed systems.

8.6Dependency resolution and lazy startup: Service presence

-
95At least, this is the ideal.

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. 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 make both to automatically compute a suitable startup ordering and to automatically parallelize system startup.

With Syndicate, we can both ensure correct ordering and automatically parallelize

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.")))))))
system startup where possible, by taking advantage of service presence information (Konieczny et al. 2009). 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.

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 structural presence indicator, while the latter corresponds to a form of nominal service presence.

+
95At least, this is the ideal.

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. 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 make both to automatically compute a suitable startup ordering and to automatically parallelize system startup.

With Syndicate, we can both ensure correct ordering and automatically parallelize system startup where possible, by taking advantage of service presence information (Konieczny et al. 2009). 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.

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 structural presence indicator, while the latter corresponds to a form of nominal service presence.

(assertion-struct service-ready (name))