X hits on this document





12 / 14

lation guarantees between processes, usually sharing a single heap managed by a single VM. In contrast, our processes are strongly isolated and can be killed and reclaimed individu- ally.

Many systems and languages support channel-based inter- process communication. An early system using messages to communicate between tasks is DEMOS [6] on the CRAY-1. Channels (links in DEMOS) were unidirectional and could be passed over other channels. Hardware protection and copying was used to prevent inappropriate access and shar- ing rather than compile-time checking.

Channels in programming languages are typically uni- directional streams of uniform type, for example in the lan-







stream based communication types are CML

languages with [31], Newsqueak

[29], and Limbo [13]. However, in contrast to the present work, none of the above cited work attempts to statically verify that exchanged data blocks are unshared without the need to copy memory.

Recent work on writing an operating system in OCCAM [4] has extended the language to support mobile data, which corresponds to what we call tracked data in this paper [5]. The main difference with the present work is that we have in- tegrated mobile semantics into a main-stream OO-language without compromising safety or aliasing. Furthermore, the OCCAM channels are synchronous, uni-directional, and uni- formly typed, whereas the channels described here are asyn- chronous, bi-directional and governed by channel protocols. Their reported message transfer times are extremely efficient (80 cycles). The factor of 20 in increased performance over our approach is achieved by exploiting further invariants their system has over ours. The scheduling in their kernel is purely cooperative and assumes a single processor, whereas we assume a pre-emptive scheduler in a multicore/multi-cpu environment. Furthermore, an OCCAM thread waits on a single channel, whereas our threads can be blocked on any number of wait conditions, which causes more accounting on waking a thread. Our implementation also has to cooperate with two garbage collectors, the process’ own, and the ker- nel’s. On process-kernel boundaries, we push special stack markers that allow the respective GC’s to avoid scanning stack frames they don’t own. Finally, their implementation uses the channel as the synchronization event itself, whereas we currently use primitive events to implement the channel synchronization. We believe that we can further improve our channel performance by careful optimizations for the common case.

On the systems side, much research has gone into tech- niques to avoid copying of memory in the IO-system. For ex- ample, IO-Lite [28], uses read-only buffers accessed through mutable buffer aggregates to allow wide sharing of the buffers among different parts of the system. Buffer aggregates al- low splicing together various regions of buffers. The IO- Lite approach uses VM pages and page protection to enforce read-only access. The main drawback of IO-Lite appears to be the need to know, during buffer allocation, which other processes will share the page in order to avoid remapping of pages and fragmentation. In comparison, the statically enforced mutual exclusion of access to buffers described in this paper does not suffer from page granularity restrictions. Similarly, the IPC mechanism in L4 micro kernel [20] is based on hardware protection and is only zero-copy if entire pages are transferred by remapping. Otherwise, the cost is

proportional to the size of transferred buffers. Compared with measurements for L4 on the Alpha, our message round trip times are faster than L4’s for all transfer sizes above 64 bytes (which L4 passes in registers).

The lack of read-only sharing in our system is one of its main drawbacks at the moment. We plan to address this issue in future work by incorporating ideas from IO-Lite while retaining a purely software based protection approach.

Ennals et al. use linear types to pass ownership of buffers in a language for packet processing compiled to network pro- cessors [14], thereby proving isolation between the sender and receiver statically as we do. Our resource tracking is rather similar to linear types and can be formalized using separation logic [32].

Supporting safe, explicit memory management in program- ming languages has been studied in Vault [12] and Cyclone [25]. The verification technique employed in Sing# builds on this earlier work. Type systems based on ownership hi- erarchies [9] or lexically-scoped regions [36] are not strong enough to prove the necessary non-aliasing properties at ar- bitrary ownership transfer points, e.g., when memory must be freed or transferred to other processes.

Real-time Java [8] is a version of Java for real-time con- strained systems. It provides programers with memory ar- eas that have a stack based lifetime. The explicit mem- ory management in RTSJ is runtime verified, not statically checked as in our work, i.e., storing a pointer to an object in a memory area might cause a runtime error as opposed to a compile-time error if the target object lives beyond the memory area’s lifetime. Scoped types [37] proposes a set of rules that statically guarantee the absence of such errors. Still, life-times of memory areas have lexical scopes whereas in our work, a block can get allocated by a process, get trans- ferred to another process, and live beyond the lifetime of the allocating process. Furthermore, our memory model guar- antees that every block is accessed by at most one thread at a time, thus providing statically enforced mutual exclusion. RTSJ to the best of our knowledge does not provide such features.

Guava [3] is a Java dialect providing statically guaranteed mutual exclusion through true monitors. Guava’s stronger exclusion guarantees over Java enable compilers to optmize code more aggressively. Guava achieves mutual exclusion through hierarchical ownership domains [9] called regions. As discussed above, these techniques do not allow true own- ership transfer as described in this paper. As a result, Guava relies on deep copying of data structures. It also does not ad- dress the cross process transmission of data, nor does it have any notion of message passing. As such, the ideas in Guava are very much orthogonal to those presented here and one could imagine combining these system, so that e.g., tracked data could be transferred between ownership domains with- out the need to copy it.

The Erlang language has been successfully used in the telecommunication industry [2]. It is based on a purely func- tional programming model in which all data is read-only and sharing cannot cause unwanted side effects. Depending on the runtime system employed [33], message data is either copied or processes share pointers into shared heaps. The latter scenario makes garbage collection a global affair. Er- lang runtime systems can benefit from the tracked data ap- proach of Sing# by keeping garbage collection process-local without the need to copy messages.

Document info
Document views44
Page views44
Page last viewedTue Jan 17 15:19:50 UTC 2017