Compared to the channels described in this paper, Erlang uses port based communication and messages can be re- ceived out of order. The language does not statically guard against “message not understood errors”, but a global static analysis ensuring that processes handle all messages sent to them is described in .
Specifying and statically checking the interaction among communicating threads via protocols is the subject of nu- merous studies [24, 21, 17, 27, 16]. From a theoretical view point, the work on session types for inter-process commu- nication by Gay et al.  is closely related to ours. The session types have the same expressive power as our channel contracts and their type system also keeps track of aliases to determine proper ownership management of endpoints.
To our knowledge, this work is the first to integrate a full- fledged garbage-collected language with statically verified channel contracts and safe zero-copy passing of memory blocks. The main novelty of the work is the enabling of simple and efficient implementation techniques for channel communication due to the system-wide invariants guaran- teed by the static verification. Our channel contracts are expressive and support passing channel endpoints and other memory blocks as message arguments with zero-copy over- head.
The message-based programming model is well supported by the language through a switch receive statement which allows blocking on complicated message patterns. The static checking prevents ownership errors and helps programmers handle all possible message combinations, thereby avoiding “message not-understood errors”. The runtime semantics restricts channel failure to be observed on receives only, thus eliminating handling of error conditions at send operations where it is inconvenient.
Our programming experience with the language and chan- nel implementation has been positive. Programmers on the team, initially skeptical of the value of contracts, now find them useful in preventing or detecting mistakes. The chan- nel contracts provide a clean separation of concerns between interacting components and help in understanding the sys- tem architecture at a higher level.
8.1 Future Work
We already mentioned the need to deal with exceptional control flow in the static verification. We are also develop- ing extensions to the channel contracts that enable static prevention of deadlock in the communication of processes. Finally, we are investigating how to build abstractions over channel objects and communication while retaining their asynchronous nature and the static checking of the protocol.
The present work would not have been possible without the effort of a large number of people. We would like to thank Paul Barham, Nick Murphy, and Ted Wobber for feedback and putting up with a research compiler and experimental static analysis. Thanks to Qunyan Mangus, Mark Plesko, Bjarne Steensgaard, David Tarditi, and Brian Zill for imple- menting support for the exchange heap in the Kernel and the Bartok native code compiler. Special thanks goes to Her- man Venter for providing the inital compiler infrastructure and support.
 Partition III: CIL Instruction Set. ECMA Standard 335 http://www.ecma- international.org/publications/standards/Ecma- 335.htm.
 Joe Armstrong, Robert Virding, Claes Wikstr¨om, and Mike Williams. Concurrent Programming in Erlang. Prentice-Hall, second edition, 1996.
 David F. Bacon, Robert E. Strom, and Ashis Tarafdar. Guava: A Dialect of Java without Data Races. In Proceedings of 2000 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’00), pages 382–400, October 2000.
 F.R.M. Barnes, C.L. Jacobsen, and B. Vinter. RMoX: a Raw Metal occam Experiment. In Communicating Process Architectures 2003, WoTUG-26, Concurrent Systems Engineering, ISSN 1383-7575, pages 269–288, September 2003. ISBN: 1-58603-381-6.
 F.R.M. Barnes and P.H. Welch. Mobile Data, Dynamic Allocation and Zero Aliasing: an occam Experiment. In Communicating Process Architectures 2001, number 59 in Concurrent Systems Engineering Series, pages 243–264. IOS Press, Amsterdam, The Netherlands, September 2001.
 Forest Baskett, John H. Howard, and John T. Montague. Taks communication in DEMOS. In Proceedings of the Sixth ACM Symposium on Operating Systems Principles, pages 23–31, 1977.
 Brian N. Bershad, Craig Chambers, Susan Eggers, Chris Maeda, Dylan McNamee, Przemyslaw Pardyak, Stefan Savage, and Emin Gu¨n Sirer. SPIN: An Extensible Microkernel for Application-specific Operating System Services. In Proceedings of the 6th ACM SIGOPS European Workshop, pages 74–77, 1994.
 Greg Bollella, James Gosling, Ben Brosgol, Peter Dribble, Steve Furr, and Mark Turnbull. The Real-Time Specification for Java. Addison-Wesley, June 2000.
 David G. Clarke, James Noble, and John Potter. Simple Ownership Types for Object Containment. In 15th European Conference on Object-Oriented Programming (ECOOP 2001), volume 2072. Lecture Notes in Computer Science, 2001.
 Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Conference Record of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, January 1999.
 Fabien Dagnat and Marc Pantel. Static analysis of communications for Erlang. In Proceedings of 8th International Erlang/OTP User Conference, 2002.
 Robert DeLine and Manuel F¨ahndrich. Enforcing High-Level Protocols in Low-Level Software. In Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation (PLDI ’01), pages 59–69, 2001.
 Sean Dorward, Rob Pike, and Phil Winterbottom. Programming in Limbo. In Proceedings of COMPCON. IEEE, 1997.