X hits on this document





10 / 14


int y;


b.RecvR(out y);



1 2 3 4 5 6 7 8 9 10 11

Endpoint [] endpoints = new Endpoint[]{a,b}; int enabled case = Endpoint.Select(pattern , endpoints ); switch ( enabled case ) {

case 0: int x; char [] in ExHeap vec;

  • a.

    RecvM(out x);

  • b.

    RecvQ(out vec);


case 1:

Listing 2: Generated code for switch receive

15 16 17 18 19 20 21 22 23 24


case 2: block2

case 3: block3

default : throw new Exception(” Unsatisfiable switch receive ”);

message, or -1 if there is no message and the peer endpoint is closed, or 0, if there is no message and the peer endpoint is not closed. Given this information, Select can determine if a case is satisfied and whether the case can still be satisfied by the arrival of new messages.

If no case is satisfied, but some cases are still satisfiable in the future, Select waits on the waithandles of all endpoints involved in the switch. When woken due to a new message arrival or channel closure, the patterns are scanned again. 3

Note that the implementation uses no locking or other synchronization beyond the signalling of new messages via the waithandles. This lock-free implementation is again en- abled by the global invariants provided by our ownership model: only a single thread can use a given endpoint in a switch receive at any time. Thus, we are guaranteed that when Select determines a case is satisfiable, the state of its endpoints won’t change until the thread enters the cor- responding case and removes the messages at the head of the endpoints involved. If multiple threads were to be able to receive on a single endpoint, the implementation would be much more involved, since it must atomically determine which case is satisfied and dequeue the corresponding mes- sages.


In practice, we use a couple of extensions to the channel mechanisms described so far. In this section, we briefly men- tion them as well as other ongoing work.

5.1 Endpoint sets and maps

Threads often need to handle an apriori unknown number of endpoints. This arises most frequently in services that have numerous connections to clients. In order to handle these situations, Sing# provides an endpoint set abstraction. An endpoint set contains endpoints that are all of the same type and in the same prototol state. Threads can create sets, add

3Only the pattern column of the endpoint that caused the wakeup is scanned in practice.













Figure 4: Cross machine channel via TCP proxy

endpoints, and use these sets in switch receive statements to wait for messages on any of the endpoint in a set. When an endpoint has a matching message, the endpoint is removed from the set and bound in the case branch.

Endpoint maps are similar to sets, but associate arbitrary data with each endpoint in the set.

5.2 Channel contract hierarchies

Channel contracts can form hierarchies such that a contract can extend another contract by adding more message se- quences than the parent contract. In order for this to be sound, restrictions must be in place for when such exten- sions are allowed and how the corresponding types of end- points can be cast to each other. A formal study of channel contract inheritance is the topic of an upcoming paper.

5.3 Process local channels

The channel implementation described does not require the two channel endpoints to be in different processes. The channels work just as well between threads of the same pro- cess. If such intra-process channels are declared as such, they can support a wider range of exchangeable types, since GC’ed objects could be safely transmitted over such chan- nels.

5.4 Cross machine channels

The Singularity OS includes a TCP/IP stack and network interface drivers. Thus, communicating with other machines on the network is no different than on Unix or Windows. An obvious question though is whether the strongly typed Sin- gularity channels can be extended to cross machine bound- aries. Although we haven’t implemented this feature, we believe it to be straight-forward as depicted in Figure 4. A process P on machine Kiwi wants to talk to a process Q on machine Barnowl using channel contract C. From the con- tract C we should be able to automatically produce proxy processes proxyQ and proxyP that marshall and unmarshall messages to and from the network and dynamically check the protocol of incoming network messages. The clients P and Q talk to the proxies over strongly typed channels, oblivi- ous (up to latency) to the fact that they are communicating remotely. The semantics of our channels poses no immedi- ate problem due to the fact that sends never block and that the channel failure is communicated only on receives. Thus, when proxies determine that the TCP connection has failed, they can just close the channel the their clients.

5.5 Running unverified code

To run on Singularity, applications must currently be ex- pressible in verifiable MSIL. This requirement makes it im-

Document info
Document views49
Page views49
Page last viewedThu Jan 19 06:54:37 UTC 2017