Verification of C11 Concurrency

Sanjana Singh, Divyanjali, Subodh Sharma
Nov 10, 2020 Concurrency

Verification of parallel systems is a complex exercise. The large state spaces created due to thread interleavings complicates the verification of such parallel systems. The problem becomes even harder in case of parallel programs executed under relaxed memory models. Under this project we are investigating two directions:

  • A runtime analysis that uses dynamic partial order reduction (DPOR) to verify other multi-copy atomic (oMCA) behaviors of C++11 programs
  • A static analysis of Release-Acquire memory fragment of C11 concurrency by exploiting thread-modular abstract interpretation technique.

These projects is funded by the DST Early Career Research grant.

DPOR Abstract Interpretation Concurrency
Subodh Sharma
Subodh Sharma
Associate Professor and Pankaj Gupta Chair Professor in Privacy and Decentralisation