Static Analysis of Multi-Core Applications

The goal of this project is to develop a static analysis tool that identifies program flaws that may arise when executing on a multi-core processor. In particular, we will target flaws that arise in lock-free algorithms. Concurrent programs are often plagued by race conditions on shared data. Lock-based solutions to this problem are conceptually simple and work reasonably well. However, they typically do not perform well for the fine-grained concurrency that is often needed on multi-core processors. As the number of processor cores increases, lock contention also increases and many processors are left idle. Lock-free algorithms achieve much greater processor utilization (and better performance) as the number of cores increases. However, lock-free algorithms are difficult to reason about. (To make matters worse, multi-core processors often use a relaxed memory model.) This project will focus on using bounded model checking in order to verify libraries that implement lock-free algorithms.