Contact persons: Ahmed Rezine, Christoph Kessler
Description:
Powerful Multicore computers are now widespread and more and more concurrent code is being produced in order to get the most of these platforms. The problem is that designing, implementing, testing and debugging concurrent programs can be much more challenging and intricate than for sequential ones. Typically, concurrent programs allow for a huge number of possible interleavings between their concurrent sequential parts. Many bugs only appear in a fraction of these possible interleavings. Traditional testing approaches would only explore a tiny portion of these interleavings, leading to embarrassing hidden bugs mysteriously appearing at the customer site.
This situation resulted in an important amount of work that looked for effective ways to hunt such bugs and to validate the concurrent code. The available techniques range from best effort monitoring tools that record certain aspects (memory accesses, race conditions, etc) of the program behavior during runtime to verification tools that aim at proving correctness of the programs. These approaches strike different balances between scalability and resulting guaranty. Monitoring tools handle large and realistic programs (at least larger than those handled by verification approaches) but explore only a tiny fraction of the possible interleavings, namely the one that happens to be executed when executing the program under test. Verification tools typically either generate too many false positives (or false alarms, spurious errors that do not exist in the code), or do not scale. A middle approach, which gained a lot of interest lately, monitors and tests concurrent programs by systematically steering the possibleinterleavings to be executed in order to boost the explored state space and to reproduce the bugs if any are found.
In this thesis project, the student(s) will start by gaining familiarity with a number of recent works for the systematic testing of concurrent programs. The student(s) will then implement a recent and promising verification approach [1] and assess its applicability by evaluating it on a number of "real life" benchmarks.
Requirements
This 30 hp thesis can be carried by one or two Masters students that:
References
[1] Santosh Nagarakatte, Sebastian Burckhardt, Milo M.K. Martin,
and Madanlal Musuvathi: Multicore acceleration of priority-based schedulers
for concurrency bug detection.
Proceedings of the 33rd ACM SIGPLAN conference on Programming Language Design
and Implementation (PLDI'12), June 11-16, 2012, Beijing, China
[doi>10.1145/2254064.2254128]
Back to my master thesis students page