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 nonblocking
algorithms, e.g. a counter and a stack. Our speci cations 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.