Title: Verifying Programs in Weak Memory Models with Persistency

Speaker: Prakash Saivasan    (bio) (bio)

Prakash Saivasan is an Assistant Professor at the Institute of Mathematical Sciences, Chennai. He obtained his PhD from Chennai Mathematical Institute in 2016 and has done postdocs at T U Braunschweig and T U Kaiserslautern in Germany. His areas of interest are automata theory, logic, concurrency, and formal verification.

When: Tuesday, 06 August 2024 at 1900 hrs (IST)       

Abstract:
In this talk, we will consider the problem of verifying concurrent programs. In here, we are given a set of programs that communicate through shared memory and a specification, we wish to algorithmically check if the programs violate the specification. The programmers, while writing code usually assume that the memory operations are immediate (referred to as sequential consistency). However, the modern day architectures, to optimise the running time, re-order the memory operations in a non-trivial manner. This leads to various memory models such as TSO, PSO and so on. We will walk through some of these memory models during the talk. The recent intel processor introduced persistency mechanism that allows for the writes to be archived. This can then be used to restart the computation in case of a crash. The main focus of the talk will be how to verify programs when persistency is combined with weak memory.