Language support for fast and reliable message-based communication in singularity OS
Language support for fast and reliable message-based communication in singularity OS
复制标题
奇点操作系统中快速可靠的基于消息的通信的语言支持
DOI：
10.1145/1217935.1217953
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Steven P. Levi
中科院分区：
文献类型：
--
作者：
M. Fähndrich;Mark Aiken;C. Hawblitzel;O. Hodson;G. Hunt;J. Larus;Steven P. Levi
基于消息的通信提供了提供更强规格和组件之间更清洁的分离的潜在好处。与共享内存互动相比，消息传递具有更昂贵的数据交换（无直接共享）和更复杂的编程的潜在缺点。在本文中，我们报告了有关语言，验证和运行时系统功能，使消息可实用奇点操作系统中过程之间交流的唯一手段。我们表明，使用先进的编程语言和验证技术，可以提供和强制执行强大的系统范围的不变性，从而实现有效的通信和基于软件的流程隔离。此外，沟通渠道的规格有助于早日检测程序员错误 - 即在编译时 - 从而减少了基于消息的编程模型的难度。本文描述了我们的通信不变性，语言和验证功能，支持它们的语言和验证功能，以及基础架构的实施细节。许多基准表明这种方法的竞争力。
Message-based communication offers the potential benefits of providing stronger specification and cleaner separation between components. Compared with shared-memory interactions, message passing has the potential disadvantages of more expensive data exchange (no direct sharing) and more complicated programming.In this paper we report on the language, verification, and run-time system features that make messages practical as the sole means of communication between processes in the Singularity operating system. We show that using advanced programming language and verification techniques, it is possible to provide and enforce strong system-wide invariants that enable efficient communication and low-overhead software-based process isolation. Furthermore, specifications on communication channels help in detecting programmer mistakes early---namely at compile-time---thereby reducing the difficulty of the message-based programming model.The paper describes our communication invariants, the language and verification features that support them, as well as implementation details of the infrastructure. A number of benchmarks show the competitiveness of this approach.