CPA-CPL Certified Garbage Collection for Highly Responsive Systems

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

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.