Analysis of Concurrent Software

Event-driven concurrent programming is central in many software domains such as smartphone applications, web browsers and cloud applications. While it makes software responsive and scalable, programmers have to deal with resulting non-determinism. The SEAL research group has developed foundational algorithmic techniques for finding bugs or proving their correctness. We have developed and released program analysis tools (www.iisc-seal.net/software) through which we found 50+ real bugs that were subsequently fixed by the developers. This work appears in several papers:

• Race detection for Android applications, P. Maiya et al. [PLDI 2014]
• Static deadlock detection for asynchronous C# applications, A. Santhiar et al. [PLDI 2017]
• Event-based concurrency: Applications, abstractions and analyses, A. Kanade [Invited book chapter, Advances in Computers, 2018]

For example, the PLDI 2017 paper above addresses the following problem. Asynchronous programming is a standard approach for designing responsive applications. Modern languages such as C# provide async/await primitives for the disciplined use of asynchrony. In spite of this, programs can deadlock because of incorrect use of blocking operations along with non-blocking (asynchronous) operations. While developers are aware of this problem, there is no automated technique to detect deadlocks in asynchronous programs.

This work presents a novel representation of control flow and scheduling of asynchronous programs, called continuation scheduling graph and formulate necessary conditions for a deadlock to occur in a program. We design static analyses to construct continuation scheduling graphs of asynchronous C# programs and to identify deadlocks in them. We have implemented the static analyses in a tool called DeadWait. Using DeadWait, we found 43 previously unknown deadlocks in 11 asynchronous C# libraries. We reported the deadlocks to the library developers. They have confirmed and fixed 40 of them.