Title: Context-bounded liveness verification of multithreaded shared-memory programs

Speaker: Ramanathan S. Thinniyam    (bio) (bio)

Ramanathan Thinniyam is a postdoc at the Max Planck Institute for Software Systems at Kaiserslautern Germany, in the Rigorous Software Engineering group headed by Rupak Majumdar. He has been working on verification of multithreaded shared-memory programs, with an emphasis on context-bounded analysis. These results have been published at ICALP, POPL (Distinguished Paper, 2021) and TACAS (EAPLS Best Paper award, 2021). He obtained his PhD (TCS) from IMSc (HBNI Outstanding Doctoral Student award in Mathematics, 2019), MSc (TCS) from CMI and Btech Mech. from IIT Madras.

When: Tuesday, 01 February 2022 at 1900 hrs (IST)    

Abstract:
We study context-bounded verification of liveness properties of multi-threaded, shared-memory programs, where each thread can spawn additional threads. Our main result shows that context-bounded fair termination is decidable for the model; context-bounded implies that each spawned thread can be context switched a fixed constant number of times. Our proof is technical, since fair termination requires reasoning about the composition of unboundedly many threads each with unboundedly large stacks. In fact, techniques for related problems, which depend crucially on replacing the pushdown threads with finite-state threads, are not applicable. Instead, we introduce an extension of vector addition systems with states (VASS), called VASS with balloons (VASSB), as an intermediate model; it is an infinite-state model of independent interest. A VASSB allows tokens that are themselves markings (balloons). We show that context bounded fair termination reduces to fair termination for VASSB. We show the latter problem is decidable by showing a series of reductions: from fair termination to configuration reachability for VASSB and thence to the reachability problem for VASS. For a lower bound, fair termination is known to be non-elementary already in the special case where threads run to completion (no context switches).