HW-SW Co-verification of Concurrent Programs

In the ever-developing world of technology, more and more situations arise where the life of many people lay in the hands of computers - be it the processor of a self-driving car or an airplane, or the command center of a nuclear reactor. The most important expectation of critical software is that they should never fail in a way that could have been prevented. As there have already been many accounts of catastrophes that were caused by malfunctioning computers or programs, we need to verify these systems before deployment - which could mean, among others, to prove mathematically that no unintended outcome can ever occur in the foreseeable operational circumstances. On the software side, there have been many successful attempts at creating a verification framework that takes a formal model and verifies whether it conforms to specified criteria. However, there is a lack of approaches targeting system level correctness - even if the software is perfect, a hardware bug can still occur that could render the whole system unsafe. The co-verification of HW-SW systems is even more challenging for multi-core systems. The main goal of this research is the co-verification of multi-core hardware and concurrent software running on top of them. I have developed an approach that not only takes multithreading capabilities into account but does so while checking for memory consistency problems. My research is based on a previous research where authors showed that there are many situations violating the Memory Consistency Model (MCM) of programming languages running on modern architectures. In the scope of this project, I propose an approach that can help programmers developing software for such mission-critical systems leverage the tools of formal verification and MCM validation resulting in safer, more reliable code. Furthermore, I provide a proof-ofconcept implementation of a tool that enables the automation of the introduced verification workflow, providing the following features: • Automated MCM verification of a specified {Microarchitecture, MCM, High-level language} combination resulting in a list of possible MCM violations using TriCheck. • Parsing and transformation of C11 code into a formal modelling language, enabling the use of traditional model verification frameworks. • Automated query generation for use in above-mentioned model checking frameworks. • Feedback of error-prone lines of code in the editor itself. • Suggested corrections using conditionals and mutex locks for safer code