SHF: Medium: Collaborative Research: Micro Virtual Machines for Managed Languages: Abstraction, defined and contained

标题：托管语言的微型虚拟机：抽象，包含今天的大部分软件都是用托管语言编写的。这些语言通过在非常高的级别支持编程来提高软件生产率，隐藏了现代计算机硬件和操作系统的复杂性。例如，Java、PHP、Objective-C、Java、C#、Python和Ruby。这些语言具有巨大的经济重要性。不幸的是，这些语言中的大多数效率低下，与C等正统语言选择相比，造成高达50倍的开销。这项研究的更广泛影响是双重的：(1)由于托管语言正日益成为经济的关键，部署在全球电子商务平台和互联网应用程序(包括关键软件公司，如亚马逊、谷歌、Facebook、苹果、甲骨文和微软的引擎室)的引擎室中，提高这些托管语言平台的可靠性和性能将带来经济效率以及资源效率，其形式是降低数据中心的电力成本和提高移动设备的电池寿命；(2)关于计算领域的人类多样性，这项研究将吸引来自代表性不足群体的本科生，并鼓励他们进入研究生院并从事计算和研究工作。这项研究项目正在定义、开发、评估和提炼管理语言实现的新基础层的基本组成部分。在这样做的过程中，它解决了系统效率低下的一个关键来源，开创了“微虚拟机”(MicroVM)作为托管语言实现的高效高性能基板的先河。微VM和现有托管语言实现之间的关系类似于操作系统微内核和诸如Linux的单片操作系统之间的关系。微VM抓住了这样一个观点，即大多数现代语言都有一个定义良好的基础，可以负责硬件、并发性和内存的基本抽象。通过隔离和暴露这种底层，微VM体现了语言实现者可用的最先进的基础技术，同时将他们与这些抽象的有害复杂性隔离开来，使他们能够专注于所有重要的特定于语言的优化。这项研究使软件效率更高，并使语言执行研究和开发的重点明显更加突出。研究的智力价值是：(1)研究并通过原型和评估识别正确的微VM抽象，允许将低级语言中立的关注点和高级语言特定的关注点清楚地分开，捕获核心行为，同时也承认高性能的语言实现；(2)产生次要的研究挑战，特别是关于硬件、并发性和内存的抽象的有效和高效的组合；以及(3)创建正式验证的可行目标，因为微VM具有相对较小的代码基，从而在迈向可信赖的子系统以保证托管软件的道路上迈出了一步。

Title: Micro Virtual Machines for Managed Languages: Abstraction, containedA large fraction of today's software is written in managed languages. These languages increase software productivity by supporting programming at a very high level, hiding the complexity of modern computer hardware and operating systems. Examples include JavaScript, PHP, Objective-C, Java, C#, Python, and Ruby. These languages have great economic importance. Unfortunately, most of these languages are inefficient, imposing overheads as large as a factor of fifty compared to orthodox language choices such as C. The broader impacts of this research are two-fold: (1) Since managed languages are increasingly becoming economic linchpins, deployed in the engine rooms of global e-commerce platforms and Internet applications (including those of key software companies such as Amazon, Google, Facebook, Apple, Oracle, and Microsoft), improving the reliability and performance of these managed language platforms will lead to economic efficiencies as well as resource efficiencies in the form of reduced power costs to data centers and improved battery lifetime on mobile devices;(2) Concerning human diversity in the computing field, the research will engage undergraduates from under-represented groups, and encourage them to pursue graduate school and careers in computing and research.This research project is defining, developing, evaluating, and refining the essential components of a new foundation layer for managed language implementation. In doing so, it addresses a key source of systemic inefficiency, by pioneering the "micro virtual machine" (microVM) as an efficient high-performance substrate for managed language implementation. The relationship between a microVM and existing managed language implementations is analogous to that between an operating system micro kernel and monolithic operating systems such as Linux. The microVM captures the insight that there exists a well-defined foundation common to most modern languages that can take responsibility for fundamental abstractions over hardware, concurrency, and memory. By isolating and exposing this substrate, the microVM embodies state-of-the-art base technology available to language implementers while isolating them from the pernicious complexities of these abstractions, freeing them to focus on all-important language-specific optimizations. The research is enabling more efficient software and a distinctly sharper focus for language implementation research and development. The intellectual merits of the research are: (1) Researching and identifying, via prototyping and evaluation, the right microVM abstractions, allowing clean separation of low-level language-neutral and high-level language-specific concerns, capturing the core behaviors, while also admitting high-performance language implementations; (2) Generating secondary research challenges, especially with regard to the effective and efficient combination of abstractions for hardware, concurrency, and memory; and (3) Creating a viable target for formal verification because the microVM has a relatively small code base, thus taking one step on the way towards trustworthy subsystems for assurance of managed software.