Project: DTrace and Runtime Verification

DTrace is a popular dynamic tracing facility implemented in the Solaris and FreeBSD operating systems, with support coming up in Apple’s next release of MacOS called “Leopard”. It allows to instrument the running system to obtain valuable data for debugging and performance measurement, right down into the kernel.


In previous work, we presented an algorithm for verifying Linear Time Logic (LTL) temporal formulae with value bindings on program traces with a special application to the behaviour of concurrent, that is threaded, programs. We implemented it in Java and provided tools using Aspect-Oriented Programming techniques to instrument existing Java (byte code) programs.


The goal of the project is to extract DTrace data and feed it either online or offline into the verification algorithm. Either adaptations to the existing Java program could be made, or a simple reimplementation of the algorithm in another language.


A prospective student should

  1. •learn how to extract threading-related data from DTrace (that is, write DTrace scripts and test programs, for example in C using pthreads)

  2. •how to pass this data in an efficient way to another program for post-processing

  3. •understand and optimize the existing algorithm and data-structures for the task at hand


Requirements:

  1. •basic programming skills in almost any language (functional programmers are welcome!)

  2. •basic knowledge about finite automata (no previous knowledge on temporal logics required!)

  3. •interest to work with bleeding-edge technology :)


Bibliography:

  1. •Dynamic Instrumentation of Production Systems, Bryan M. Cantrill, Michael W. Shapiro, and Adam H. Leventhal, Sun Microsystems, Proc. of USENIX’04

  2. •J-LO, the Java Logical Observer, Eric Bodden, Volker Stolz

  3. •Temporal Assertions using AspectJ (PDF), Volker Stolz, Eric Bodden. RV'05 - Fifth Workshop on Runtime Verification, Satellite workshop of CAV 2005, Edinburgh, Scotland, UK, July 2005

  4. •Runtime Verification of Concurrent Haskell Programs. Volker Stolz, Frank Huch. RV'04 -Fourth Workshop on Runtime Verification, ENTCS Vol.113, Elsevier Science Publishers, 2004


Contact: Volker Stolz