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!