From Single-threaded to Multithreaded

Event details
Date | 07.01.2010 |
Hour | 16:15 |
Speaker | Jean-Loup Carré |
Location |
BC 355
|
Category | Conferences - Seminars |
A great variety of static analyses that compute safety properties of single- thread programs have now been developed. I will present a systematic method to extend a class of such static analyses, so that they handle programs with multiple POSIX-style threads. Starting from a pragmatic operational semantics, the final algorithm is then derived by abstract interpretation. It analyses each thread in turn, propagating interferences between threads, in addition to other semantic information. The combinatorial explosion, ensued from the explicit consideration of all interleavings, is thus avoided. The worst case complexity is only increased by a factor n compared to the single-thread case, where n is the number of instructions in the program. This method is implemented in Penjili, an EADS tool, demonstrating the practicality of the approach.
Practical information
- General public
- Free
Contact
- Viktor Kuncak