Exploiting partial orders and symmetries in efficient analysis of message-passing concurrency
02/09/2022
Speaker
Abstract
The message passing paradigm is the lingua franca for developing large distributed-memory programs, such as high-performance scientific computing and event-driven web applications. Message-passing applications are often found to be using communication nondeterminism (used primarily to obtain efficiency by masking network latencies) and symmetric communication among processes (which keeps programming simple). Under communication nondeterminism, a process can post (possibly asynchronous) receive calls that can potentially match any of the messages sent to the process. Under symmetric communication, a process’s communication structure may be partly or completely symmetric with the communication structure of other processes. Interestingly, communication nondeterminism is one of the important sources of analysis complexity and detecting symmetries is, in general, hard. This talk will present practical techniques to efficiently analyse message passing programs by (i) exploiting partial order among the communication dependencies and (ii) detecting symmetries in process-communication. The work covered in this talk has been published in TOPLAS 2017, FM 2018, ICST 2021, and ASE 2022.
Bio
Dr Subodh Sharma is an Associate Professor in Computer Science at IIT Delhi and holds the Pankaj Gupta Chair Professor position in Privacy and Decentralisation. He is also an associated faculty member in the School of Public Policy at IIT Delhi. Dr Sharma's research interests include ensuring the reliability of parallel software via static and dynamic program analyses, model checking, and PL solutions and employing HPC to create scalable verification technology. His recent research investigations have been in systems security, data privacy, and Blockchain.