Possible Seminar and Master's Thesis Topics on Parallel Model Checking

I am currently looking for Master students interested in parallel algorithms and architectures. The following is a list of possible topics to write a paper in the seminars FSA and SET. They are also very suitable for writing a Master's thesis. In most cases, parallel programming is only optional, although a parallel implementation of an interesting algorithm would definitely strengthen the thesis.

Feel free to contact me if you are interested in one of these, also if you are not attending one of the two seminars mentioned, but are looking for a Master's thesis topic.

1. Formal Models of Parallel Computing

This entails doing a literature study on the existing models for parallel computing, such as PRAM and BSP. Most of these models have good and bad points. For instance, PRAM assumes that there are always as many processors available as required, which is not realistic, and communication overhead is not taken into account. The assignment is to describe the different models, and give suggestions for improvement.

Literature suggestions:

Possible Master's thesis topic: Using the outcome of the literature study, define a formal model for GPGPU CUDA programming. Currently, it is hard to determine how well a GPGPU will perform, given a parallel program. A formal model would be very helpful for this.

2. Parallel sorting algorithms

Sorting algorithms are very basic algorithms relevant for many applications. In model checking, when reducing state spaces, sorting the states can help speedup the reduction. Therefore, parallel versions of sorting algorithms can impact the speed of these model checking operations. This assignment entails doing a literature study on parallel sorting algorithms. Questions to ask are:
  • Which parallel sorting algorithms exist already, and for which platforms (GPGPU, multi-core CPU, network-on-chip, clusters)?
  • Why do they work (or don't they work)? Is the efficiency dependent on the input data or not? (for instance, how does the running time increase if the input list of data elements is increased in length?).

    Literature suggestions:

    Possible Master's thesis topic:

    3. Multi-Core Nested-Depth First Search

    Liveness properties state that "something good eventually happens" in a model. A counter-example to such a property consist of a reachable accepting state (something bad) in an accepting cycle (the bad situation can occur infinitely often). A classic algorithm to find reachable accepting states in the product of the system behaviour and the Buchi automaton of the property is Nested Depth-First Search (NDFS). Recently, we developed a multi-core NDFS algorithm, to run multiple randomized NDFS instances together on a multi-core system, where the instances moreover share information concerning the cycle detection part. The assignment is to perform a literature study on NDFS, with all its extensions proposed over the years. Some of those extensions have not yet made it into the MC-NNDFS algorithm. Consider which extensions could be useful to add, and perhaps you can think of a new extension.

    Literature suggestions: Multi-Core Nested Depth-First Search. References to work on extensions of NDFS can be found in this paper.

    4. Garbage Collection in Multi-Threaded Programs

    Garbage collection is another classical issue in parallel shared memory programs. In Informed Swarm Verification (see next assignment), the HIVE manager maintains a growing search tree using multiple threads. As it grows, however, parts of the tree become redundant, therefore being able to free that memory up again can result in vast reduction of memory use. At some points, a thread can determine that a particular branch should be thrown away, but at that moment, other threads may be traversing it. The threads are not aware of each other's activities. The assignment consists of doing a literature study on available techniques to do garbage collection in multi-threaded programs, with the goal to give a suggestion for the problem given above. A solution ideally requires not too much extra book-keeping (for instance, storing counters in all nodes of the tree, to keep track of the number of threads that run below that node).

    Possible Master's thesis topic: Implement a garbage collection technique in the HIVE source code. This requires programming experience in C. Some experience with pthreads is a plus, but certainly not required.

    Literature suggestions:

    5. Informed Swarm Verification

    Swarm Verification (SV) consists of running many independent search threads, either on a multi-core system or a cluster, where each thread performs a randomized Depth-First Search. Because of this search diversification (due to the randomization), all threads go in different directions if the state space is sufficiently large. This makes it more likely that reachable counter-examples are found faster. However, if these are not present (in other words, the state space describes correct behaviour), the speedup of SV is lost, since all threads will exhaustively explore all reachable states. Informed Swarm Verification (ISV) is an extension to improve on this: if the system consists of a number of components in parallel composition, then each thread is given a particular trace through some selected subsystem (a subset of components), to be bounded by. Each thread exhaustively searches all other behaviour (not stemming from the subsystem) plus the given behaviour of the subsystem. In practice, this is very effective, but it depends on which subsystem is selected. The assigment entails studying why particular components in given system models are suitable for subsystem selection, and why others are not. This requires virtually no programming. The ISV technique has been implemented in an extended version of SPIN, and in iSPIN (the graphical tool of SPIN), it is possible to display the components graphs. A set of benchmark models can be analysed in SPIN, and ISV can be launched on them with different subsystem settings.

    Literature suggestions: Towards Informed Swarm Verification

    Possible Master's thesis topic: Design a automatic subsystem selection method, such that ISV can select a subsystem without user input. It is not required to also implement the method, but it will seriously strengthen the thesis. The ISV implementation in SPIN is programmed in C, hence experience with C is required.

    6. Model Checking with CUDA GPGPUs

    More information on this can be found here.

    7. Model Checking Without a Model

    More information on this will shortly appear.