Kyriakos Georgiou, a current MSc student, is presenting the results of his MSc project at "The Multicore Challenge" conference to be held in Bristol on 14 September 2010. The project evaluates a new coverage metric for the verification of message-passing multi-threaded code. The research is supervised by Dr Kerstin Eder in collaboration with Dr Mike Bartley (TVS). The project is based on the theoretical foundations established in a previous collaboration that supported the MSc project of Xiaorong Yu.
Kyriakos' MSc project is entitled: "Practical Validation of a Proposal for a New Coverage Model for the Verification of Multi-Threaded Code". Concurrency related bugs are reportedly the most difficult to catch during verification of multi-threaded code. It is therefore important to ensure that the tests run during verification fully exercise the scenarios where threads interact. Traditional code coverage models such as statement, branch and expression coverage are inherently week for this purpose. This talk presents a new coverage model designed to capture the communication between threads in programs that utilize the message-passing paradigm. The coverage model is built up over several layers increasing in Complexity as more detail is introduced. Static code analysis is used to extract the coverage model from a given multi-threaded program prior to tests being run. A prototype tool has been implemented for XC, the concurrent and real-time programming language designed for the XMOS XCore processor. The coverage model was evaluated by running the prototype tool on point-to- point message-passing XC programs containing concurrency bugs. This evaluation provides evidence that the theoretical coverage model proposed is valid and adds value to the verification process in practice. While the evaluation is performed on the XC language, this does not restrict the general applicability of the proposed new coverage model. Hence, this evaluation provides results that are generally applicable to programming languages based on the message-passing paradigm.