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.
Long Term Goal
A platform that allows, with minimal human interaction, the verification and the validation of new cache protocols and hardware accelerated transactional memories.
Develop new approaches, symbolic representations and techniques to automatically prove correctness for realistic models of cache coherence and hardware accelerated transactional memory protocols.
To achieve automatic verification, we develop our techniques and tools based on using:
- Symbolic representations
- Language inclusion and simulation, Abstractions,
- Regular model checking
- First time full automatic verification of several cache coherence protocols for arbitrarily many caches
- Verification of strict serializability for a hardware accelerated transactional memory for arbitrarily many large transactions
- A software is being produced to combine regular automata techniques with abstractions for verification
Senior: Parosh Abdulla (Contact), Lukas Holik
Ph.D. student: YunYun Zhu