The TAU Programming Languages and Systems Seminar - Proving consistency of concurrent data structures and transactional memory systems
Artem Khyzha, PhD (Alexey Gotsman) at IMDEA Software Institute. Currently a post-doc at TAU
ABSTRACT:
Programmers can manage the complexity of constructing concurrent software with the help of libraries of concurrent data structures and, more recently, transactional memory. Both approaches facilitate software development by giving a programmer correctness guarantees that abstract from the implementation details of libraries and transactional memory: the programmer can expect that each library method or transaction execute atomically, even if in reality the implementation executes them concurrently. To justify these correctness guarantees, researchers typically prove certain consistency conditions: linearizability for concurrent data structures and opacity for transactional memory.
This presentation is dedicated to proving consistency conditions formally. We propose a modular program logic and proof techniques capable of reasoning about fine-grained concurrent implementations of data structures and transactional memory. We also provide formal foundations for the programming model in which memory can be accesses both inside and outside of transactions.