Runtime Verification and Monitoring

["Eric Bodden" <eric.bodden AT mail.mcgill.ca>]

Hi all.

I am happy to announce that the latest version 1.3.0 of the abc
compiler [1] supports three new pointcuts that assist the development
of runtime verification algorithms with a focus on multi-threaded
programs:

* lock() matches whenever one enters a synchronized block or synchronized 
method

   * one can use lock() && args(l) to expose the lock l to the advice

* unlock() matches whenever one exits a synchronized block or
synchronized method

   * one can use unlock() && args(l) to expose the lock l to the advice

* maybeShared() matches any field access (set or get), but only those
that may be accessing shared fields

   * e.g. set(int *) && maybeShared() matches all potentially shared
writing accesses to int fields

An example of what you can do with these pointcuts is RacerAJ [2], an
AspectJ based version of the Racer race detection algorithm [3] (a
variant of Eraser) that uses this language extension.

The first two pointcuts, lock() and unlock(), are also supported by
current versions of ajc, but maybeShared() requires a static
whole-program analysis only present in abc.

So next time you want to implement your own race detection or deadlock
detection algorithm for Java, consider making use of those tools. They
were specifically designed to make your life easier.

Cheers,
Eric

[1] abc http://abc.comlab.ox.ac.uk/introduction
[2] RacerAJ http://www.bodden.de/tools/raceraj/
[3] Racer http://www.bodden.de/2008/05/07/racer/ (joint work with
Klaus Havelund, to appear at ISSTA 08)

--
Eric Bodden
Sable Research Group
McGill University, Montréal, Canada