×

Static data race analysis of heap-manipulating C programs. (English) Zbl 1360.68004

Dissertationes Mathematicae Universitatis Tartuensis 64. Tartu: University of Tartu Press; Tartu: Univ. Tartu, Faculty of Mathematics and Computer Science (Diss.) (ISBN 978-9949-19-508-4/pbk; 978-9949-19-509-1/ebook). 137 p. (2010).
Summary: Modern computer architectures are capable of carrying out many computations at the same time. Writing and testing programs for such systems is notoriously difficult because the interaction between concurrently executing threads is unpredictable. A particularly elusive flaw in shared-memory concurrent systems is the data race, a situation where multiple threads may simultaneously attempt to update the same memory location. This may result in data corruption and ultimately system malfunction. Static program analysis is an automated formal method, which computes all possible run-time behaviours of a program by solving a system of data flow equations. This dissertation contends that static analysis can be used to verify the absence of data races in real-world systems, especially operating system modules like Linux device drivers. The challenge in developing static analyses for such code is that both data structures and locks protecting the data are created at run-time. To face this problem, three novel techniques were developed: an abstract domain for equalities between address expressions, a region-based heap abstraction, and a shape domain suitable for low-level programs. We have implemented these techniques in the Goblint analyzer and used it to experimentally validate the contention that verification of race-freedom in real-world systems is possible by means of static analysis.

MSC:

68-02 Research exposition (monographs, survey articles) pertaining to computer science
68M07 Mathematical problems of computer architecture
68N15 Theory of programming languages
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N20 Theory of compilers and interpreters
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68P05 Data structures
PDFBibTeX XMLCite
Full Text: Link Link