X hits on this document





8 / 14

element in the same way as we exposed an entire struct. Below is an example showing the manipulation of a vector of network packets, using the previously defined method to double the buffer in each packet.

void DoubleAll(NetworkPacket[] in ExHeap vec) { for ( int i=0; i<vec.Length; i++) { expose(&vec[i]) { DoubleBufferSize(vec[ i ]); }



Note that expose always acts on the slot of the vector, not the content of the slot. The invariant of a vector is that if the vector has no exposed slot, all the contents of all slots is owned. When exposing a slot, ownership of that slot’s contents is transferred to the method, which can then act on it. On exit of the expose block, the ownership of the slot’s contents is transferred back to the vector in order to satisfy its invariant.

3.2.1 Discussion

The expose blocks shown in the previous sections have no impact on the generated code or the instructions executed at runtime. The exposing and unexposing of vectors and structs are only hints for the static analysis on how to prove the code safe. All checking of ownership invariants is per- formed statically at compile time. The only runtime opera- tions in conjunction with ownership are acquires and releases of TCells.

As mentioned earlier, channel endpoints are just point- ers into the exchange heap and are thus tracked like other blocks in the exchage heap. Additionally, the verifier stat- ically tracks the protocol state of each endpoint. This is again a relatively simple matter if we specify the protocol state of each endpoint whenever a message acquires own- ership of them. Thus, we require endpoint arguments and results of methods to specify the protocol state of the end- point. Similarly, message declarations must specify the state of endpoints they transport and TCells specify the state of the endpoints they encapsulate.

The verifier computes for each program point and each owned endpoint the possible protocol states of the endpoint. At Send calls, the verifier checks that the endpoint is in a state where the message can be sent. At Select calls, the verifier determines if the cases are exhaustive, i.e., whether there is a case for every message combination on the end- points.

In summary, the static tracking ensures the following system- wide invariants:

  • Each block in the exchange heap has at most one own- ing thread at any point in time.

  • Blocks in the exchange heap are only accessed by their owner. (thus no access after free or transfer of owner- ship)

  • A block not owned by a thread is owned by a TCell and thus effectively by the garbage collector’s finalizer thread.

  • The sequence of messages observed on channels corre- spond to the channel contract.





C.Exp* peer;

C.Imp* peer;

WH waithandle;

WH waithandle;

int state;

int state;

int Tag0;

int Tag0;

0 C.M Msg_M ;

0 C.E Msg_E ;

0 C.N Msg_N ;

0 C.F Msg_F ;


Figure 3: Channel representation in memory


This section describes the runtime data and code represen- tation for channels and switch receive statements.

4.1 Channel representation

Channel endpoints are represented as rep structs in the ex- change heap. Each endpoint struct has a general part man- aged by the kernel and a contract-specific part. The kernel managed part contains a pointer to the channel peer, a spe- cial waithandle for signalling message arrival, and a boolean indicating whether this end of the channel has been closed.

A channel contract C is compiled into two rep structs C.Exp and C.Imp. Besides the kernel managed part, these structs contain a numeric field capturing the current protocol state of the endpoint, tag fields, and message argument buffers. Figure 3 shows a channel in memory.

The messages and protocol states of a channel (including implicit intermediate states in message sequences) are as- signed numeric values. Then we compute maps C QI Exp and C QI Imp mapping protocol states to a queue index, thereby capturing how many messages are (maximally) waiting to be received at that protocol state. The queue index is com- puted by examining the protocol state machine and noting the maximal number of message receipts since the last send in the state machine.

For each queue index i, the endpoint contains a tag field Tagi. The tag fields describe whether messages are present in the queue as follows: if a C.Exp endpoint is in protocol state X and C QI Exp(X) = i, we can determine whether a message has arrived on it by examining field Tagi. If the field is 0, no message is ready. Otherwise, the field value indicates the message tag that is present. Thus, if we are to send message m in state X on endpoint C.Imp, the sending code uses the queue index C QI Exp(X) = i for the peer endpoint, and then stores the message tag for m in the peer’s Tagi field. After storing the tag, the sender signals the waithandle on the peer. The reasoning in the other direction is symmetric.

The message data is handled similarly to the message tag. The compiler emits a struct type C.M for each mes- sage m whose fields are the message arguments. For each queue index i in an endpoint, if message m could be re- ceived in a state mapping to i, we add a message buffer field Msg Mi in the endpoint structure. Sending message m now involves also storing the message arguments in the peers Msg Mi field, prior to setting the message tag Tagi. On multi-processors/cores, a memory barrier is needed af-

Document info
Document views53
Page views53
Page last viewedSun Jan 22 21:09:29 UTC 2017