Description

Recently, within the FMT group there have been two Master projects studying run-time checking of concurrent programs.

Jorne Kandziora developed a technique to do interference-free checking of assertions in concurrent programs, by evaluating assertions in snapshots, see http://fmt.ewi.utwente.nl/education/master/178/.

Stijn Gijsen developed a technique to check permissions, which help you to ensure that a program is free of data races, see http://fmt.ewi.utwente.nl/education/master/287/.

Both approaches can be used to test certain aspects of concurrent programs. However, for practical test of concurrent programs, it is also necessary that you can control the scheduler, such that you are able to run the test over different interleavings of the threads. CalFuzzer, see http://srl.cs.berkeley.edu/~ksen/calfuzzer/ supports active testing, where results of an earlier analysis can be used to influence the scheduler.

The goal of this Bachelorproject is to investigate if and how CalFuzzer can be combined with the run-time checking approaches described above. The following steps are foreseen:

• understand the different run-time checking techniques and the working of CalFuzzer
• describe a design to combine CalFuzzer with one of the run-time checking techniques
• provide a basic implementation of your design
• demonstrate usability of your approach on several examples, i.e., show that it can be used errors that are caused by different interleavings of a concurrent program.

Additional Resources

1. The paper