Hartung-Gorre Verlag Inh.: Dr. Renate Gorre D-78465 Konstanz Fon: +49 (0)7533 97227 Fax: +49 (0)7533 97228 www.hartung-gorre.de

S

Series in Computer Science
Edited by Thomas M. Stricker

Vol. 5

Cyrille Artho,
Combining Static and Dynamic Analysis to Find
Multi-threading Faults Beyond Data Races.
2005; XX, 200 pages/Seiten, € 64,00. ISBN 3-89649-997-1

Multi-threaded programming gives rise to errors that do not occur in sequential programs. Such errors are hard to find using traditional testing. In this context, verification of the locking and data access discipline of a program is much more promising, as it finds many kinds of errors quickly, without requiring a user-defined specification.

Run-time verification utilizes such rules in order to detect possible failures, which do not have to actually occur in a given program execution. A common such failure is a data race, which results from inadequate synchronization between threads during access to shared data. Data races do not always result in a visible failure and are thus hard to detect. Traditional data races denote direct accesses to shared data. In addition to this, a new kind of high-level data race is introduced, where accesses to sets of data are not protected consistently. Such inconsistencies can lead to further failures that cannot be detected by other algorithms. Finally, data races leave other errors untouched which concern atomicity. Atomicity relates to sequences of actions that have to be executed atomically, with no other thread changing the global program state such that the outcome differs from serial execution. A data-flow-based approach is presented here, which detects stale values, where local copies of data are outdated.

The latter property can be analyzed efficiently using static analysis. In order to allow for comparison between static and dynamic analysis, a new kind of generic analysis has been implemented in the JNuke framework presented here. This generic analysis can utilize the same algorithm in both a static and dynamic setting. By abstracting differences between the two scenarios into a corresponding environment, common structures such as analysis logics and context can be used twofold. The architecture and other implementation aspects of JNuke are also described in this work.

Keywords: Software verification, Static Analysis, Dynamic Analysis, Run-time Verification, Model Checking, Data Races, Atomicity

Series in Computer Science

Buchbestellungen in Ihrer Buchhandlung, bei www.amazon.de

oder direkt:

Hartung-Gorre Verlag / D-78465 Konstanz

Telefon: +49 (0) 7533 97227 Telefax: +49 (0) 7533 97228

http://www.hartung-gorre.de eMail: verlag@hartung-gorre.de