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, a specification and we wish 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.
Short Bio:
Prakash Saivasan | The Institute of Mathematical Sciences (imsc.res.in)
