Software Model Checking in the Multicore Era

contact: ahmed rezine

ceniit project 12.04

Bachelor and master's project proposals

Incremental Inductive Verification, Does It Work? Does It Scale?

(Master's level, relevant for Prover Technology) Modern Multicore Computers are able to deliver a greater computing power for programs that can be run in parallel. This generated a great amount of work in coming up with ways to run programs in parallel. This project explores using Multicores to perform verification tasks. As opposed to testing and simulation, verification aims at exploring all possible scenarios before validating a program or a design. Verification typically targets safety critical systems (transportation, medical instruments, etc). The price of the supplied guaranty is a complexity that often limits verification efforts to only target (relatively) small and simple computer systems. An important amount of work aims at coming up with clever verification techniques and algorithms that allow to handle larger and more complex systems. Among the newly developed algorithms for the verification of computer systems, some are particularly well suited for performing parallel verification. This project will experiment possibilities of running them on a multicore platform.

Qualifications

This 30 hp thesis can be carried by one or two Masters students that:

Verification of Synchronization patterns of GPU programs

(Master's level) More and more programs involve pieces of code targeting GPU platforms. This is particularity true for programs that allow for highly parallel computations. The problem is that the sought after gain is only achieved with low level tuning at threads level. This entails a degree of intricacy that make writing such programs extremely error prone and difficult to get right. Testing and simulation based debugging are typically difficult in this context due to the concurrent and intricate nature of these programs. Promissing verification techniques already exist. This project is part of an effort that aims at verifying the absence of certain synchronization errors. For this, GPU programs need to be parsed and relevant synchronization parts need to be isolated. This project aims at isolating the synchronization patterns in typical GPU programs.

Qualifications

This 30 hp thesis can be carried by one or two Masters students that:

Systematically checking concurrent code

(Master's level) 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. The student(s) will start by gaining familiarity with a number of tools (with available source code) for the systematic testing of concurrent programs. An important part of the work will then be to collect a set of benchmarks of concurrent code, either from existing work, from open source applications, or from Ericsson applications. It is expected that an important part of the code will be in a language different from the one handled by the targeted tools. The benchmarks might therefore have to be rewritten to C# and Java. The thesis will leverage on the availability of the source code in order to modify the tools and to experiment with different heuristics, combining with user supplied hints or with other verification or static analysis techniques.

Requirements

This 30 hp thesis can be carried by one or two Masters students that: