This work was done at the Chair of Computer Science 2, at RWTH Aachen University.

J-LO, the Java Logical Observer
A tool for runtime-checking temporal assertions

• Introduction
• Requirements
• System overview
• Specifying temporal assertions
• Running J-LO (with examples)
• FAQ
• Related publications
• License
• Download
• Changelog
• Documentation
• Mailing lists

News

June 5th, 2006

March 3rd, 2005

November 5th, 2005

November 2nd, 2005

October 28th, 2005

tracecheck(Singleton s1, Singleton s2) {

  sym create(Singleton s) after returning (s):
    call(static Singleton Singleton+.inst());
  sym createAnother(Singleton s, t) after returning (s):
    call(static Singleton Singleton+.inst()) && if(s!=t);

  G(create(s1) -> XG !createAnother(s2,s1) ) {
   throw new SpecViolationException
     ("two singletons detected:"+s1+","+s2);
  }
}

Introduction

J-LO, the Java Logical Observer, is a tool for runtime-checking temporal assertions in Java 5 applications. Temporal properties (see below) can be specified using a linear time logic (LTL) over AspectJ pointcuts. Specification takes place right in the source code in the form of Java 5 annotations. After compiling this source code with a Java 5 compliant compiler, Java extracts those annotations from the bytecode and, at the same time, instruments the application with the appropriate runtime checks.

The work is based on a Haskell-prototype developed at our department.

J-Lo is being delevoped by Eric Bodden and Volker Stolz.

Requirements

• A Java 5 compliant compiler.
• A Java 5 runtime environment to run J-LO and later on the instrumented application.*

* J-LO comes with a small runtime library that contains classes necessary for the runtime verification process. This class library is compiled to Java 5 bytecode at the current time. Thus you will need a Java 5 environment to run your instrumented application in.

If you require a Java 1.4 compatible version, please let us know as we can provide one based on the retroweaver and backport 175 (thanks to Toby Reyelts, Jonas Boner and Alexandre Vasseur for providing those).

System overview

At design time...

... software architects usually define temporal interdependencies (TID) between events in the lifecycle of an application. Such TIDs may also be a result of the way certain objects have to interact, a result of the contract, classes adhere to by implementing a certain interface for instance. One such requirement could for instance be that each object of a type T should have its tearDown method called before it is garbage collected and no method is called afterwards on this object. The software architect should formulate those requirements in a formal way, best in LTL.

At implementation time...

... the programmers annotate their source code with LTL formulae stating the requirements as defined in the above process. They use J-LO as an additional tool in their build chain to instument the application under test.

At testing time...

... the instrumented application will emit an error message whenever one of the temporal assertions is falsified or verified. Formulae that could not be falsified or verified by the time the virtual machine shuts down will be reported for manual inspection.

At deployment time...

... J-LO is simply removed from the build chain. This means that no instrumentation will take place. The original bytecode is not touched, No performance overhead is generated.

Specifying temporal assertions: Linear temporal logic over pointcuts

In the following we require that the reader is familiar with the terminology of pointcuts and join points. A definition can be found in the AOSD Wiki. Also we require basic knowledge of LTL. You might find the Specification Patterns project helpful.

Our formalism consists of two key components:

AspectJ pointcuts

Those are the proposition of our logic. At each join point, all those pointcuts are valid which match this join point.

Linear temporal logic - LTL

LTL operators are used to arrange pointcuts on the timeline in order to specify the intended behavior at runtime.

We provide the following LTL operators:

We allow X only to occur in front of another temporal operator. This is a deliberate restriction because we believe that users should not be able to reason about the next join point in a system because those semantics can easily break for a number of reasons.

At the moment, also we require full bracketing for all operators. This is going to change in future revisions.

The entry and exit of any valid AspectJ 1.2 pointcut is a valid propositions for our logic, so for example:

entry( call( public static void *.main(String[]) ) )

This captures the event of entering the call join point for an arbitrary main method.

Exits of join point can also expose the returned object or thrown exception (if any). Thus the complete syntax for propositions is:

The identifier can either be the (fully qualified) name of a type or the name of a free variable declared in the formula.

Free variables

Formulae can contain free variables in the same way as AspectJ pointcuts do. Unlike AspectJ though, variables in if-pointcuts can refer to variables bound earlier in the execution history. Those variables have to be declared at the beginning of each formula for type safety.

Example

As an example we want to use the statement from above:

Each object of a type T should have its tearDown method called before it is garbage collected and no method is called afterwards on this object.

Here we somehow have to quantify over all objects of type T. Thinking in temporal terms, all objects of this type have certainly in common that they have been created some time. Thus we reformulate:

For each object of a type T, after a constructor has been called, its tearDown method is called before it is garbage collected and no method is called afterwards on this object.

This leads us to the following formula:

T t1, T t2:
G(
        (
                exit( call( T.new(..) ) ) returning t1
        ) -> (
                F(
                        (
                                entry( call( * T.tearDown() ) && target(t2) && if( t1==t2 ) )
                        ) && (
                                G(
                                        !(
                                                entry( call( * T.*() ) && target(t2) && if( t1==t2 ) )
                                         )
                                 )
                        )
                )
        ) 
)

Here, parts of the LTL syntax are colored in blue, parts of AspectJ in purple and black.

Important are the free variables t1 and t2. The former is bound by the first join point in the formula that matches (here naturally any join point picked up by the pointcut call( T.new(..) )). For subsequent join points, this t1 is bound, which means that it can be reffered to, as it is done in the two if pointcuts.

Such if pointcuts can refer to bound variables as well as static members of any class.

Annotating the code

Annotating the Java code is the easiest part: Just paste the formula in String form in an appropriate annotation.

If the annotation is put at a reasonable position, two special keywords thisType and thisMember may be used. The former is substituted by the name of the surrounding type/class, the latter is substituted by the complete signature for the member the annotation is put on.

Hence, the above example could look as follows:

import rwth.i2.ltlrv.LTL;
public class T {

@LTL("
T t1, T t2:
G(
        (
                exit( call( thisType.new(..) ) ) returning t1
        ) -> (
                F(
                        (
                                entry( call( thisMember ) && target(t2) && if( t1==t2 ) )
                        ) && (
                                G(
                                        !(
                                                entry( call( * thisType.*() ) && target(t2) && if( t1==t2 ) )
                                         )
                                 )
                        )
                )
        ) 
)
")
public void tearDown() {
	//code for tearDown
}

//code for other members

}

What are annotations?

Temporal assertions are a simple String using the following annotation type:

@Retention(CLASS)
@Target({CONSTRUCTOR, FIELD, METHOD, TYPE})
public @interface LTL {

String value();

}

The annotation type itself is annotated with tags stating that this annotation is to be retained in the bytecode, so that J-Lo can process it, (however not at runtime of the application) and that the annotation can be used at constructor, field, method, and type declarations.

Running J-LO

J-LO is a commandline based tool, an extension of the popular abc compiler for AspectJ.

You can run J-LO directly from the JAR file:

java -jar jlo.jar -help

This will give you a verbose list of all available options, some of them specific to the underlying abc. All options necessary to operate J-LO are isted here:

So a typical usage could look as the following:

java -jar jlo.jar -cp mylib.jar;myotherlib.jar -ltlpath spec -inpath bin -outjar instrumented.jar

This would instrument all classes in "bin", extracting formulae from class files in "spec", loading libraries from "mylib.jar" and "myotherlib.jar" and producing the output in "instrumented.jar".

Examples

This is a collection of examples for download that we have used in practice together with a short program demonstrating the behaviour. All those examples are contained in the thesis examples packages (see below) along with build scripts to process them.

IteratorTest.java

Safe Iterator-pattern: For each Iterator i obtained from a Collection c, there must never be an invocation of i.next() after the collection has been modified. [Java API docs]

HashSetTest.java

HashSet use case: For each HashSet s that contains a Collection c, there must be no invocation of s.contains(c) if the collection has been modified, unless the collection has been removed from the set in between. This example also demonstrates that aliasing is no problem for the analysis.

FailSafeEnumJLO.java

Variant of the Safe Iterator-pattern causing a fault in JHotDraw. Since instrumentation is a bit more involved here, we provide an already instrumented JAR-file. Start it with:

java -cp ../jlo-rt.jar:jhotdraw-debug.jar CH.ifa.draw.samples.javadraw.JavaDrawApp

.

Create a new figure, draw two figures, group them and then start the animation. While the application is running, select the grouped objects and ungroup them. On the console, you should see a message from J-LO stating the violation of the formula. (The unmodified JAR is also required since it contains some images that somehow don't survive the weaving process.)

Custom listeners

J-LO comes with a default console-listener, which reports verification results to the console. It is possible to plug in custom listeners by setting the LTLRV_LISTENERS environment variable to a semicolon-separated list classes implementing the interface rwth.i2.ltlrv.management.VerificationRuntime.Listener.
Example: java -DLTLRV_LISTENERS=listeners.L1;listeners.L2 -jar jlo.jar ...

FAQ

Here are some frequently asked questions:

1. Does the instrumentation performed by J-LO have any performance implications on the application under test?
   Since the instrumentation is triggering the evaluation of a temporal formula / an automaton, there is naturally some overhead involved. Theoretically, the overhead produced at each join point in question is linear to the average size of a formula times the number of formulae containing pointcuts which may match this join point. So the performance overhead heavily depends on what join points one instruments. In our tests it turned out that when instrumenting e.g. the execution of a somewhat larger method, the overhead was consideribly low. The bigger however the relatively constant overhead of evaluation becomes with respect to the execution time of the join point shadow, the larger the performance overhead will be. We hope to improve performance in the future by performing some static analysis.
   In general, we also do not recommend ungarded if-expressions such as entry( if(SomeClass.someMethod()) ) because those would be evaluated at every single join point. Also we do not recommend the use of expensive methods in if pointcuts.
2. What about objects that are being garbage collected? How behave formulae binding such objects in such a case? Does the binding in a formula prevent an object from being garbage collected?
   J-LO provides a well-defined behavior for such cases. In particular, J-LO will not prevent an object from being garbage collected! A strong reference will be hold during a single step of evaluation for the sake of consistency. However, between evaluation steps, only weak references remain, which do not prevent the garbage collector from collecting bound objects. When an object o bound to a particular proposition p(o) is being collected, p(o) is implemented to never match again. It becomes essentially equivalent to FF, which is consistent with the semantics because no joinpoint will occur any more where o is bound to the object in question.
3. What happens when I mess up with if-pointcuts?
   The case where evaluation of an if-pointcut causes an exception to be thrown is well captured within J-LO: The exception is being passed to Listener.notifyOnUserCauseException(...) and the formula is being removed from further verification.
4. Why are you working on bytecode?
   Bytecode simply gives more flexibility on the deployment side: The specification can be done by a third party, encoding specs, for instance for interfaces, right in the bytecode. Implementors of such interfaces can then use J-LO to instantly check their implementation for compliance with this specification.
5. Your question here

Related publications

• Tracechecks: Defining semantinc interfaces with temporal logic, E.Bodden, V.Stolz. Fifth Intl. Symp. on Software Composition (SC 2006), to appear in LNCS.
• Temporal Assertions using AspectJ, V.Stolz, E.Bodden. RV'05 - Fifth Workshop on Runtime Verification, Satellite workshop of CAV 2005, Edinburgh, Scotland, UK, July 2005
• Runtime Verification of Concurrent Haskell Programs. V.Stolz, F.Huch. RV'04 - Fourth Workshop on Runtime Verification, ENTCS Vol.113, Elsevier Science Publishers, 2004
• A Lightweight LTL Runtime Verification Tool for Java. Eric Bodden. In OOPSLA'04 ACM Conference on Object-Oriented Systems, Languages and Applications (Companion), SIGPLAN, Vancouver, Canada, October 2004.
  This paper was finalist of the OOPSLA Student Research Competition. It gives a first vague introduction about the topic and the proposed solution.
• Concern specific languages and their implementation with abc. Eric Bodden. In Workshop on Software-engineering Properties of Languages and Aspect Technologies (SPLAT) 2005, Chicago, USA, March 2005.
  This paper introduces the notion of Concern specific languages (CSLs) as a subclass of Domain specific languages and identifies the LTL used in J-LO as one special case of such a CSL.
• Implementing concern-specific languages with abc. Eric Bodden. In Seminar on Aspect-oriented technologies. Institut für Informationssysteme, Prof. Steimann, Fachgebiet Wissensbasierte Systeme, Hannover University. February 2005.
  This paper explains in detail how abc was extended in order to achive the implementation of J-LO. It gives useful hints to abc extenders.
• Efficient and Expressive Runtime Verification for Java. Eric Bodden. In Proceedings of the Grand finals of the ACM Student Research Competition 2005, San Francisco, CA, USA, March 2005.
  This paper is winner of the Grand Finals of the 2005 ACM Student Research Competition. It is an extension of the OOPSLA'04 paper including new intermediate results, first implementation details and a proposal for implementing bindings.
• J-LO - A tool for runtime-checking temporal assertions. Eric Bodden. Diploma thesis.
  This thesis holds all information about the implementation semantics of J-LO.

License

Download

J-LO compile time tool

J-LO runtime library

This jar file contains the J-LO runtime library. This code has to be linked with your instrumented application (included in the CLASSPATH) in order to get the verification working.
Download here J-LO runtime library, version 0.9.2.

J-LO source code

Changelog

You can find the log of previous changes here.

Documentation

The following API-Docs are available:

• J-LO (RWTH Informatik internal)
• J-LO runtime library

Shortcomings of this prototype

• As mentioned above, all LTL expressions need to be fully bracketed. This will be fixed with a new version of our grammar.
• Provided error messages for syntactical errors are still quite poor. This is actually a problem of the underlying abc compiler.

Mailing Lists

Acknowledgements

Acknowledgements go to a lot of people including the whole abc development team, especially Oege de Moor who helped quite a lot with debugging our implementation. Also we are grateful to all the people who attended the "perobjects BOF" at the AOSD conference, which ended in a very fruitful discussion about the implicit instantiation and bookkeeping of aspects. We wish to thank the many reviewers involved with the above papers as well as all the people who commented on J-LO during the various presentations. Much gratitude goes to Adrian Colyer for picking up the idea of aspects as automaton. We thank the team of the TU Darmstadt for providing BAT2XML, which we use for annotation extraction.