These are some topics I am proposing as COMP 621 projects. Generally I am very interested in people working on tracematches and/or verification. However, feel free to suggest anything else that might interest you. You may also want to look at an old project that one of last year's students successfully completed and which will be published at AOSD 2008. (Eric Bodden)

More efficient trace matching through data sharing


Tracematches provide a means to match on sequences of events in a Java program via a regular pattern over AspectJ pointcuts. This makes them very suitable for runtime verification. Our current implementation is very efficient if a single tracematch is woven into a piece of software. The task of this project is to explore techniques to generate efficient code if multiple tracematches are applied to the same piece of software. In particular, sharing should be attempted. Have a look at the following example, consisting of two tracematches:

tracematch(File f) {

	sym open after returning(f):
		call(File.new(..));
	sym close after returning:
		call(* File.close(..)) && target(f);
	sym shutdown before:
		/* some pointcut that capture shutdown here */

	open shutdown { 
		//file was opened, but never closed (before shutdown)
	}

}
tracematch(File f) {

	sym close after returning:
		call(* File.close(..)) && target(f);
	sym write before:
		call(* File.write(..)) && target(f);

	close write { 
		//tried to write to a closed file
	}

}

Those two tracematches assert two guarantees over a file f: A file should always be closed after having been used. Also, it should not be written to a file aftwer having closed it. Note that those two tracematches both refer to the event close. This would in the current implementation to two joinpoint shadows (pieces of instrumentation) be woven after calls to File.close(). In this project, the student should exploit means of data sharing in the sense that multiple tracematches share the same data structure. This should provide both, less memory consumption and faster runtime.

If done properly, such a project could well lead to a publication at a major conference like AOSD, PLDI or OOPSLA.

This project has also the potential of being a Master's thesis topic, because it could easily be extended in multiple directions.

The project would be supervised by Eric Bodden.


Model checking of residual proof obligations from static analysis for tracematches

Introduction

The abc compiler has a very higly optimized implementation of tracematches. A tracematch matches a regular expression over events on the dynamic execution trace of a program. The following tracematch can for example be used to check a safety requirement of the JDK: When iterating over a synchronized collection c, one must hold a lock on c. (see here for details)

        pointcut createSync(): call(* Collections.synchr*(..)) && !within(dacapo..*);
        tracematch(Object sync) {
            sym sync after returning(sync): createSync();
            sym asyncIteration before: call(* Collection+.iterator()) && target(sync) && if(!Thread.holdsLock(sync));            
            sync asyncIteration {
                   throw new IllegalStateException("Collection "+System.identityHashCode(sync)+
                       " is synchronized. You may only iterate from within a synchronized block.");
            }
        }

During the last two years, we developed a static analysis (and another one) that can in many cases determine statically that such a safety property always holds in a given Java program. In some cases however, this cannot be guaranteed. When this happens, instrumentation is inserted at all the necessary places, i.e. at all the places in the program which could not be proven safe.

Task

The goal of this project is to use a model checking tool like Bandera in order to check the program for complete correctness assuming that the abovementioned static analysis was already performed. This means that not the whole program should be model-checked, i.e. not the whole state space should be explored, but rather should the state spaced be explored based on the information that was gained by the static analysis. This is very similar to slicing, which is already implemented in Bandera.

Like in the static analysis for tracematches, even if the program cannot be proven safe using the model checkig approach (for instance because the program has a bug), the results of the model checking process could be fed back to abc in order to remove the amount of necessary instrumentation for runtime checking further.

Ideally, the student would integrate the approach within the static analysis in abc.

If done properly, such a project could well lead to a publication at a major conference like CAV.

The project would be supervised by Eric Bodden.

Note: We note that this project is very loosely defined. Therefore we are very open to suggestions from the student. Anything along these lines would be very welcome!