This is an overview of recent work on the verification of concurrent programs. Traditionally concurrent programs are interpreted under sequential consistency (SC). Even though SC is very intuitive and easy to use, modern multiprocessors do not employ SC for performance reasons, and instead use so-called ‘weak memory models’. Some of the well known weak memory models in vogue among modern multiprocessor architectures are Intel x-86, IBM POWER and ARM. The use of weak memory is also prevalent in the C11 model, leading to the release acquire fragment of C11. In this talk, I will introduce some of these memory models, as well as recent efforts in the verification of programs under these.
Short Bio:
Krishna is a professor at the Department of Computer Science and Engineering at the Indian Institute of Technology, Bombay. She obtained her PhD from IIT Madras. Her primary interests are in the areas of automata theory, logic, and formal verification of timed and probabilistic systems.
