DTrace is a popular dynamic tracing facility implemented in modern operating systems such as Solaris, FreeBSD, Linux and Apple’s MacOS. 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, programs. We implemented it in Java and provided tools using Aspect-Oriented Programming techniques to instrument existing Java 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:
- learn how to extract threading-related data from DTrace (that is, write DTrace scripts and test programs, for example in C using pthreads)
- how to pass this data in an efficient way to another program for post-processing
- understand and optimize the existing algorithm and data-structures for the task at hand
Requirements:
- basic programming skills in almost any language (functional programmers are welcome!)
- basic knowledge about finite automata (no previous knowledge on temporal logics required!)
- interest to work with bleeding-edge technology :)
Bibliography:
- Dynamic Instrumentation of Production Systems, Bryan M. Cantrill, Michael W. Shapiro, and Adam H. Leventhal, Sun Microsystems, Proc. of USENIX’04
- J-LO, the Java Logical Observer, Eric Bodden, Volker Stolz
Utfyllende informasjon
DTrace and Runtime Verification