High Assurance Hard Real-Time Java needs static property enforcement - Embedded.com

High Assurance Hard Real-Time Java needs static property enforcement

Developers often describe Java as a dynamic programminglanguage and many programmer productivity gains result from certaindynamic aspectsof the Java platform.Examples of dynamic language features include dynamicclass loading and JIT compilation to accelerate the develop-test-debugcycle,and automatic garbage collection to simplify the task of managingdynamicmemory allocation.These dynamicfeatures, which are very empowering to Java developers, often stand outindevelopers' minds as the key reasons why Java allows them to beapproximatelytwice as productive as C++ developers.

It turns out, however, that Java's dynamic featuresrepresent only part of the reason that Java developers are moreproductive thanC++ developers.In comparison with C++,the Java compilers and linkers also perform more static propertyanalysis toenforce stronger consistency checking within software systems.This stronger consistency checking reducesprogramming errors, which further improves developer productivity.Examples of built-in static propertyenforcement in Java include:

1. Strong type checking prohibits incompatibletypecoercion between, for example, an integer and a reference type, orbetween twoincompatible reference types.

2. Programmers are prohibited from addinginteger valuesto reference values to create references to new objects.

3. Byte-code verification assures that thetypes ofactual parameters passed to a method invocation exactly match the typesof theformal parameters declared for the invoked method.

4. Contexts that invoke methods that might throw “checkedexceptions” are required by the compiler and byte-code verifier to dealexplicitly with the possibility that an exception might be thrown.This consistency checking is especially helpful whenlarge software systems are assembled from components that wereindependentlyproduced by different teams of developers.

It turns out that Java productivitybenefits are even greater during the integration and maintenance phasesof thesoftware life cycle than during the development of new functionality.Whencompared with C++, Java developers typically see a 5 to 10 foldreduction inthe effort, calendar time, and costs incurred during softwaremaintenance.

Because of the strong static property checking alreadyenforced by the Java programming environment, Java has attracted theattentionof safety-critical developers as a possible language of choice forimplementation of future safety-critical systems.Safety-criticalsoftware includes anti-lockbraking systems in consumer vehicles, fly-by-wire control of flightsurfaces incommercial aircraft, automatic shutdown of nuclear power plants, andcomputer-controlled switching systems in passenger railroad stations.

Various different protocols exist for certifying thatsoftware written for these sorts of applications is reliable andcorrect,depending on the regulating government agency which is responsible fortheparticular industry.All of thecertification techniques share a common goal: to prove through analysisofstatic properties of the software that it will always run correctly.

A draft specification for safety-critical Javahas beenproposed to the Embedded and Real-Time Systems Forum of the Open Group.The intention of this effort is toproduce a standard that is endorsed both bythe Java Community Process and by ISO.The draft standard is based on the traditional Java platform asextendedby the official Real-Time Specification for Java (RTSJ).

From this basis, dynamic features such asdynamic class loading, automatic garbage collection, and explicit useofScopedMemory regions are all removed.Then, certain enhancements are added to provide even more staticverification than is available in traditional Java.Programmers who develop their code accordingto the published safety-critical guidelines can rely upon assurancesfrom thesafety-critical Java compiler that:

1. The maximum amount of CPU time required toexecuteparticular methods (and all overriding methods) is bounded by aconstant thatcan be derived as a static property of the program and knowledge of thetargethardware.

2. The maximum amount of stack memory requiredto executeparticular methods (and all overriding methods) is bounded by aconstant thatcan be derived as a static property of the program and knowledge of thetargethardware.

3. Execution of a particular method (or of anyoverridingmethod) will not allocate any memory in the shared immortal heap.(Since the safety-critical Java environmenthas no automatic garbage collector, any objects allocated in the heapareconsidered to be immortal, because their memory will never bereclaimed.)

4. Execution of particular methods will not result inthrowing of RTSJ-defined CeilingViolationException,DuplicateFilterException,IllegalAssignmentError, InaccessibleAreaException, MemoryAccessError,MemoryScopeException, MemoryTypeConflictException, OutOfMemoryError,ScopedCycleException, StackOverflowError, or ThrowBoundaryErrorexceptions.

Figure 1 : SourceCode for AnalyzableBubbleSort Program

Programmer Declaration of Static Properties

Source Code For Analyzable in Figure1 above representssource code for an analyzable bubble-sort program.In this program, Java 5.0 style meta-dataannotations and assertions allow developers to specify staticpropertiesassociated with their programs.The@StaticAnalyzable annotation in line 10 denotes that the worst-caseexecutiontime and the worst-case memory allocation needs for the sort() methodintroduced on line 11 must be analyzable as a static property of theprogram.

Note that the @StaticAnalyzableannotation is accompanied by two attributes, named enforce_analysis andmodes.The modes attribute represents anenumeration class that identifies the various modes of operation forthismethod's execution.Analysis of themethod's static resource requirements always depends on the modespecified inthe context from which the method is invoked.

Figure 2 : Source Code for Analysis Modes Enumeration

Figure 2 above shows the declaration of the AnalysisModesenumeration.In this example, there arefive different modes of operation.Thefirst mode is named UNBOUNDED.Thisrepresents a situation in which the size of the array passed as anargument tothe sort() method is not known as a static property of the caller'scontext.

In this mode of operation, the resource needs cannot beanalyzed.This is indicated by a falsevalue in the first entry of the enforce_analysis array. The other modesofoperation are named SMALL, BIG, SMALL_PRESORTED, and BIG_PRESORTED.In all of these cases, the correspondingvalue in the enforce_analysis array's initializer evaluates to true.

In the SMALL mode of operation, the array argument isassumed to have fewer than 16 elements.In the BIG mode of operation, the array argument is assumed tohavefewer than 64 elements.SMALL_PRESORTEDand BIG_PRESORTED correspond to similarly sized arrays in which all butone ofthe elements in the incoming array are known to be in sorted order.

In analyzing the CPU time required to complete executionof the sort() method, we expect SMALL_PRESORTED to execute in less timethanBIG_PRESORTED, which will execute in less time than SMALL, which willexecutein less time than the BIG mode of operation.

Whenever the sort() method is called from a context thatis itself analyzable, the calling context must define the mode ofoperationunder which it expects the sort() method's resource requirements to beanalyzed.This is accomplished bypreceding the invocation with an assertion that specifies the intendedmode ofoperation for the called method, as shown in Figure 3 below.

 Note that the initialization expression forthe array (line 11) creates an array with six elements, only one ofwhich isout of sequential order.

If the assertion in line 13 of Figure 3 had beenomitted, the sort() method would have been analyzed according to therules ofthe first entry in the AnalysisModes enumeration.Since,in that case, the corresponding entryin the sort() method's enforce_analysis attribute is false, thesafety-criticalJava compiler would reject this program as invalid because the caller'scontextrequires analyzability of all called methods.

Note that the assertions provided in the body of thesort() method (Figure 1 ) aresufficient to limit the number of iterationsconsumed in each of the analysis modes except forUNBOUNDED.The assertion in line 19, for example, denotes that theinner-mostnested loop (the one that begins on line 16) will iterate no more thantwice ifthis method is being executed in analysis mode SMALL_PRESORTED.

The NestedIterationBound assertion in line 26 signifiesthat the body of code that includes this assertion will execute no morethan 29times for each entry into the outer loop at outer-nesting level one(the loopthat begins on line 16) if the sort() method is being analyzedaccording to theSMALL_PRESORTED analysis mode.Similarly, the NestedIterationBound assertion at line 29requires thatthe enclosing body of the if-then statement executes no more than 15times foreach entry into the outer-nested loop if this method is being analyzedaccording to the SMALL_PRESORTED mode of execution.

Enforcement of Static Properties

The astute reader may have already observed that it isnot possible in the most general case for a compiler to enforce thattheprogrammer supplied assertions are all valid.A programmer might, for example, claim that he is passing asmall arrayto the sort() method, when he is really passing an array with more than1,000elements.Or a programmer who assertsthat a particular loop will execute no more than 100 times for a givenconfiguration of input values might have misrepresented ormisunderstood thealgorithmic complexity.

The primary objectives of the static property analysis inthe draft safety-critical Java specification are to enable programmersto makevery clear their intentions regarding the static properties associatedwithparticular components, to enable automatic enforcement of consistencybetweenthe static properties of independently created components, and toeliminatemuch of the tedium associated with analyzing worst-case executiontimes, stackgrowth, and heap memory allocation.

Enforcement of static software properties inthe safety-criticalJava specification takes two specific forms:

1. The compiler, byte-code verifier, and linkerworktogether to assure that all programmer-declared assertions areinternallyconsistent.This means if a particularcomponent is declared to be analyzable, any components that it dependson mustalso be declared to be analyzable and the results of analysis mustsatisfy allprogrammer-declared requirements.

2. If the program is compiled with assertions enabled, anassertion exception will be thrown any time the program behaves in sucha wayas to violate any of the assertions that describe theprogrammer-intendedstatic properties.

In a safety-critical system, a separate proof system isrequired to assure that each component satisfies the static propertiesdescribed in the programmer-supplied annotations.Inparticular, it must be proven that foreach method's available analysis modes, the bounds on loop iterationsare validfor every possible set of input values that is consistent with thatparticularanalysis mode.

Further, it must be shown that whenever an analyzablemethod is invoked from within a context that is itself consideredanalyzable,the invocation is preceded by an appropriateStaticLimit.InvocationMode()assertion which “sets” the invoked method's analysis mode to a valuethatappropriately represents the complexity of executing the invoked methodwiththe input values that are passed as parameters from this context.

These proofs are required in all safety-criticaldevelopment.Some of these proofs can beautomated using automatic theorem proving technologies facilitated, forexample, by formal JML (Java Modeling Language) annotations.In the most general cases, generation ofthese proofs cannot be entirely automated because automatic theoremproving ofarbitrary static program properties is “not computable.” This is why the proposed safety-critical Java languagestandard restricts its automatic static property analysis to the realmofstatic property checking and consistency enforcement that can be easilyandefficiently solved by compilers and other static analysis tools.

Conclusion

Though it may be more difficult to programhigh-performance, hard real-time code in Java than to write traditionalJavacode, certain components of most mission-critical systems must beimplementedusing technologies that are more efficient and more deterministic thantraditional Java.

At the same time, development and maintenance of theselow-level components using portable stylized Java rather thanassembler, C, orC++ will yield significant productivity improvements and cost savings.We haveevery reason to believe that the two-fold developer productivitybenefits andfive- to ten-fold software maintenance benefits that Java hasdemonstrated overC++ in traditional information technology markets can be matched in thedeeplyembedded mission-critical and safety-critical markets as well.

By restricting the use of Java programming languagefeatures and libraries, and by exploiting special static analysistools, it ispossible to apply many of the benefits of the Java programming languageto thevery specialized domain of safety-critical development and hardreal-timemission-critical systems. Standards to support these developmentapproaches arebeing developed under the auspices of the Open Group, which is workingtoestablish standards that are to be blessed both by the Java CommunityProcessand by ISO.

Kelvin Nilsen,Ph.D., is Chief Technical Officer at AonixNorth America.

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.