CPA-CPL Certified Garbage Collection for Highly Responsive Systems

Purdue University, West Lafayette IN

Investigators

Abstract

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.