CPA-CPL Certified Garbage Collection for Highly Responsive Systems

正在用Java开发数百万条线路系统，用于航空电子、舰船计算和模拟。用于此类系统的Java实时规范的一个主要吸引力在于，它使开发在同一环境中以内存安全的方式混合硬、软和非实时任务的应用程序成为可能。不幸的是，这些优势是以实时子系统的可预测性为代价的。Java中这种不可预测性的主要罪魁祸首之一是垃圾回收，它通常需要应用程序中断数百毫秒。这种暂停在实时系统中是不可接受的。解决这一关键问题的一种方法是开发实时垃圾收集器(RTGC)，该收集器具有最坏情况下的暂停时间界限和最小赋值器利用率。RTGC研究仍处于初级阶段。就其提供的定时保证的强度而言，当前算法的适用性是有限的。此外，在安全和任务关键型环境中使用RTGC的一个严重限制是软件的认证问题。在目前的技术状态下，还没有正式验证过垃圾收集器。如果没有这些保证，采用的希望就很小。本研究包括高级语言实时虚拟机的两个关键问题的工作。首先，它正在探索基于概率无锁同步的RTGC新方法，这种方法提供了强大的定时保证，而被违反的概率几乎为零。其次，利用定理证明生成了一个可证明正确的垃圾收集算法。这一步对于高级运行时环境的确定至关重要，众所周知，这是以前从未尝试过的。RTGC原型是在高性能开源实时Java虚拟机的环境下实现的。该实验平台是对Java的工业级实现，它是唯一经过测试(与波音公司合作)的Java虚拟机。结果包括一套大型实时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.