Caches, Coherence and Accelerations of Transactional Memories

In a multicore machine a number of caches are used to efficiently make data available. Caches improve performance by reducing memory access time and by decreasing the required bandwidth. Caches play a central role in the working of a multicore machine as they ensure efficient data access for the processors. As there can be several processors each with its own cache(s), protocols are needed to organize the access to the shared memory. Several Problems araise when dealing with the correctness of such protocols as they can become tricky to get right. The protocols we consider in this project can be used to maintain the consistency between all caches in the system (Directory based or snoopy Coherency protocols), or to use the caches to store tentative versions for transactional memory algorithms. These algorithms are used to shield multicore programmers from the complexity of concurrency by importing database techniques (STMs) and accelerating them using hardware. In this project, we concentrate on the automatic verification of properties ranging from cache coherence and deadlock freedom of cache coherence protocols, to strict serializability and progress of hardware accelerated transactional memory algorithms. All these verification problems are hard in that they may involve an arbitrary number of caches or transactions of arbitrary length.