A Type System to Assure Scope Safety within Safety-Critical Java Modules

ABSTRACT

To address the needs of safety-critical system developers, a type system based on Java 5.0 meta-data annotations and special byte-code verification techniques is described. This type system enables programmers to develop code for which the byte code verifier is able to prove the absence of scoped memory protocol errors, thereby eliminating the need for run-time assignment checks. Benefits of the type system include improved software reliability, easier maintenance and integration of independently developed real-time software modules, and higher performance.

1. INTRODUCTION

In the traditional information processing domain, Java’s high-level support for scalable composition of software modules is among its most highly valued benefits in comparison with C and C++. A difficulty with integration and maintenance of real-time software modules written according to the NoHeapRealtimeThread conventions of the Real-Time Specification for Java (RTSJ) [1] is that scope properties of independently developed modules do not compose in a modular fashion. Modules that follow proper scoped memory conventions in one context are likely to violate scoped memory convention if integrated with other modules in a different context. The type system described in this paper assures that independently developed real-time modules compose in a modular fashion.

Several important factors combine to motivate development of a RTSJ scope-safe type system to support developers of safety-critical software. Among these are the following:

1. The safety-critical development community desires to leverage commercially popular technologies such as Java rather than specialized niche technologies such as Ada because free-market competition among a broader supplier base delivers higher quality technologies for lower prices.
    

2. Safety-critical systems need to pass stringent certification requirements. Certification authorities expect proofs that programs function correctly. Certification guidelines also recommend elimination of all dead code, and require independent proofs that any deployed dead code is “deactivated”, meaning the code will never be executed. Run-time assignment checks are very problematic, because they add significantly to the burden of proof associated with certification of safety-critical software.
    

3. The size and complexity of safety-critical software continues to grow. Because the costs of developing and certifying safety-critical software modules are so high, there is increasing pressure to reuse safety-critical modules and their certification artifacts. This demands a strong separation of concerns between independently developed software modules. Traditional whole-program analysis techniques are problematic because a small change to a single module may invalidate all of the certification artifacts in the system. For many development organizations, this is cost prohibitive.
    

4. The desire to reuse safety-critical software modules also scales to the domain of mission-critical systems that do not require safety certification. Whenever there are common functional requirements between safety- and mission-critical systems, the industry generally prefers solutions that allow them to maintain a single implementation of the common functionality. Thus, there is a general desire to allow code written to the stringent safety-critical requirements to be deployed in mission-critical systems which may be larger, more complex, and more dynamic than typical safety-critical deployments. For this reason, there is a desire to be able to support dynamic loading of safety-certified real-time modules.

The domain of problems addressed by safety-critical development is much smaller than the domains targeted by full RTSJ. This is because the certification requirements for safety-critical software significantly restrict the flexibility and freedom of developers. Thus, safety-certified software systems tend to be smaller, simpler, and more static than typical command and control environments.

Though the final specification has not yet been completed, consensus has been reached on various issues. In particular, the safety-critical profile will not support execution of traditional java.lang.Thread, nor of javax.realtime.RealtimeThread. Thus, there is no garbage-collected heap within the safety-critical Java execution environment. We have also decided to forbid safety-critical programs from overriding Object.finalize(). Together, these restrictions simplify development of a safety-critical Java scope-safe type system.

2. RELATED WORK

Others have examined the challenge of using type systems to make the use of scope- or stack-based memory allocation safe. The Cyclone system seeks to establish a safe alternative to C [2]. Cyclone introduces a type system to support safe stack allocation and deallocation of memory, and combines this with explicit safe deallocation of heap objects, along with automatic conservative garbage collection. A project at MIT has also developed a type system for safe region-based memory management of RTSJ programs [3]. Though the MIT system has many similarities with the approach described in this paper, a key difference deals with identification of scope levels in argument lists. The MIT approach requires that every scoped argument be associated with a particular named scope, whereas the approach described in this paper, for the most part, simply identifies that certain referenced objects may reside in scoped memory, without requiring programmers to differentiate one scope from another. For certain special circumstances, the type system described in this paper allows programmers to require that certain incoming scoped arguments reside in more outer-nested scopes, or at the same scope level, as certain other scopes that are relevant to execution of a particular method or constructor. While the MIT approach is capable of describing more complicated algorithms and data structures, the MIT type system imposes far greater restrictions on the generality of individual software modules. This hinders software reuse and increases the volume of code that must be written and certified. A third approach to type-safe scoped memory has been described in reference [4]. This approach makes use of existing aspect-oriented programming tools to analyze and transform stylized Java source code. A fourth approach, representing a precursor to this document, is described in reference [5]. This precursor document provides a more comprehensive and detailed description of the type system than is allowed by workshop space constraints.

All three of the Java-based scope-safe type systems described above recommend that real-time programmers use a different API than the vanilla RTSJ memory management libraries, and use an automatic translation system to convert code to vanilla RTSJ. In this paper, we describe an approach that eliminates the need for automatic translation.

3. THREAD STACK MEMORY MODEL

The RTSJ introduced the notion of "scoped memory" as an alternative to automatic garbage collection. This proposed safety-critical Java profile supports the notion of scoped memory, but hides the RTSJ APIs that manipulate memory scopes. Instead, safety-critical Java programmers describe their intentions with respect to use of scoped memory by using annotations which can be statically analyzed and enforced at compile time. The safety-critical Java profile also supports the notion of "immortal memory", which represents the outer-most memory scope. Objects allocated within the immortal memory region will not be reclaimed.

The need to support temporary memory allocation within real-time programs has been well motivated. At the same time, there is general agreement that developers of hard real-time modules do not require the full generality and flexibility offered by automatic garbage collection.

Within the RTSJ, hard real-time programmers are encouraged to use the LTMemory abstraction. This service makes it possible to allocate new memory within a dynamic scope in time that is proportional to the size of the allocation request. A developer of hard real-time software must face several significant difficulties with the use of this abstraction:

1. Knowing how big to make an LTMemory region in order to reliably support execution of a particular real-time module is quite difficult and error prone. Furthermore, it is non-portable between different compliant RTSJ implementations.
    

2. Instantiation of an LTMemory region is not a hard real-time operation. There is no bound on how much time this will take, and there is, in fact, no guarantee that a request to instantiate an LTMemory region will succeed even if there is sufficient available memory in the system at the time of the request. This is because memory may become fragmented during the course of a program’s execution.

Many RTSJ programmers overlook these difficulties with use of the LTMemory abstraction. They regularly allocate and discard LTMemory objects, and successful execution of test programs instills confidence that the code will work reliably in the field. This is a dangerous practice, because it is not generally possible to test all of the different ways that the allocation pool might become fragmented. Further, the program may not behave the same way if it is moved to a different vendor’s compliant RTSJ implementation, or even if the same vendor provides a new maintenance release of the same RTSJ implementation.

RTSJ programmers who understand and appreciate the risks of memory fragmentation find that the only way to reliably and safely use LTMemory abstractions in their hard real-time code is to allocate all of the LTMemory objects that their application might need during initialization of the application. This adds significantly to the difficulty of implementing and maintaining the software, and adds considerably to the amount of memory required for reliable execution of the application since many of the LTMemory instances allocated during startup sit idle throughout most of the program’s execution.

The hard-real-time Java profile addresses these issues by providing static analysis tools to determine the amount of memory required to execute particular program modules and by requiring all creation and destruction of scopes to follow a strict LIFO (stack) ordering.

At startup, all of the workspace memory available to support execution of the program is set aside as the run-time stack for the main hard real-time Java thread. If the application needs to support more than a single thread, the main program carves memory from its run-time stack to represent the run-time stacks for each of the threads it spawns.

Figure 1 illustrates the organization of the main thread’s run-time stack immediately after it has spawned three new threads. This illustration assumes that all three threads were spawned from the same context within the main thread.

 Note that space has been reserved within the main thread’s stack to allow the main thread to continue to populate its run-time stack. Note also that it is essential at this point in the program’s execution to know the amount of memory that must be reserved to represent each of the spawned thread’s run-time stacks. These stacks need not be the same size. In a typical application, the size of each stack is custom-tailored to the needs of the given thread.

As execution proceeds, each of the three spawned threads and the main thread will continue to populate their respective stacks. Assume the stack memory is organized as shown in Figure 2 at a subsequent execution point.

The scoped memory usage guidelines, as defined in the RTSJ, allow inner-nested objects to refer to objects residing in more outer-nested scopes, but forbids references that go in the opposite direction. These scope-nesting restrictions guarantee that there will never exist a dangling pointer from an outer-nested object to an inner-nested memory location that no longer exist because its inner-nested scope has been reclaimed.

Given these conventions, any data structures that must be shared between multiple threads need to reside either in immortal memory (the outer-most scope, which is never reclaimed) or must exist within the parent or some other ancestor thread’s stack below the point at which the descendent thread was spawned. Shared objects do not necessarily need to exist at the time the subthreads are spawned, but the memory allocation contexts within which the shared objects will eventually be allocated must be set aside and entered within the parent thread’s stack before the point at which the child thread is spawned.

A special protocol must be enforced to support these conventions. In particular, whenever an ancestor thread desires to unwind its thread stack beyond the point at which it had spawned descendent threads, it must wait for all of the threads that were spawned from this context to terminate execution before it returns from this context. Otherwise, we might create a situation in which a spawned child thread refers to non-existent objects that once resided within the parent’s scope.

This special protocol is enforced by the hard real-time Java byte-code verifier. In particular, the byte-code verifier requires that the spawning of a new thread or BoundAsyncEventHandler occurs within a try statement, and that the corresponding finally statement includes an invocation of the join() operation on the corresponding ThreadStack object. This is exemplified in the following code:

try {
    NoHeapRealtimeThread thread =
        new A_NoHeapRealtimeThread(args);
    ThreadStack stack = new ThreadStack(stack_size);

    stack.spawn(thread);
} finally {
    stack.join();
}

Additional description of the ThreadStack data abstraction is provided in Section 7.

4. TYPE ATTRIBUTES

Every reference variable within a scope-safe program is classified as having one or more of the following five attributes.

The scoped attribute marks variables that may, but need not, hold references to objects residing in scoped memory. A variable that does not have the scoped attribute is not allowed to hold references to objects residing in scoped memory.

The immortal attribute marks variables that are known to hold references to immortal memory, or null. The immortal attribute is mutually exclusive with the scoped attribute.

The array attribute is used in combination with the scoped attribute to identify variables that may hold references to arrays residing in scoped memory, the elements of which are considered to be scoped variables. In the case that an element of a scoped-array object is itself a reference to another array, the referenced array is considered to have the scoped-array attribute. Note that some reference arrays may have the scoped attribute without having the array attribute. Such an array may reside in scoped memory, but its array elements must reside in immortal memory.

The local attribute is used in combination with the scoped attribute to identify variables whose contents cannot be copied into any other variable that could possibly live longer than this variable itself.

The result attribute identifies local reference variables whose value might be returned from the currently executing method.

5. META-DATA ANNOTATIONS

The scope-safe type system uses Java Standard Edition 5.0 style meta-data annotations to characterize the type attributes associated with method and constructor arguments, method return values, instance variables, and static variables. Allowing static variables to hold references to scope-allocated objects anticipates future RTSJ enhancements that would allow classes to be loaded and unloaded within inner-nested scopes. In these circumstances, a dynamically loaded class might have static variables that refer to objects allocated in more outer-nested scoped memory regions. The annotations described in this section are a small subset of the full set of annotations designed for the scope-safe type system. Space does not allow presentation of the full system. See reference [5] for more detail.

The @Scoped annotation applies to instance and static fields, methods, and method and constructor argument declarations to indicate that the corresponding variable has the scoped attribute. When applied to a method, this annotation denotes that the method may return a reference to an object that resides in scoped memory.

The @ScopedThis annotation applies to instance methods and constructors to indicate that within the corresponding method or constructor body, the this variable has the scoped attribute. In order to construct an object within scoped memory, the constructor’s this variable must have the scoped attribute.

The following implementation of a complex number abstraction demonstrates the use of both annotations:

public class Complex {
    float real, imaginary;

    @ScopedThis public Complex(float r, float i) {

        real = r;
        imaginary = i;
    }

    public static boolean realGT(@Scoped Complex c1,                                            @Scoped Complex c2) {

        return (c1.real > c2.real);
    }
}

The @CallerAllocatedResult annotation applies to methods to denote that the caller specifies the context within which the method’s return object will be allocated. Consider introduction of a multiply() method into the Complex class as an example of this annotation:

@CallerAllocatedResult @ScopedPure

public Complex multiply(Complex arg) {

    float r, i;

    r = this.real * arg.real - this.imaginary * arg.imaginary;

    i = this.real * arg.imaginary + arg.real * this.imaginary;

    return ScopeManagement.allocInCallerContext(Complex.class, r, i);

}

This example introduces the @ScopedPure annotation, which is shorthand to denote @ScopedThis and @Scoped for all reference arguments. Before invoking a caller-allocated result method, the caller is required to specify the scope into which it desires the method’s result to be placed.  This is described below, under the subheading  “Invoking a caller-allocated result method”.

There are certain situations under which a constructor may desire to return an object which contains references to other more outer-nested objects. Consider, for example, the following code:

public class String {

    @Scoped StringBuilder data;

    int offset, length; 

    @ScopedThis

    public String(@Scoped StringBuilder sb, int off, int len) {

        data = sb^[1];

        offset = off;

        length = len;

    }
}

The type system requires that any @Scoped arguments to a @ScopedThis constructor reside in scopes that are at equal or more outer-nested scope level than the object to be constructed^[2]. In most constructor invocations, demonstrating compliance with this requirement is trivial, because the typical object is instantiated in the inner-most scope. However, invocation of constructors from within caller-allocated result methods, for example, may introduce violations of this rule. For example, the following source code is rejected by the safety-critical byte-code verifier because the StringBuilder object passed as an argument to the String constructor at line 11 resides in a scope that is nested within the scope that holds the constructed String object:

[1] @CallerAllocatedResult String toString(int i) {

[2] class MethodBody implements Runnable {

[3]          int i_copy;

[4]          @Scoped String result;

[5]          private MethodBody(int i) {

[6]              i_copy = i;

[7]          }

[8]          public void run() {

[9]              StringBuilder b = new StringBuilder(i_copy);

[10]            result = ScopeManagement.

[11]                allocInCallerContext(String.class, b, 0,

[12]                                            b.length());

[13]        }

[14]   }

[15] try {

[16]        ScopedMemory ma = null;

[17]        SizeEstimator size = new SizeEsimator(;

[18]        ma = ScopeManagement.newLocalScope(size);

[19]        r = new MethodBody(i);

[20]        ma.enter(r);

[21]        return ma.result;

[22] } finally {

[23]        ScopeManagement.popScope(ma);

[24]   }

[25] }

In general, the type checker enforces that any @Scoped arguments passed to inner-nested caller-allocated result methods, or to a constructor that initializes an object to be returned from a caller-allocated result method originate outside the current method’s scope. Through inductive reasoning, this proves that the @Scoped arguments passed to any @CallerAllocatedResult method and to any constructor reside in more outer-nested scopes than the object to be constructed.

In certain situations, the code that invokes a caller-allocated result method may choose to request that the caller-allocated result be placed in immortal memory. In this circumstance, the type system requires that all @Scoped arguments passed to the caller-allocated-result method refer to objects residing in immortal memory.

Programmers have an alternative annotation to mark the scoped arguments of constructors and caller-allocated-result methods which might refer to objects residing in scopes that are nested internal to the scope of result object. These arguments are marked with the @ScopedLocal or @ScopedThisLocal annotations. The type system forbids constructors from copying scoped-local arguments to the fields of the newly constructed object.

Another special annotation, @NestedReentrantScope, marks classes for which certain private @Scoped instance variables and all @Scoped arguments sent to, and @Scoped values returned from the instance methods are known by the type system to reside at the same scope that holds this object instance. The type checker enforces these invariants by restricting allocation of the object itself, restricting allocations performed by the object’s instance methods, and restricting assignments to the object’s private instance fields. This annotation is useful when building data structures to represent, for example, balanced binary trees, arbitrary precision numbers, or variants of the java.util.collections libraries. Space constraints do not allow for a complete description of the type checking associated with use of the @NestedReentrantScope or @ReentrantScope annotations. See reference [5] for a more thorough explanation.

6. INFERENCE OF LOCAL ATTRIBUTES

Though Java 5.0 meta-data annotations may be associated with the declarations of local (auto) variables, these annotations are not preserved in the class file representation. Since one of the goals of our design is to enforce the scope-safe type system through byte-code verification, the scope-safe type attributes for local variables must be inferred from context. The type inference system implements the algorithm described below.

In discussing this algorithm, the term “variable” represents temporary locations on the operand stack and dedicated slots within the method’s activation frame. In both cases, a particular variable’s lifetime begins when the value of that memory location is first defined, and ends immediately following the last use of that memory location’s value. By this definition, a given memory location may represent different variables at different times.

1.     All local reference array variables are assumed to be scoped-array-local unless demonstrated otherwise.

2.     All other local reference variables are assumed to be scoped-local unless demonstrated otherwise.

3.     If this method returns a reference result, mark each of the variables passed as an operand to the areturn byte-code instruction as having the result attribute.

4.     By analysis of a method’s data flow, analyze the usage of every scoped-array-local variable. If there exists a path by which its value might be copied to a variable that is:

a.       scoped-array (but not scoped-array-local), change the first variable’s attribute to scoped-array.

b.      scoped-local (but not scoped-array-local), change the first variable’s attribute to scoped-local.

c.       scoped (but not scoped-array-local or scoped-array), change the first variable’s attribute to scoped.

d.      not scoped in any form, change the first variable’s attribute to immortal.

5.     By analysis of a method’s data flow, analyze the usage of every scoped-array variable. If there exists a path by which its value might be copied to a variable that is:

a.       scoped (but not scoped-array), change the first variable’s attribute to scoped.

b.      not scoped in any form, change the first variable’s attribute to immortal.

6.     By analysis of a method’s data flow, analyze the usage of every scoped-local variable. If there exists a path by which its value might be copied to a variable that is:

a.       scoped (but not scoped-array-local or scoped-array), change the first variable’s attribute to scoped.

b.      not scoped in any form, change the first variable’s attribute to immortal.

7.     By analysis of a method’s data flow, analyze the usage of every scoped variable.

a.       If there exists a path by which its value might be copied to a variable that is not scoped in any form, change the first variable’s attribute to immortal.

8.     By analysis of a method’s data flow, analyze the usage of every reference variable that does not have the result attribute.

a.       If there exists a path by which its value might be copied to a variable that has the result attribute, add the result attribute to the first variable’s type description.

In order to assure a consistent interpretation of program semantics, the above analysis is performed on the raw byte-code program before all code optimization.

Note that the algorithm described above may result in changes to the attributes of each local variable. When a local variable’s attribute changes, the type inference engine must reconsider the type inference impact of all assignments to that variable. The type inference engine iterates in search of a fixed point. The upper bound on running time is n³ in the number of local variables and assignments contained within a method. Since most methods contain a relatively small number of local variables and assignments, the execution time is generally tolerable.

7. ALLOCATION LIBRARIES

Undisciplined use of the RTSJ scoped memory API services is difficult (generally intractable) to analyze statically and may result in memory fragmentation of the memory from which scope regions must be allocated. To facilitate static analysis of the relative nesting relationships between scope-allocated objects, and to enable automatic calculation of worst-case scope size requirements, we require that all object allocation conform to the protocols described in this section.

The local scope stack

Conceptually, each method that performs local object allocations introduces a private scope within which the temporary allocations are performed. The programmer is expected to enclose the body of each such method within a try-finally statement of the following form:

Object allocatingMethod(args) {

    class MethodBody implements Runnable {

        <private method’s argument copy declarations>

        <private method’s result copy declaration>

        private MethodBody(<arguments>) {

            copy arguments to instance variables

        }

        public void run() {

            <method body goes here, assigns result

                to result instance variable>

        }

    }

    try {

        // verifier requires that ma be treated as a

        // scoped variable

        ScopedMemory ma = null;

        SizeEstimator size = <initialization-expression>;

        ma = ScopeManagement.newLocalScope(size);

        r = new MethodBody(<argument list>);

        ma.enter(r);

        return <result copy instance variable>;

    } finally {

        ScopeManagement.popScope(ma);

    }

}

Methods that perform no allocations are not required to introduce local scopes. Since the verifier enforces that the local variable ma is treated as a scoped variable, no references to this memory area survive beyond the activation of this method. Thus, the memory that represented by ma is reclaimed by the popScope() method.

Allocation within constructors

If a constructor allocates objects which are to be referenced directly or indirectly from the object that is being constructed, these allocations must be served from the same scope that holds the newly constructed object itself. In order to facilitiate enforcement of allocation budgets for particular modules, a topic not discussed thoroughly in this paper, we require that all such allocations be syntactically distinguished. The following code template represents allocation within a constructor’s persistent scope.

ScopeManagement.allocInConstructorScope(this, Foo.class, <constructor arguments>)
 

We pass this to the method as a marker to help identify the memory area within which the object is being constructed. The second argument is of type Class, and must be specified using the <class-name>.class notation to enable static analysis of the code. The remaining arguments are passed using Java 5.0 varargs conventions. Note that the run-time implementation of this service requires temporary allocation of an Object array to hold the argument list. Thus, the constructor that uses this service must push a temporary allocation scope onto the local scope stack.

Allocation within reentrant scopes

Classes identified with the @ReentrantScope annotation establish a scope at construction time within which new objects subsequently created by instance methods of the class may be allocated. Within the constructor, the program is expected to invoke the ScopeManagement.establishReentrantScope() method, passing as an argument a SizeEstimator object to represent the desired size of the reentrant scope allocation region^[3]. This method returns a reference to the MemoryArea object within which subsequent reentrant scope allocations are to be performed. The constructor should assign the returned value to a final private instance variable of type MemoryArea and name reentrantScope. Within the reentrant-scope class’s instance methods, each allocation of an object within the reentrant scope invokes the allocInReentrantScope() service. Since this method expects Java 5.0 style varargs parameters, the implicitly created array must be allocated in a temporary scope that is reclaimed upon return from the instance method. All invocations of these services should match the pattern shown by the following sample code:

@ReentrantScope public class Baz {

    private final MemoryArea reentrantScope;

    Baz() {

        SizeEstimator z = new SizeEstimator();

        reentrantScope = ScopeManagement.

            establishReentrantScope(z);

        <other initialization goes here>

    }

 

    Object instanceMethod(<method-arguments>) {

        class MethodBody implements Runnable {

            MemoryArea reentrantScope;

            <declarations for private method’s argument copies>

            public Object methodResult;

            private MethodBody(MemoryArea ma, <method-arguments>) {

                reentrantScope = ma;

                <copy method arguments to instance variables>

            }

            public void run() {

                <method body goes here>

                // reentrant-scope allocation looks like:

                // this.field = ScopeManagement.allocInReentrantScope(

                //      reentrantScope, Foo.class, <constructor-args>);

                methodResult = <result>;

            }

        }

        try {

            // verifier requires that ma be treated as a

            // scoped variable

            ScopedMemory ma = null;

            SizeEstimator size = <initialization-expression>;

            ma = ScopeManagement.newLocalScope(size);

            r = new MethodBody(reentrantScope, <method-arguments>);

            ma.enter(r);

            return r.methodResult;

        } finally {

            ScopeManagement.popScope(ma);

        }

    }

}

Invoking a caller-allocated result method

The run-time environment maintains a stack of caller-specified allocation scopes. Before invoking a method that is declared with the @CallerAllocatedResult or @CallerAllocatedArrayResult annotations, the caller must assure that the top of the caller-specified allocation scope stack holds a reference to the MemoryArea that is to hold the result of the method’s invocation. Depending on the caller’s requirements, it may desire that the caller-allocated method place its result in the caller’s local allocation scope, in immortal memory, the caller’s shared reentrant scope, a constructor’s persistent scope, or in the caller’s caller-allocated scope. The methods to establish each of these caller-specified allocation scopes are respectively named: localCallerAllocationScope(), immortalCallerAllocationScope(), and constructorCallerAllocationScope(). All are static methods of the ScopeManagement class. If a method that is declared to return a caller-allocated result invokes another @CallerAllocatedResult method to produce the result to be returned from the first method, there is no need to push a new value onto the caller-specified allocation context stack.

The methods that identify caller-specified allocation scopes each return the previously active caller-specified allocation scope. The caller is responsible for saving this value and restoring it upon return from the caller-allocated-result method. The general pattern mimics the following template:

MemoryArea outer_context;

try {

    outer_context = ScopeManagement.localCallerAllocationScope();

    <invoke caller-allocated-result method>

} finally {

    ScopeManagement.restoreCallerAllocationScope(outer_context);

}

Returning a caller-allocated result

When a method is declared with the @CallerAllocatedResult or @CallerAllocatedArrayResult annotations, the value returned from the method, including elements of the array in the latter case, are all allocated in the caller-specified context. To allocate a result object from within a caller-allocated result method, use the ScopeManagement.allocInCallerContext() method, which takes as arguments the Class to be instantiated and the constructor arguments as a varargs parameter list. To allocate an array of primitives, invoke ScopeManagement.allocPrimitiveArrayInCallerContext(), passing the desired array length as an integer, and the type of each element as a java.lang.Class reference. To allocate an array of references, invoke ScopeManagement.allocArrayInCallerContext(), passing the same arguments.

Allocating in immortal memory

Occasionally, it is necessary to allocate objects within immortal memory. This is generally rare, reserved for initialization phases of a software system’s execution. We require the @ImmortalAllocation annotation on all methods and constructors that allocate immortal memory to reduce the likelihood that accidental allocations will result in unwanted memory leaks. To allocate in immortal memory, use ScopeManagement.allocInImmortal(), ScopeManagement.allocPrimitiveArrayInImmortal(), or ScopeManagement.allocArrayInImmortal(). These are parameterized the same as the caller-specified context allocators.

Spawning subthreads

To support efficient and reliable use of defragmented memory for representation of the thread’s operand and scope stacks, we require that the starting of every NoHeapRealtimeThread and of every BoundAsyncEventHandler be orchestrated through the use of a special ThreadStack programming abstraction. In the proposed safety-critical profile, we forbid thread activation of RealtimeThread, Thread, and (unbound) AsyncEventHandler. A ThreadStack may be allocated either within immortal memory (using an invocation of ScopeManagement.allocInImmortal()), or within scoped memory, simply using new to allocate within the currently active local scope context. The conventions are as follows:

1.     An argument to the ThreadStack constructor specifies the size of the stack.

2.     To start execution of a BoundAsyncEventHandler or NoHeapRealtimeThread, using the ThreadStack memory for temporary representation of the corresponding operand and scope stacks, invoke the ThreadStack.spawn() method, supplying as an argument a reference to the corresponding NoHeapRealtimeThread or BoundAsyncEventHandler objects. This is the only legal way to start up a new thread within the proposed safety-critical RTSJ profile.

3.     If a ThreadStack is allocated in immortal memory, the scope stack for any spawned thread is initially empty.

4.     If a ThreadStack is allocated in scoped memory, the scope stack for any spawned thread inherits from the allocating thread. In other words, the outer-most scope of a spawned thread descends from the inner-most scope of the parent thread at the time the ThreadStack allocation is performed.

5.     For any ThreadStack that is scope allocated, the byte-code verifier requires that the parent thread joins the spawned ThreadStack before returning from the context in which it allocated the ThreadStack. This ensures that ThreadStack memory is deallocated in LIFO order, thereby assuring absence of stack memory fragmentation.

6.     ThreadStack supports a joinAndSpawn() service to allow the ThreadStack memory to serve a different NoHeapRealtimeThread or BoundAsyncEventHandler after the originally associated thread terminates its execution.

8. BYTE-CODE VERIFICATION

Space constraints limit the discussion of byte-code verification to a high-level overview. A more complete description is available in reference [5]. Key concepts are discussed in this section.

Localizing references to scope-allocated objects

To enable compile-time assurance of scope safety, the verifier enforces that the content of a scoped variable is never assigned to another variable that is not scoped. Likewise, it enforces that scoped-local values are never copied to variables that are not identified as scoped-local variables.

Assuring scalable composition of modules

An important benefit that has made Java more popular than C and C++ for traditional information processing applications is the ease with which independently developed modules are assembled into large and complex software systems. One goal of the scope-safe type system is to assure that the scope semantics of individual modules are clearly identified in the annotated API definitions of the modules. These annotations make it possible for software developers and maintainers to easily determine whether particular modules compose simply by examining the interface declarations for those modules.

To enable scalable software development, the verifier enforces consistency between overriding method declarations in subclasses and superclasses. If, for example, the superclass definition of a method declares its first argument to have the @Scoped attribute, all subclass implementations of the same method must also declare the first argument to be @Scoped or @ScopedLocal. And if a method is declared with @ImmortalAllocation, all overridden superclass methods must also carry the @ImmortalAllocation annotation. Also, @ImmortalAllocation methods and constructors may only be invoked from contexts that are themselves declared with the same annotation. This assures that programmers do not inadvertantly invoke a method that performs allocation in immortal memory.

Work is under way to integrate the byte-code verifier within the Eclipse development environment, as illustrated in Figure 3. When the programmer saves his files, the Eclipse build system automatically invokes the PERC Pico verifier and any errors detected by the enhanced byte-code verifier are immediately displayed within the Eclipse edit window.

Enabling code patterns that elide scope checks

In safety-critical systems, developers are required to offer certification artifacts that prove to the satisfaction of peer reviewers and certifying authorities that code runs correctly, without abnormal termination because a run-time assignment check detects an illegal assignment.

The byte-code verifier is required to perform certain analyses in order to justify that particular assignments are scope safe. For example, when assigning to a @Scoped field of an object, the verifier recognizes the following conditions as not requiring a run-time assignment check:

1.     If the object that contains the field to be assigned was just allocated within this thread’s inner-most local scope context, the verifier recognizes that any values assigned to this field reside in the same or outer-nested contexts.

2.     If the value to be assigned was copied from another reference field (or array element) of the same object, the verifier recognizes that the assigned reference value refers to an object residing in the same or outer-nested context.

3.     If the value to be assigned was copied from another reference field (or array element) of an object that was reachable from the object that is being assigned to, the verifier recognizes that the assigned reference value refers to an object residing in the same or outer-nested context.

4.     If a reference value being returned from a method was passed in as an argument to the method, or was reachable from one of the objects passed in as arguments to the method, the verifier recognizes that the returned value is visible in the scope of the caller’s method.

All of the above-described analyses are based on data-flow analysis of reaching definitions within the unoptimized byte-code representation of each software module.

More sophisticated byte-code analysis rules deal with more complex software constructs. For example, the verifier enforces at the point of invocation that all of the @Scoped (but not necessarily the @ScopedLocal) arguments of a method declared with the @CallerAllocatedResult annotation reside in scopes that are at the same or more outer-nested scope level than the scope that holds the caller-allocated result. Based on inductive reasoning, the byte-code verifier allows the values of incoming @Scoped arguments to be assigned to the fields of the caller-allocated result object without requiring a run-time assignment check. Similar analysis enables certain check-free assignments within the instance methods of @NestedReentrantScope classes.

9. EXPERIENCE

A prototype byte-code verifier that enforces rules similar to those described in this paper was implemented and tested on a proposed scope-safe profile of the RTSJ and java.lang libraries. This code represents more than 20,000 lines of reusable real-time software modules. We have also ported several benchmarks to the scope-safe type system, including the FFT benchmark of the Java Grande Forum, the prismjlight benchmark developed by Boeing, and the CaffeineMark benchmark. These experiments have demonstrated that the type system is sufficiently expressive to support scope-safe solutions to a broad variety of real-time programming challenges. Evaluation of several synthetic benchmarks demonstrates that scope-safe Java programs run between 8% and 226% faster than Java HotSpot. This is because they incur neither the run-time overheads of real-time garbage collection, nor the run-time overheads of scope enforcement.

The effort required to convert vanilla RTSJ and vanilla Java code to the scope-safe type system is facilitated by enforcement of the scope-safe type system. The porting process typically consists of:

1.     Copying the standard-edition or RTSJ Java source code into a directory appropriate for use of the Eclipse development environment with the special byte-code verification tools;

2.     Setting up a Makefile or Eclipse to build the desired program using the safety-critical Java tool chain; and

3.     Repeatedly:

a.       compiling the code,

b.      examining the error messages produced by the byte-code verifier, and

c.       adding appropriate annotations and/or refactoring the code to address the problems identified in the error messages.

This is a very different process than the typical effort required to port traditional Java to vanilla RTSJ. In order to port traditional Java code, programmers generally need to understand the program’s memory allocation behavior (a non-trivial task for programs that might consist of tens if not hundreds of thousands of lines of code), and need to map all memory allocation operations to appropriate RTSJ scopes (or to the immortal region). With traditional RTSJ porting, programmers are rarely confident that they’ve done the port correctly, and generally depend on extensive testing to make sure the ported code does not result in illegal assignments, illegal fetches, or scope cycles. Even then, there often remains a lingering uncertainty that testing has not fully exercised all of the paths and data values that might possibly lead to violation of scoped-memory protocol rules.

For many applications, the process of porting to the scope-safe type system is straightforward. For example, the effort required to properly annotate the vanilla Java Grande FFT benchmark was roughly half a day for one software engineer.

Certain other programs require more effort. For example, Boeing’s prismjlight benchmark makes use of Vector and Hashtable libraries. When running this benchmark under vanilla RTSJ implementations, Boeing was able to blindly use off-the-shelf implementations of these collection libraries because they performed all allocations within the immortal memory region. However, the scope-safe type system guards against undisciplined and accidental allocations within immortal memory, because in general the use of immortal memory represents a potential memory leak that hinders software maintainability, reuse, and scalability. To support the prismjlight benchmark, we implemented simplified versions of these collection libraries and annotated them so that the type system would allow the necessary immortal allocations.

Programs that require scope-allocated collections are not yet supported. Scope-compatible collections are currently being designed and implemented. Certain changes to the traditional collection APIs are required to support the creation of an appropriately sized scope to hold all internal data structures associated with each collection object, and to make scope-compatible copies, when necessary, of the objects that are to be inserted into the collection.

10. GENERALIZATIONS

Space constraints limit the breadth of topics that can be effectively treated in this paper. Here, we provide brief mention of several possible generalizations of the scope-safe type system.

1.     The same techniques that are used to enforce scope safety could also be used to enforce initialization of reference variables. A @NonNull annotation could be introduced for argument, instance, and static variables. A @NonNull instance variable must be initialized with a non-null result in the object’s constructor. A @NonNull static variable must be initialized in the static initialization code for the class. Assignments to @NonNull variables are only allowed from other @NonNull variables. The code generator and safety-certification analysis need not concern itself with checking for null when accessing the values of @NonNull variables.

2.     Reference [3] discusses the need to support producer/consumer relationships in which producer and consumer threads share access to a common scoped memory allocation pool within which memory is reclaimed and recycled at a higher frequency than the rate at which the producer and consumer threads are spawned. The scope-safe type system can be extended to support this capability as follows:

a.       The transient scope to be used for communication between the producer and consumer threads is instantiated in the parent thread’s context before spawning these threads.

b.      The producer and consumer threads establish infrastructure data structures which they use to process the information passed between producer and consumer. The type system must assure that no references to these intermediate data structures are inserted into the transient buffer, because the transient buffer resides in a more inner-nested scope.

c.       Introduce a new type named @Ephemeral to represent reference variables that might point to objects residing within the private scope stacks of the producer and consumer threads.

d.      Mark the methods that account specially for @Ephemeral references as @Scaffolding methods. Enforce that a @Scaffolding method is only called by another @Scaffolding method. Allow the producing and consuming NoHeapRealtimeThread objects to annotate the run() method as @Scaffolding.

e.       Provide attach() and detach() services for the transient scope that serves as the communication channel between producers and consumers. The attach() method provides services comparable to MemoryArea.executeInArea(), except it requires that the run() method carry a special @Transient annotation. Enforce that the attach() service is only invoked from within a @Scaffolding method.

f.       The @Transient annotation on methods and constructors denotes that the method may be running on a scope stack that is nested external to the scope stack of the producer or consumer thread that invokes it. @Transient methods are only allowed to call other @Transient methods.

g.       Within @Transient methods, the contents of @Ephemeral variables may not be arbitrarily copied to @Scoped variables.

3.     Reference [5] describes additional conventions for an annotation and assertion system that supports automatic analysis of the size requirements for each scope. Adding static analysis of scope sizes greatly simplifies software maintenance, integration of independently developed modules, and reliability of real-time software which might otherwise fail because programmers miscalculated scope size requirements.

11. ACKNOWLEDGMENTS

The author expresses appreciation to workshop referees for their careful review and helpful suggestions, especially to Jan Vitek who suggested numerous improvements to the paper. The author also acknowledges the assistance of the PERC Pico development team, Greg Bentley, Art Dyer, and Andrew Klein, whose work has been instrumental in demonstrating the value of this type system for the support of safety-critical and hard real-time Java development.

12. REFERENCES

[1]   G. Bollella, B. Brosgol, J. Gosling, P. Dibble, S. Furr, M. Turnbull, “The Real-Time Specification for Java”, Addison Wesley Longman, 195 pages, Jan. 15, 2000.

[2]   M. Hicks, G. Morrisett, D. Grossman, T. Jim, “Experience With Safe Manual Memory-Management in Cyclone”, Proceedings of the 4th International Symposium on Memory Management, pp. 73-84, 2004.

[3]   A. Salcianu, C. Boyapati, W. Beebee, Jr., M. Rinard, “A Type System for Safe Region-Based Memory Management in Real-Time Java”, Proceedings of the ACM Conference on Programming Language Design and Implementation, San Diego, June 2003.

[4]   C. Andreae, Y. Coady, C. Gibbs, J. Noble, J. Vitek, T. Zhao, “Scoped Types and Aspects for Real-Time Java”, ECOOP, pp. 124-147, Springer-Verlag, 2006.

[5]   K. Nilsen. “Guidelines for Scalable Java Development of Real-Time Systems”, March 2006, available at http://research.aonix.com/jsc.

Kelvin can be reached at kelvin@aonix.com.

© ACM, 2006. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in JTRES 2006, October 11-13, 2006