SAAPP: Activity

In cooperation with Virtutech, a prototype tool for detection of shared memory communication, synthesis of formal specifications, and analysis of data races is developed. Initially, the main focus will be on data race detection, but the prototype will be designed with the other objectives in mind.

A vital part of the tool is to efficiently monitor and report shared memory communication. Compared to other dynamic methods, using the simulator to monitor the execution instead of using binary rewriting, no probe effects or "Heisenbugs" can emerge. The purpose of the prototype is to implement an absolutely non-intrusive trace mechanism for shared memory communication. As far as we know, this has never been done in software before, whereas more esoteric hardware solutions may exist.

First, a naive data race detector is constructed on top of the memory monitor. During this stage, small toy-example programs, e.g., locking algorithms, is used as input programs to the prototype. Based on the results, necessary modifications will be made to the monitor. When the monitor functionality and performance are satisfactory, other dynamic data race detection algorithms similar to the one used in VeriSoft [GHJ98] and RecPlay tool [ROB00] will be experimented with.

To fully understand the differences between intrusive, low-intrusive and non-intrusive monitoring, the prototype will be compared to existing approaches or tools. We will look at accuracy, time and memory consumption and other performance issues. After evaluation, we can target the simulator based data race detection to a more specific task of the overall race detection problem.

With a more precise target domain, we might be able to build more specific support into the tool. If required, modifications or new features to the Virtutech Simics simulator may be necessary. Depending on the attained accuracy and overall performance of the prototype for the target domain, further development of the data race detection may be needed, or the tool can be extended to detect other classes of races (see future work). Other possibilities are to add features such as deadlock/livelock detection.

Improvements to the described dynamic simulator aided data race detection technique, such as combining dynamic and static methods (the result from the static analysis guides the dynamic analysis) or mixing simulation with binary rewriting (the results of the intrusive analysis guides the non-intrusive analysis) may also be considered (see future work).

For 2003, the activities of the project will be to

• develop a prototype tool for detection of shared memory communication, synthesis of formal specifications, and analysis of data races, by analysing memory accessed by different processors in a multi-processor system,
• use the prototype tool on applications such as locking algorithms and parallel shared memory benchmarks,
• evaluate the approach and find the specific points where it is a significant improvement over earlier work.

Virtutech will give technical support, and develop functionality in the Simics simulator as specified under Budget below.

There are a number of interesting avenues to pursue as future work, given here in no particular order.

• Combination of methods: As mentioned above, it is possible that we for efficiency need to combine the simulator approach with other approaches, such as code instrumentation or static analysis.
• Other communication primitives: In addition to shared memory communication, Simics offers the possibility to detect and analyse also other types of communication between processes, e.g., through pipes, sockets, network and file system.
• Operating system data: By parsing operating system data structures, we can analyse not only communication between processes (cf threads) through shared memory, but perhaps we can also interpret scheduling queues to "see into the future" and predict scheduling behaviour. Such functionality would be very difficult to achieve using instrumentation, because of the probe effects. (This type of work would be operating-system dependent, but should be possible for a range of systems where sufficient information about data structures is available.)
• Model synthesis: To analyse race conditions, we only need to construct a the "happens-before" partial order. An interesting task would be to construct a formal model describing the also communication between processes, thus creating a specification of the system, which could be further analysed.