CPA-CPL Certified Garbage Collection for Highly Responsive Systems

CPA-CPL 认证的高响应系统垃圾收集

• 批准号: 0811691
• 负责人: Jan Vitek
• 金额: $ 39万
• 依托单位: Purdue University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-08-01 至 2012-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0811691&HistoricalAwards=false
• 关键词: CPA; CPL; Certified; Garbage; Collection

Multi-million line systems are being developed in Java for avionics, shipboard computing and simulation. A key attraction of the Real-Time Specification for Java for such systems is that it makes it possible to develop applications that mix hard-, soft-, and non-real-time tasks in the same environment in a memory-safe way. Unfortunately these advantages come at the expense of predictability of the real-time subsystems. One of the main culprits for such unpredictability in Java is garbage collection, which often requires applications to be interrupted for hundreds of milliseconds. Such pauses are not acceptable in real-time systems. One way to address this critical problem is to develop real-time garbage collectors (RTGC) with worst-case bounds on pause times and minimum mutator utilization. RTGC research is still in its infancy. There are limits to the applicability of current algorithms in terms of the strength of the timing guarantees that they offer. Furthermore, one serious limitation to the use of RTGC in safety- and mission- critical settings is the issue of certification of the software. In the current state of the art, no garbage collector has been formally verified. Without these guarantees there is little hope of adoption.This research comprises work on two crucial issues in real-time virtual machines for high-level languages. First, it is exploring new approaches to RTGC based on probabilistic lock-free synchronization that provide strong timing guarantees that have a vanishingly small probability of being violated. Second, it uses theorem proving to generate a provably correct garbage collection algorithm. This step is critical for certification of advanced runtime environments and, as best is known, has never been attempted before. RTGC prototypes are being implemented in the context of a high-performance open source real-time Java virtual machine. This experimental platform is an industrial strength implementation of Java which is the only Java virtual machine to have been flight tested (in a collaboration with Boeing). Outcomes include empirical results for a suite of large real-time Java programs. All results are being released as open source.

目前正在用Java开发数百万行系统，用于航空电子设备、舰载计算和仿真。一个关键的吸引力的实时物种fi Java在这类系统中的优势在于，它可以以内存安全的方式在同一环境中开发混合硬、软和非实时任务的应用程序。不幸的是，这些优点是以牺牲实时子系统的可预测性为代价的。Java中这种不可预测性的罪魁祸首之一是垃圾收集，这通常需要应用程序中断数百毫秒。这种暂停在实时系统中是不可接受的。解决这一关键问题的一种方法是开发实时垃圾收集器（RTGC），它具有最坏情况下的暂停时间和最小mutator利用率。RTGC研究仍处于起步阶段。就它们提供的定时保证的强度而言，当前算法的适用性存在限制。此外，在安全和使命关键设置中使用RTGC的一个严重限制是软件的认证问题。在现有技术中，还没有垃圾收集器被正式验证&。ed.没有这些保证是希望不大的通过。这项研究包括工作的两个关键问题，在实时虚拟机的高级语言。首先，它正在探索基于概率无锁同步的RTGC新方法，这些方法提供了强有力的时序保证，而被违反的概率非常小。其次，它使用定理证明来生成可证明正确的垃圾收集算法。此步骤对于高级运行时环境的认证至关重要，众所周知，以前从未尝试过。RTGC原型正在高性能开源实时Java虚拟机的上下文中实现。这个实验平台是Java的工业强度实现，Java是唯一经过#64258;ight测试的Java虚拟机（与波音公司合作）。结果包括一套大型实时Java程序的实证结果。所有结果均以开源形式发布。