Logics and analyses for concurrent heap-manipulating programs

Reasoning about concurrent programs is difficult because of the need to consider all possible interactions between concurrently executing threads. The problem is especially acute for programs that manipulate shared heap-allocated data structures, since heap-manipulation provides more ways for threads to interact. Modular reasoning techniques sidestep this difficulty by considering every thread in isolation under some assumptions on its environment. In this dissertation the author develops modular program logics and program analyses for the verification of concurrent heap-manipulating programs. The approach is to exploit reasoning principles provided by program logics to construct modular program analyses and to use this process to obtain further insights into the logics. In particular, the author builds on concurrent separation logic-a Hoare-style logic that allows modular manual reasoning about concurrent programs written in a simple heap-manipulating programming language.

The contributions are twofold. First, it shows the soundness of concurrent separation logic without the conjunction rule and the restriction that resource invariants be precise, and to construct an analysis for concurrent heap-manipulating programs that exploit this modified reasoning principle to achieve modularity. Secondly, it develop logics and analyses for modular reasoning about features present in modern languages and libraries for concurrent programming: storable locks, first-order procedures and dynamically-created threads.
 
Reasoning about concurrent programs is difficult because of the need to consider all possible interactions between concurrently executing threads. The problem is especially acute for programs that manipulate shared heap-allocated data structures, since heap-manipulation provides more ways for threads to interact. Modular reasoning techniques sidestep this difficulty by considering every thread in isolation under some assumptions on its environment. In this dissertation the author develops modular program logics and program analyses for the verification of concurrent heap-manipulating programs. The approach is to exploit reasoning principles provided by program logics to construct modular program analyses and to use this process to obtain further insights into the logics. In particular, the author builds on concurrent separation logic-a Hoare-style logic that allows modular manual reasoning about concurrent programs written in a simple heap-manipulating programming language.

The contributions are twofold. First, it shows the soundness of concurrent separation logic without the conjunction rule and the restriction that resource invariants be precise, and to construct an analysis for concurrent heap-manipulating programs that exploit this modified reasoning principle to achieve modularity. Secondly, it develop logics and analyses for modular reasoning about features present in modern languages and libraries for concurrent programming: storable locks, first-order procedures and dynamically-created threads.