X hits on this document





4 / 14






NIC Driver



Figure 2: Channels between network driver and netstack

rep struct Imp { void SendAckEvent(); void RecvNicEvent(out NicEventType eventType);


rep struct Exp { void SendNicEvent(NicEventType eventType); void RecvAckEvent();


Listing 1: Methods on endpoints

the IO CONFIGURE BEGIN state, where the client must send message RegisterForEvents to register another channel for re- ceiving events and set various parameters in order to get the conversation into the IO CONFIGURED state. If some- thing goes wrong during the parameter setting, the driver can force the client to start the configuration again by send- ing message InvalidParameters . Once the conversation is in the IO CONFIGURED state, the client can either start IO (by sending StartIO), or reconfigure the driver (ConfigureIO). If IO is started, the conversation is in state IO RUNNING. In state IO RUNNING, the client provides the driver with packet buffers to be used for incoming packets (message PacketForReceive). The driver may respond with BadPacketSize, returning the buffer and indicating the size expected. This way, the client can provide the driver with a number of buffers for incoming packets. The client can ask for packets with received data through message GetReceivedPacket and the driver either returns such a packet via ReceivedPacket or states that there are no more packets with data (NoPacket). Similar message sequences are present for transmitting pack- ets, but we elide them in the example.

From the channel contract it appears that the client polls the driver to retrieve packets. However, we haven’t ex- plained the argument of message RegisterForEvents yet. The argument of type NicEvents.Exp:READY describes an Exp chan- nel endpoint of contract NicEvents in state READY. This end- point argument establishes a second channel between the client and the network driver over which the driver notifies the client of important events (such as the beginning of a burst of packet arrivals). The client retrieves packets when it is ready through the NicDevice channel. Figure 2 shows the configuration of channels between the client and the network driver. The NicEvents contract is shown below.

contract NicEvents { enum NicEventType { NoEvent, ReceiveEvent, TransmitEvent, LinkEvent }

out in

message NicEvent(NicEventType message AckEvent();


state READY: one { NicEvent! AckEvent? READY; }


code is used:

  • C.

    Imp imp;

  • C.

    Exp exp;

  • C.

    NewChannel(out imp, out exp);

Two variables imp and exp of the corresponding endpoint types are declared. These variables are then initialized via a call to C.NewChannel which creates the new channel and returns the endpoints by initializing the out parameters.1

Endpoint types contain method definitions for sending and receiving messages described in the contract. For ex- ample, the endpoints of the NicEvents contract contain the method declarations shown in Listing 1. The semantics of these methods is as follows. Send methods never block and only fail if the endpoint is in a state in the conversation where the message cannot be sent. Receive operations check that the expected message is at the head of the queue and if so, return the associated data. If the queue is empty, re- ceives block until a message has arrived. If the message at the head of the queue is not the expected message or the channel is closed by the peer, the receive fails.

As is apparent from these declarations, there is no need to allocate a message object and fill it with the message data. Only the message arguments are actually transmitted along with a tag identifying the message. The sender and receiver only manipulate the message arguments, never an entire message. This property is desirable, for it avoids the possibility of failure on sends. Furthermore, as we discuss in Section 2.6, it simplifies the implementation.

Direct calls to the receive methods are not useful in gen- eral, since a program has to be ready to receive one of a num- ber of possible messages. Sing# provides the switch receive statement for this purpose. Here’s an example of using the NicDevice channel endpoint in the server:

NicDevice.Exp:IO RUNNING nicClient ...

switch receive { case nicClient .PacketForReceive(buf ): // add buf to the available buffers , reply ...

case nicClient .GetReceivedPacket(): // send back a buffer with packet data if available ...

So far we have seen how channel contracts specify messages and a finite state machine describing the protocol between the Imp and Exp endpoints of the channel. The next section describes how programs use channels.


case nicClient .ChannelClosed(): // client closed channel ...

2.4 Channel Operations To create a new channel supporting contract C, the following

1In C# an out parameter is like a C++ by-ref parameter, but with the guarantee that it will be initialized on all nor- mal code paths.

Document info
Document views51
Page views51
Page last viewedSun Jan 22 05:59:40 UTC 2017