Draft Modular Termination Verification for Non-blocking Concurrency

We present Total-TaDA, a program logic for verifying the to-tal correctness of concurrent programs: that such programs both terminate and produce the correct result. The termina-tion behaviour of a single thread can be conditional on the behaviour of its concurrent environment. With Total-TaDA, we are able to specify such constraints. This allows us to verify total correctness for non-blocking algorithms, such as a counter and a stack. Moreover, our approach is modular: we can verify the operations of a module independently, and build up modules on top of each other