I present recent work on the expressive specification and verification of termination of busy-waiting modules under a fair scheduler, as well as ongoing work on the expressive specification and verification of deadlock-freedom of programs that use blocking primitives such as futexes (under any scheduler). The specifications are expressive in that they support a wide variety of client scenarios, such as where a client acquires a lock in one thread and releases it in another, as seen in “cohort lock” implementations. I will point out the core shared idea underlying both approaches, as well as their differences.

Associate professor at the DistriNet research group at the Department of Computer Science, KU Leuven, Belgium