X hits on this document





3 / 14




Figure 1: Process heaps and the exchange heap

called the exchange heap, to hold data that can move be- tween processes. Figure 1 shows how process heaps and the exchange heap relate. Processes can contain pointers into their own heap and into the exchange heap. The exchange heap only contains pointers into the exchange heap itself. Although all processes can hold pointers into the exchange heap, every block of memory in the exchange heap is owned (accessible) by at most one process at any time during the execution of the system. Note that it is possible for processes to have dangling pointers into the exchange heap (pointers to blocks that the process does not own), but the static verification will prevent the process from accessing memory through dangling references.

To make the static verification of the single owner prop- erty of blocks in the exhange heap tractable, we actually en- force a stronger property, namely that each block is owned by at most one thread at any time. The fact that each block in the exchange heap is accessible by a single thread at any time also provides a useful mutual exclusion guarantee.

2.2 Exchangeable Types

Exchangeable types encompass the type of all values that can be sent from one process to another. They consist of scalars, rep structs (structs of exchangeable types), and pointers to exchangeable types. Pointers can either point to a single exchangeable value or to a vector of values. Below, we explain in more detail how these types are declared.

rep struct NetworkPacket { byte [] in ExHeap data; int bytesUsed;


NetworkPacketin ExHeap packet;

The code above declares a rep struct consisting of two fields: data holds a pointer to a vector of bytes in the exchange heap and bytesUsed is an integer. The type of variable packet spec- ifies that it holds a pointer into the exchange heap pointing to a NetworkPacket struct.

Allocation in the exchange heap takes the following forms:

byte [] in ExHeap vec = new[ExHeap] byte[512];

NetworkPacketin ExHeap pkt = new[ExHeap] NetworkPacket(...);

The syntax for new is retained from C#, but the ExHeap modifier makes it clear that the allocation is to be perfomed in the exchange heap. Blocks in the exchangeable heap are deleted explicitly via the statement delete ptr, modeled after

C++. Section 3 shows why this cannot lead to dangling pointer accesses or leaks.

Endpoints themselves are represented as pointers to rep structs in the exchangeable heap so that they can be ex- changed via messages as well. Section 4 describes in more detail how endpoints are implemented.

2.3 Channel Contracts

Channel contracts in Sing# consist of message declarations and a set of named protocol states. Message declarations state the number and types of arguments for each message and an optional message direction. Each state specifies the possible message sequences leading to other states in the state machine.

We explain channel contracts via a simplified contract for network device drivers.

contract NicDevice { out message DeviceInfo (...);

in in

message RegisterForEvents(NicEvents.Exp:READY message SetParameters (...);


out message InvalidParameters (...); out message Success();

in in in

message StartIO(); message ConfigureIO(); message PacketForReceive(byte[] in ExHeap pkt);

out in out out

message message message message

BadPacketSize(byte[] in ExHeap pkt, int mtu); GetReceivedPacket(); ReceivedPacket(NetworkPacketin ExHeap pkt); NoPacket();

state START: one { DeviceInfo ! IO CONFIGURE BEGIN; }

state IO CONFIGURE BEGIN: one { RegisterForEvents ? SetParameters? IO CONFIGURE ACK;


state IO CONFIGURE ACK: one { InvalidParameters ! IO CONFIGURE BEGIN; Success ! IO CONFIGURED;




state IO RUNNING: one { PacketForReceive? (Success ! or BadPacketSize!) IO RUNNING; GetReceivedPacket? (ReceivedPacket! or NoPacket!) IO RUNNING;




A channel contract is written from the exporting view point and starts in the first listed state. Message sequences consist of a message tag and a message direction sign (! for Exp to Imp), and (? for Imp to Exp). The message direction signs are not necessary if message declarations already contain a direction (in ,out), but the signs make the state machine more human-readable.

In our example, the first state is START and the net- work device driver starts the conversation by sending the client (probably the netstack) information about the device via message DeviceInfo. After that the conversation is in

Document info
Document views43
Page views43
Page last viewedTue Jan 17 03:16:11 UTC 2017