TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

01/17/2019

∙

by   Emanuele D'Osualdo, et al.

∙

0

∙

share

We introduce TaDA Live, a separation logic for reasoning compositionally about the termination of fine-grained concurrent programs. We illustrate the subtlety of our reasoning using a spin lock and a CLH lock, and prove soundness.