Modular Termination Verification for Non-blocking Concurrency

Authors

  • Pedro da Rocha Pinto
  • Thomas Dinsdale-Young
  • Philippa Gardner
  • Julian Sutherland

Abstract

We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread’s concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.

Venue

Proceedings of the 25th European Symposium on Programming (ESOP’16), pp. 176–201

Publication Date

Apr 2016

Identifiers

Source Materials