You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Figure~\ref{rqmflowchartgenericsignature} shows the process of query machine construction, beginning with the minimal requirements of a generic signature:
77
+
Figure~\ref{rqmflowchartgenericsignature} shows how a query machine is constructed from the minimal requirements of a generic signature:
78
78
\begin{enumerate}
79
79
\item The \index{rule builder}\emph{rule builder} lowers the generic signature's minimal requirements to \emph{rewrite rules}; these become the \IndexDefinition{local rule}\emph{local rules} of our new requirement machine.
We will show that the protocols that can appear in the \index{derived requirement}derivations of a given generic signature are precisely those reachable from an initial set in the \index{protocol dependency graph}protocol dependency graph. We begin by considering protocol dependencies between protocols first. Along the way, we also introduce the \emph{protocol component graph} to get around complications caused by circular dependencies.
215
215
216
216
\begin{definition}
217
-
A protocol $\protosym{P}$\emph{depends on} a protocol $\protosym{Q}$ (or has a \emph{protocol dependency} on~$\protosym{Q}$) if we can derive a conformance to $\protosym{P}$ from the protocol generic signature $G_\texttt{P}$; that is, if $G_\texttt{P}\vDash\ConfReq{T}{P}$ for some type parameter \texttt{T}. We write $\protosym{P}\prec\protosym{Q}$ if this relationship holds. The \emph{protocol dependency set} of a protocol $\protosym{P}$ is then the set of all protocols $\protosym{Q}$ such that $\protosym{P}\prec\protosym{Q}$.
217
+
A protocol $\protosym{P}$\emph{depends on} a protocol $\protosym{Q}$ (or has a \emph{protocol dependency} on~$\protosym{Q}$) if we can derive a conformance to $\protosym{Q}$ from the protocol generic signature $G_\texttt{P}$; that is, if $G_\texttt{P}\vDash\ConfReq{T}{Q}$ for some type parameter \texttt{T}. We write $\protosym{P}\prec\protosym{Q}$ if this relationship holds. The \emph{protocol dependency set} of a protocol $\protosym{P}$ is then the set of all protocols $\protosym{Q}$ such that $\protosym{P}\prec\protosym{Q}$.
218
218
\end{definition}
219
219
220
220
Lemma~\ref{substlemma} implies that $\prec$ is a \index{transitive relation}transitive relation; that is, if $\protosym{P}\prec\protosym{Q}$ and $\protosym{Q}\prec\protosym{R}$, then $\protosym{P}\prec\protosym{R}$. In fact, $\prec$ is the \index{reachability relation}reachability relation in the protocol dependency graph. Before we can prove this, we need a technical result.
The protocol component graph of Listing~\ref{protocolcomponentlisting} is shown on the left. With the exception of $\protosym{Foo}$ and $\protosym{Bar}$, which have collapsed to a single vertex, every protocol is in a protocol component by itself. The protocol component graph is always acyclic. However, it is still not a tree or a forest; as we see in our example, we have two distinct paths with source $\protosym{Top}$ and destination~$\protosym{Bot}$, so components can share ``children.'' To not import duplicate rules, we must take care to visit every downstream protocol machine once, and take only the \emph{local} rules from each. (Every imported rule was local in its original protocol machine, so we import it exactly once from there, never ``transitively.'')
359
+
The protocol component graph of Listing~\ref{protocolcomponentlisting} is shown on the left. With the exception of $\protosym{Foo}$ and $\protosym{Bar}$, which have collapsed to a single vertex, every protocol is in a protocol component by itself. The protocol component graph is always acyclic. However, it is still not a tree or a forest; as we see in our example, we have two distinct paths with source $\protosym{Top}$ and destination~$\protosym{Bot}$, so components can share ``children.'' To ensure we do not import duplicate rules, we must be careful to only visit every downstream protocol machine once, and take only the \emph{local} rules from each. (Every imported rule was local in its original protocol machine, so we import it exactly once from there, never ``transitively.'')
360
360
361
361
A \IndexTwoFlag{debug-requirement-machine}{protocol-dependencies}debugging flag prints out each connected component as it was formed. Let's try with our example:
We number vertices in the order they are visited, by assigning an incrementing integer to each vertex~$v$ prior to visiting its successors. We denote this by denoted $\Number{v}$. Our traversal can thus keep track of those vertices that have been visited by checking if $\Number{v}$ is set.
424
+
We number vertices in the order they are visited, by assigning the current value of a counter to each visited vertex$v$, prior to visiting the successors of $v$. We denote the value assigned to a vertex $v$ by $\Number{v}$. Our traversal can determine if a vertex has been previously visited by checking if $\Number{v}$ is set.
425
425
426
426
We return to the protocol dependency graph from Listing~\ref{protocolcomponentlisting}. A depth-first search originating from $\protosym{Top}$ produces the numbering of vertices shown on the right, where the first vertex is assigned the value 1. Here, the entire graph was ultimately reachable from 1; more generally, we get a numbering of the subgraph reachable from the initial vertex.
427
427
428
428
When looking at a vertex $v$, we consider each edge $e\in E$ with $\Src(e)=v$. Suppose that $\Dst(e)$ is some other vertex~$w$; Tarjan considers the state of $\Number{w}$, and classifies the edge $e$ into one of four kinds: tree edges, ignored edges, fronds, and cross-links.
429
429
430
-
If $\Number{w}$ has not yet been set, we say that $e$ is a \emph{tree edge}; the tree edges define a \emph{spanning tree} of the subgraph explored by the search. Otherwise, $w$ was visited earlier by the traversal, and we have one of the three remaining kinds. If $\Number{w}\geq\Number{v}$ (with equality corresponding to an edge from $v$ to itself, which we allow), any path from $v$ to $w$ must pass through a common ancestor of $v$ and $w$ in the spanning tree. We say that $e$ is an \emph{ignored edge}, because $e$ cannot not give rise to any new strongly connected components. The final two kinds arise when $\Number{w}<\Number{v}$. We say that $w$ is a \emph{frond} if $w$ is also an ancestor of $v$ in the spanning tree; otherwise, $e$ is a \emph{cross-link}. (While the distinction between the final two kinds plays a role in Tarjan's correctness proof, we'll see that algorithm handles fronds and cross-links uniformly.)
430
+
If $\Number{w}$ has not yet been set, we say that $e$ is a \emph{tree edge}; the tree edges define a \emph{spanning tree} of the subgraph explored by the search. Otherwise, $w$ was visited earlier by the traversal, and we have one of the three remaining kinds. If $\Number{w}\geq\Number{v}$ (with equality corresponding to an edge from $v$ to itself, which we allow), any path from $v$ to $w$ must pass through a common ancestor of $v$ and $w$ in the spanning tree. We say that $e$ is an \emph{ignored edge}, because $e$ cannot not give rise to any new strongly connected components. The final two kinds arise when $\Number{w}<\Number{v}$. We say that $e$ is a \emph{frond} if $w$ is also an ancestor of $v$ in the spanning tree; otherwise, $e$ is a \emph{cross-link}. (While the distinction between the final two kinds plays a role in Tarjan's correctness proof, we'll see that algorithm handles fronds and cross-links uniformly.)
The algorithm also needs a cheap way to check if a vertex is currently on the stack. We associate one more piece of state with each vertex $v$, a single bit denoted $\OnStack{v}$, to be set when $v$ is pushed and cleared when $v$ is popped.
Takes a vertex $v$ as input, together with some means of enumerating the successor vertices of $v$. Builds two maps: to each vertex, we assign a component ID, and to each component ID, we assign a list of member vertices. Upon completion, $v$ has a component ID assigned. Maintains a stack, and two global incrementing counters: the next vertex ID, and the next component ID.
490
+
Takes a vertex $v$ as input, together with some means of enumerating the successor vertices of $v$. Builds two maps: to each vertex, we assign a component ID, and to each component ID, we assign a list of member vertices. Upon completion, $v$ has a component ID assigned. Maintains a stack, and two global incrementing counters: the next unused vertex ID, and the next component ID.
491
491
\begin{enumerate}
492
492
\item (Memoize) If $v$ already has a component ID assigned, return this component ID, which can be used to look up its members.
493
493
\item (Invariant) Otherwise, ensure that $\Number{v}$ has not been set. If it is set but $v$ does not have a component ID, we performed an invalid re-entrant call (see below).
\item Otherwise, $\Number{w}<\Number{v}$, so we have a frond or cross-link. If $\OnStack{w}$ is true, set $\Lowlink{v}\leftarrow\min(\Lowlink{v},\Number{w})$.
500
500
\end{enumerate}
501
501
\item (Not root?) If $\Lowlink{v}\neq\Number{v}$, return.
502
-
\item (Root) Create a new component consisting of$v$, and associate the component ID with $v$.
502
+
\item (Root) Assign the next unused component ID to$v$, and add $v$ to this component ID.
503
503
\item (Add vertex) Pop a vertex $v^\prime$ from the stack (which must be non-empty at this point) and clear $\OnStack{v^\prime}$. Add $v^\prime$ to the component of $v$, and associate the component ID with $v^\prime$.
504
-
\item (Repeat) If the stack is not empty, go back to Step~7.
504
+
\item (Repeat) If the stack is not empty, go back to Step~7. Otherwise, return.
505
505
\end{enumerate}
506
506
\end{algorithm}
507
507
After the outermost recursive call returns, the stack will always be empty. Note that while this algorithm is recursive, it is not re-entrant; in particular, the act of getting the successors of a vertex must not trigger the computation of the same strongly connected components. This is enforced in Step~2. In our case, this can happen because getting the successors of a protocol performs type resolution; in practice this should be extremely difficult to hit, so for simplicity we report a fatal error and exit the compiler instead of attempting to recover.
\lettrine{W}{e now return} to tie up a loose end in \index{type substitution}type substitution. We encountered type substitution in Chapter \ref{substmaps}, first in its most basic form, as a structural mapping of generic parameter types to the replacement types of a substitution map. The next level of detail appeared when we considered type substitution of the other kind of type parameter: the dependent member type. A substitution map can contain conformances in addition to replacement types, and Chapter~\ref{conformances} showed that under type substitution, a \index{dependent member type}dependent member type corresponds to a \index{type witness}type witness of a conformance. To find this conformance, we introduced the so-called local conformance lookup operation, but only defined it in the simplest case, where the conformance is directly stored in the substitution map. Now, we will consider the general case, which entails finding and evaluating a \emph{conformance path}. We're going to build upon associated conformances from Section~\ref{associated conformances}, and the validity results of Section~\ref{generic signature validity}.
22
+
\lettrine{W}{e now return} to tie up a loose end in \index{type substitution}type substitution. We encountered type substitution in Chapter \ref{substmaps}, first in its most basic form, as a structural mapping of generic parameter types to the replacement types of a substitution map. The next level of detail appeared when we considered type substitution of the other kind of type parameter: the dependent member type. A substitution map can contain conformances in addition to replacement types, and Chapter~\ref{conformances} showed that under type substitution, a \index{dependent member type}dependent member type corresponds to a \index{type witness}type witness of a conformance. To find this conformance, we introduced the so-called local conformance lookup operation, but only defined it in the simplest case, where the conformance is directly stored in the substitution map. In this chapter, we consider the general case of recovering the desired conformance by evaluating a \emph{conformance path}. We're going to build upon associated conformances from Section~\ref{associated conformances}, and the validity results of Section~\ref{generic signature validity}.
23
23
24
24
\begin{listing}\captionabove{Example to motivate conformance paths}\label{conformancepathslisting}
Writing down the list of protocols from each step (remember that conformance paths are read from right to left!) we get a path in the protocol dependency graph; the path visits \texttt{Q} and \texttt{R} twice, exhibiting the existence of a cycle:
Writing down the list of protocols from each step (remember that conformance paths are read from right to left!) we get a path in the protocol dependency graph; the path visits $\protosym{Q}$ and $\protosym{R}$ twice, exhibiting the existence of a cycle:
We encounter the protocol dependency graph again in Chapter~\ref{rqmbasicoperation}, when we describe the construction of the rewrite system for a generic signature.
630
+
We will encounter protocol dependency graphs again in Chapter~\ref{rqmbasicoperation}, when we describe the construction of the rewrite system for a generic signature.
631
631
632
632
\begin{figure}\captionabove{Conformance path graph for $G_\texttt{Q}$ from Listing~\ref{protocoldependencygraphlisting}}\label{infinitetreegraph}
\item Every vertex has finitely many successors (such a graph is said to be locally finite).
665
665
\item Every vertex is reachable by a path from a fixed finite set of root vertices.
666
666
\end{enumerate}
667
-
Then, the graph contains a \index{ray}\emph{ray}\index{infinite path|see{ray}} (or infinite path), an infinite sequence of distinct vertices, where each element is joined to the next by an edge.
667
+
Then the graph must contain a \index{infinite path|see{ray}}\index{ray}\emph{ray}, or infinite path: an infinite sequence of distinct vertices, where each element is joined to the next by an edge.
668
668
\end{theorem}
669
669
\begin{proof}
670
670
To choose the first element of the sequence, note that there are only finitely many roots, but every vertex is reachable from at least one root by assumption, so at least one root must be the origin of infinitely many distinct paths. This root serves as the first element of our sequence. We can then always add another vertex to our sequence, as long as the last vertex is the origin of infinitely many distinct paths, not involving any vertex already in our sequence. However, as each vertex has finitely many successors, so at least one successor of the last vertex has the necessary property. We can iterate this construction arbitrarily in this manner, giving us the desired infinite sequence of vertices.
0 commit comments