This is an overview of some 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 are Intel x-86, IBM POWER and ARM. Weak memory features are also incorporated in the development of modern programming languages such as C11 and Java. This talk is on the verification of concurrent programs under the release acquire (RA) semantics, with the main focus being on decidability and complexity questions.
Short Bio:
Krishna is a faculty member in the department of computer science and engineering at IIT Bombay. Her areas of research are automata theory, logics, and their applications to the verification of quantitative as well as distributed/concurrent systems.
