Tutorial Overview: Understanding Dynamic Memory Management in Safety Critical Java

摘要

In spite of the high-level abstraction benefits of automatic tracing garbage collection, current prevailing sentiment within the safety certification community is that a simpler memory model is required for the most rigorous levels of software safety certification. Thus, the draft JSR-302 specification for safety critical Java relies on scope-based memory allocation rather than tracing garbage collection. The scoped memory model for JSR-302 is a simplification of the RTSJ model. JSR-302 enforces a strict hierarchy of scopes and distinguishes private scopes, which can be seen only by one thread, from mission scopes, which can be accessed by all the threads that comprise a mission, including threads running within inner-nested sub-missions. The hierarchical memory structure allows implementations to guarantee the absence of memory fragmentation for scope management, unlike the Real-Time Specification for Java from which the JSR-302 specification was derived. In the absence of block structure, it is more difficult in Java to safely manage references to stack-allocated objects than in Ada. While the simplified hierarchical management of scoped memory that is part of JSR-302 addresses memory fragmentation concerns, it does not guarantee the absence of dangling pointers. As with the Real-Time Specification for Java, JSR-302 requires a run-time check to enforce that no reference assignment creates a relationship whereby an outer-nested object is allowed to point to an inner-nested object. This rule assures the absence of dangling pointers, but it introduces a different problem: every assignment to a reference field must be accompanied by a run-time check to validate the appropriate scope nesting relationship. This run-time check will throw a run-time exception if the assignment is deemed inappropriate. The safety certification evidence for a given safety-critical Java program must therefore include an argument for every reference assignment that it will not cause the program to abort with a runtime exception. Furthermore, the certification evidence must prove that sufficient memory is available to reliably execute each safety-critical task in the system. This tutorial provides an overview of dynamic memory management in Safety Critical Java and describes two annotation systems that have been designed to support static (compile-time) enforcement of memory safety properties. The first annotation system is described in an appendix to the draft JSR-302 standard. This relatively simple annotation system, which is not considered normative, serves to demonstrate that memory safety can be statically proven without requiring extensive annotations throughout existing library code. The second annotation system is the system implemented in Perc Pico. This annotation system, which is much richer than the draft JSR-302 annotation, has been in experimental use for over five years. During that time, tens of thousands of lines of experimental application code have been developed, with the experience motivating a variety of refinements to the original design.