Proving correctness of a dynamic atomicity analysis in Coq
Caitlin Sadowski, Jaeheon Yi, Kenneth Knowles, Cormac Flanagan · 2008
Writing and reasoning about concurrent programs remains notoriously difficult despite the proliferation of type systems, static analyses, and dynamic analyses targeting concurrent programs. There are examples of verified developments for concurrent languages and programs (Chou and Peled 1996; Affeldt and Kobayashi 2004; Feng et al. 2007; Hobor et al. 2008) but most analyses – especially dynamic analyses – have not been subjected to mechanical rigor. We report on our partial mechanization in Coq of the recentlyreleased Velodrome dynamic atomicity checker (Flanagan et al. 2008). Velodrome examines a trace of a program to ensure that its atomic blocks are serializable. We specify the Velodrome analysis using a multi-threaded operational semantics with a collection of invariants relating the state of the analysis data structures to properties of the program trace. On top of an axiomatization of well-known facts about relations and program traces, we prove that Velodrome accurately reconstructs the transactional happens-before relation, the quotient of the usual happens-before relation where operations in the same transaction are identified. Although this proof is still a work in progress, we were able to identify a bug in the paper proof through the formalization process. An overview of our architecture is shown in Figure 1. Building on some utility code of Aydemir et al. (2008) we have written about 200 lemmas, 100 definitions, and a bit over 4000 lines of Coq code.