Confirm
699
edits
Changes
→Protocol-specification Language
We will follow the example of [http://research.microsoft.com/pubs/69431/osr2007_rethinkingsoftwarestack.pdf Sing#] for protocol specifications. Since C++ doesn't support this kind of code, and it's extremely hard to make it do so, and we may want to allow other languages (JavaScript) to implement protocol actors, we will implement protocol specifications as a domain-specific language. (We did the same thing for IDL.) The remainder of this document focuses on this protocol-specification language.
== Protocol-specification definition Language (PDL) ==
A protocol has a ''server'' and a ''client''. Loosely speaking for IPC, the ''client'' '''MAY BE''' the process that forks the ''server'' process. Again loosely speaking, the ''server'' provides capabilities not inherent to the ''client''.
A protocol is specified with respect to the server; that is, messages the server is allowed to receive are exactly the messages a client is allowed to sent, and ''vice versa''.
A protocol consists of definitions declarations of ''messages'' and specifications of ''state machine transitions''. (This ties us to state-machine semantics.) The message definitions declarations are essentially type declarations for the transport layer, and the state machine transitions capture the semantics of the protocol itself. A protocol is specified by first naming the protocol protocol Foo { This implies the creation of a <code>FooServer</code> and <code>FooClient</code>. (Hereafter, this document speaks from the perspective of the <code>FooServer</code>.) Conceptually (but not necessarily syntactically) next are message definitions. What underlying types we allow in these, and with what qualifiers, is likely to be a central topic of debate. Another hot topic will likely be what message semantics we provide; possibilities are* '''asynchronous''': the sending actor does not expect nor listen for a response to the sent message* '''synchronous''': the sending actor is completely blocked until it receives a response* '''RPC++''': the sending actor is partially blocked until it receives a response to message ''m''. It is only allowed to process RPC++ messages sent by the actor receiving ''m'', direct resulting from the receiving actor receiving ''m''. (This is intended to model function call semantics.) (From e-mail discussions, it appears that we may want RPC++ messages, excluding synchronous messages (since they're a special case of RPC++ messages). However, I'm not convinced RPC++ is necessary, and I'm writing the strawman grammar below assuming we only require synchronous messages.) === Strawman message grammar === Message :: (SyncMessage | AsyncMessage) ';' SyncMessage :: 'sync' ('in' | 'out') Type MessageName '(' MessageArguments ')' AsyncMessage :: 'async' ('in' | 'out') MessageName '(' MessageArguments ')' MessageArguments :: (MessageArgument ',' | \epsilon)* MessageArgument :: Type Identifier Type :: SharingQualifier BasicType SharingQualifier :: ('share' | 'transfer' | \epsilon) BasicType :: ('void' | 'int' | ... ???) A few items are worth calling out. * As mentioned above, will SyncMessage be sufficient for us?* SyncMessages have a return type, whereas AsyncMessages don't.* SharingQualifiers are a discussion unto themselves. '''share''' means that the object ''o'' named lives in shared memory, and is co-owned by the client and server. If the receiving actor does not already co-own ''o'', it does after receiving the message. A lower layer needs to enforce that this is implemented correctly:# ''o'' lives in shared memory# all objects reachable from ''o'' live in shared memory# all accesses to members of ''o'' are synchronized across the client and server '''transfer''' means that the sending actor owns ''o'', and when the receiving actor receives ''o'', ownership transfers from the sender to the receiver. This means that requirement (3) above is removed for '''transfer''' types. No SharingQualifier (\epsilon) means that that object sent is serialized. How we classes are serialized is probably not a concern of the protocol layer, but very important nonetheless. This is likely to be another security concern. '''NOTE''': '''share''' and '''transfer''' are optimizations. These don't need to be included in the initial language implementation, but are worth keeping in mind. === Strawman transition grammar === Transition :: 'state' StateName '{' Actions '}' Actions :: (Action ';' | \epsilon) Action :: MessageName ('!' | '?') '->' StateName This is a dirt-simple grammar but should capture all we need in a first pass. A transition starts from a particular state (the lexically first state is the start state), and then either sends or receives one of a set of allowed messages. The syntax <code>MessageName !</code> means "send MessageName", and <code>MessageName ?</code> means "receive MessageName". The actor then transitions into another state. From a particular state, an actor can either ''only receive'' or ''only send'' messages (we could relax this, but it complicates the implementation). This is extremely easy to check statically (we could make it part of the grammar, too). Transitions only happen when the underlying message operation was "completed." For messages sent asynchronously, this means sent over the wire (resp., received). For messages sent synchronously, this means sent over the wire ''and'' replied to by the other side (resp., received and reply sent). '''TODO''': there are many things we can integrate here, but concrete use cases are necessary. This should be a main point of discussion.
