From Single-threaded to Multithreaded

Thumbnail

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

Event broadcasted in

Share