|
@@ -531,55 +531,83 @@ unexpected type is received,
|
|
eliminating the need for ad-hoc error handling code to be written by application developers.
|
|
eliminating the need for ad-hoc error handling code to be written by application developers.
|
|
|
|
|
|
% Example of a protocol contract.
|
|
% Example of a protocol contract.
|
|
-% TODO: I don't find this example very compelling. It would be more impressive to show a pub-sub
|
|
|
|
-% protocol, that would look cool.
|
|
|
|
-Let us explore the use of this system through a simple example using the HTTP/1.1 protocol.
|
|
|
|
-It is a state-less client-server protocol,
|
|
|
|
-essentially just an RPC from client to server.
|
|
|
|
-We can model this in for the contract checker by defining a trait representing the protocol:
|
|
|
|
|
|
+Let's explore how this system can be used to build a simple pub-sub communications protocol.
|
|
|
|
+In this protocol,
|
|
|
|
+there will be a server which handles \texttt{Sub} messages by remembering the names of the actors
|
|
|
|
+who sent them.
|
|
|
|
+It will handle \texttt{Pub} messages by forwarding them to all of the subscribed actors.
|
|
|
|
+The state-transition graph for the system is shown in figure \ref{fig:pubsub}.
|
|
|
|
+\begin{figure}
|
|
|
|
+ \begin{center}
|
|
|
|
+ \includegraphics[scale=0.6]{PubSubStateGraph.pdf}
|
|
|
|
+ \end{center}
|
|
|
|
+ \caption{The state-transition graph for a simple pub-sub protocol.}
|
|
|
|
+ \label{fig:pubsub}
|
|
|
|
+\end{figure}
|
|
|
|
+The solid edges in the graph indicate state transitions and are labeled with the message type
|
|
|
|
+which triggered the transition.
|
|
|
|
+The dashed edges indicate message delivery and are labeled with the type of the message delivered.
|
|
|
|
+Although \texttt{Runtime} is not the state of any actor in the system,
|
|
|
|
+it is included in the graph as the sender of the \texttt{Activate} and \texttt{Pub} messages.
|
|
|
|
+\texttt{Activate} is delivered by the runtime to pass a reference to the runtime and provide the
|
|
|
|
+actor's \texttt{Uuid}.
|
|
|
|
+\texttt{Pub} messages are dispatched by actors outside the graph and are routed to actors in the
|
|
|
|
+\texttt{Listening} state by the runtime.
|
|
|
|
+Note that the runtime itself doesn't have any notion of the state of any actor,
|
|
|
|
+it just delivers messaging using the rules described previously.
|
|
|
|
+Only an actor can tell whether a message is expected or not given its current state.
|
|
|
|
+Each of the actor states are modeled by Rust traits.
|
|
\begin{verbatim}
|
|
\begin{verbatim}
|
|
- pub trait Http {
|
|
|
|
- type Server: ServerInit;
|
|
|
|
|
|
+ pub struct ClientInit {
|
|
|
|
+ type AfterActivate: Subed;
|
|
|
|
+ type Fut: Future<Output = Result<Self::AfterActivate>>;
|
|
|
|
+ fn handle_activate(self, msg: Activate) -> Self::Fut;
|
|
}
|
|
}
|
|
-\end{verbatim}
|
|
|
|
-The purpose of this top-level trait is to specify the initial state of every party to the
|
|
|
|
-communications protocol.
|
|
|
|
-In this case we're only modeling the state of the server,
|
|
|
|
-as the client will just \texttt{call} a method on the server.
|
|
|
|
-The initial state for the server is defined as follows:
|
|
|
|
-\begin{verbatim}
|
|
|
|
- pub trait ServerInit {
|
|
|
|
|
|
+
|
|
|
|
+ pub struct Subed {
|
|
|
|
+ type AfterPub: Subed;
|
|
|
|
+ type Fut: Future<Output = Result<Self::AfterPub>>;
|
|
|
|
+ fn handle_pub(self, msg: Envelope<Pub>) -> Self::Fut;
|
|
|
|
+ }
|
|
|
|
+
|
|
|
|
+ pub struct ServerInit {
|
|
type AfterActivate: Listening;
|
|
type AfterActivate: Listening;
|
|
type Fut: Future<Output = Result<Self::AfterActivate>>;
|
|
type Fut: Future<Output = Result<Self::AfterActivate>>;
|
|
fn handle_activate(self, msg: Activate) -> Self::Fut;
|
|
fn handle_activate(self, msg: Activate) -> Self::Fut;
|
|
}
|
|
}
|
|
|
|
+
|
|
|
|
+ pub struct Listening {
|
|
|
|
+ type AfterSub: Listening;
|
|
|
|
+ type SubFut: Future<Output = Result<Self::AfterSub>>;
|
|
|
|
+ fn handle_sub(self, msg: Envelope<Sub>) -> Self::SubFut;
|
|
|
|
+
|
|
|
|
+ type AfterPub: Listening;
|
|
|
|
+ type PubFut: Future<Output = Result<Self::AfterPub>>;
|
|
|
|
+ fn handle_pub(self, msg: Envelope<Pub>) -> Self::PubFut;
|
|
|
|
+ }
|
|
\end{verbatim}
|
|
\end{verbatim}
|
|
-\texttt{Activate} is a message sent by the generated code to allow the actor access to the
|
|
|
|
-runtime and the actor's ID.
|
|
|
|
-It is defined as follows:
|
|
|
|
|
|
+The definition of \texttt{Activate} is as follows:
|
|
\begin{verbatim}
|
|
\begin{verbatim}
|
|
pub struct Activate {
|
|
pub struct Activate {
|
|
rt: &'static Runtime,
|
|
rt: &'static Runtime,
|
|
act_id: Uuid,
|
|
act_id: Uuid,
|
|
}
|
|
}
|
|
\end{verbatim}
|
|
\end{verbatim}
|
|
-We represent the statelessness of HTTP by having the requests to the \texttt{Listening} state
|
|
|
|
-return another \texttt{Listening} state.
|
|
|
|
|
|
+The \texttt{Envelope} type is a wrapper around a message which contains information about who sent
|
|
|
|
+it and a method that can be used to send a reply.
|
|
|
|
+In general a new actor state, represented by a new type, can be returned by a messaging handling
|
|
|
|
+method.
|
|
|
|
+The protocol itself is also represented by a trait:
|
|
\begin{verbatim}
|
|
\begin{verbatim}
|
|
- pub trait Listening {
|
|
|
|
- type AfterRequest: Listening;
|
|
|
|
- type Fut: Future<Output = Result<Self::AfterRequest>>;
|
|
|
|
- fn handle_request(self, msg: Envelope<Request>) -> Self::Fut;
|
|
|
|
|
|
+ pub trait PubSubProtocol {
|
|
|
|
+ type Server: ServerInit;
|
|
|
|
+ type Client: ClientInit;
|
|
}
|
|
}
|
|
\end{verbatim}
|
|
\end{verbatim}
|
|
-The \texttt{Envelope} type is a wrapper around a message which contains information about who sent
|
|
|
|
-it and a method which can be used to send a reply.
|
|
|
|
-In general a new type could be returned after each message received,
|
|
|
|
-with the returned type being dependent on the type of the message.
|
|
|
|
-The state graph of this protocol can be visualized as follows:
|
|
|
|
-\begin{center}
|
|
|
|
- \includegraphics[height=1.5in]{HttpStateGraph.pdf}
|
|
|
|
-\end{center}
|
|
|
|
|
|
+By modeling this protocol independently of any implementation of it,
|
|
|
|
+we allow for many different interoperable implementations to be created.
|
|
|
|
+We can also isolate bugs in these implementations because unexpected or malformed messages are
|
|
|
|
+checked for by the generated code.
|
|
|
|
|
|
% Implementing actors in languages other than Rust.
|
|
% Implementing actors in languages other than Rust.
|
|
Today the actor runtime only supports executing actors implemented in Rust.
|
|
Today the actor runtime only supports executing actors implemented in Rust.
|