Modular liveness proofs for concurrent programs

Reasoning about concurrent programs is difficult because of the need to consider all possible interactions among concurrently executing threads. Modular reasoning techniques sidestep this difficulty by considering every thread in isolation under some assumptions on its environment. To date, such techniques have been largely limited to the verification of properties that guarantee the absence of bad events (safety properties). The available modular techniques do not deal well with the remaining set of properties, which ensure that good events eventually happen (liveness properties).The aim of the proposed research is to develop logics for modular reasoning about liveness and performance properties of concurrent programs and methods of automating proofs in them. The logics and the methods should be applicable to a wide range of programs, including those that use fine-grained or non-blocking synchronization.The proposed research, if successful, will build the foundations for developing efficient, yet reliable, concurrent systems. In time, its results may feed into industrial tools for software development and verification.