X hits on this document

35 views

0 shares

0 downloads

0 comments

5 / 14

In general, each case can consist of a conjunction of patterns of the form

patternconjunction :pattern [ && patternconjunction ] | unsatisfiable pattern :var .M(id ,...)

A pattern describes a message M to be received on an end- point in variable var and a sequence of identifiers id ,... that will be bound to the message arguments in the case body.

A pattern is satisifed if the expected message is at the head of the endpoint’s receive queue. The execution of a switch receive statement proceeds as follows. Each case is examined in order and the first case for which all pattern conjuncts are satisfied executes. The messages of the match- ing case are removed from the corresponding endpoints and the message arguments are bound to the identifiers before execution continues with the case block. Blocks must end in a control transfer, typically a break.

If no case is satisfied, but some cases could be satisfied if more messages arrive, the switch receive will block until the arrival of new messages. If on the other hand, none of the cases could be satisfied by more message arrivals, the switch receive continues with the unsatisfiable block.

2.5 Channel Closure

Channels are the only ties between processes and thus act as the unique failure points between them. We adopted the design that channel endpoints can be closed at any time, either because a process explicitly closes an endpoint via delete ep, or because the process terminates (normally or abruptly) and the kernel reclaims the endpoint. Each end- point is closed independently but a channel’s memory is re- claimed only when both ends have been closed.

This independent closure of endpoints makes it easier to provide a clean failure semantics and a single point where programs determine if a channel peer has closed its endpoint. As we mentioned above, sends to endpoints never fail if the endpoint is in the correct state in the conversation, even if the peer endpoint is already closed. However, on receives a special message ChannelClosed appears in the receive queue once all preceeding messages have been received and the peer has closed its end. Once an endpoint has been closed, the compiler verifies that no more sends or receives can be performed on that endpoint. The ChannelClosed messages are implicit in the channel contracts.

2.6 Channel Properties

A main requirement of the channel implementation for Sin- gularity is that sends and receives perform no memory al- location. The requirement has three motivations: 1) since channels are ubiquitous and even low-level parts of the ker- nels use channels, we must be able to send and receive in out-of-memory situations, and 2) if memory allocation oc- curred on sends, programs would have to handle out of mem- ory situations at each send operation, which is onerous, and 3) make message transfers as efficient as possible.

In order to achieve this no-allocation semantics of chan- nel operations, we enforce a finiteness property on the queue size of each channel. The rule we have adopted, and which is enforced by Sing#, is that each cycle in the state transitions of a contract C contains at least one receive and one send action. This simple rule guarantees that no end can send an unbounded amount of data without having to wait for a

message. As we will describe in Section 4, this rule allows us to layout all necessary buffers in the endpoints themselves and pre-allocate them as the endpoints are allocated. Al- though the rule seems restrictive, we have not yet seen a need to relax this rule in practice.

The second property enforced on channels is that they transfer only values of exchangeable types. Allowing a refer- ence to an object in the GC’ed heap to be transferred would violate the property that no processes contain pointers into any other processes heap. Thus, enforcing this property statically is vital to the integrity of processes.

The third and final send-state property concerns end- points transferred in messages. Such endpoints must be in a state of the conversation where the next operation is a send on the transferred endpoint, rather than a receive. This property is motivated by implementation considera- tions. As we will discuss in Section 4, each block in the exchange heap (thus each endpoint) contains a header indi- cating which process owns it at the moment. In order for send operations to update this information correctly, one has to avoid the following scenario: process A sends endpoint e to process B. Before it has transferred e’s ownership to B, process C, holding the peer f of e tries to send a block m on f. C finds that the peer is owned by A. After that, A transfers e to B, but C still thinks it needs to make A the owner of m, whereas B should be the owner.

This scenario is essentially a race condition that could be attacked using various locking schemes. But such locking would involve multiple channels, is likely to cause contention and is difficult to implement without deadlocks. The send- state property rules out this race statically and allows for a simple lock-free implementation of transfers.

3. RESOURCE VERIFICATION

One of the goals for the Singularity project is to write code in a high-level garbage-collected language, thereby ruling out errors such as referencing memory through dangling point- ers. However, garbage collection is local to a process and ownership of memory blocks transferred through channels requires the reintroduction of explicit memory management into the language.

Consider the operation ep.SendPacketForReceive(ptr) from the NicDevice contract. The ptr argument points to a vector in the exchange heap (type byte [] in ExHeap). After the send operation, the sending process can no longer access this byte vector. From the sender’s perspective, sending the vector is no different than calling delete on the vector. In both cases, the value of ptr constitutes a dangling reference after these operations.

Avoiding errors caused by manual memory management in C/C++ programs is a long standing problem. Thus, it would appear that adopting an ownership transfer model for message data would set us back in our quest for more reliable systems.

Fortunately, the programming language community has made important progress in statically verifying explicit re- source management in restricted contexts [10, 12, 32]. The rules described in this section for handling blocks in the exchange heap allow a compiler to statically verify that 1) processes only access memory they own, 2) processes never leak a block of memory, and 3) send and receive operations on channels are never applied in the wrong protocol state.

Document info
Document views35
Page views35
Page last viewedWed Dec 07 10:56:34 UTC 2016
Pages14
Paragraphs544
Words12418

Comments