Technical reports

Logics and analyses for concurrent heap-manipulating programs

Alexey Gotsman

October 2009, 160 pages

This technical report is based on a dissertation submitted September 2009 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Churchill College.

DOI: 10.48456/tr-758

Abstract

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 we develop modular program logics and program analyses for the verification of concurrent heap-manipulating programs. Our 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, we build on concurrent separation logic—a Hoare-style logic that allows modular manual reasoning about concurrent programs written in a simple heap-manipulating programming language.

Our first contribution is to show 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 exploits this modified reasoning principle to achieve modularity. The analysis can be used to automatically verify a number of safety properties, including memory safety, data-structure integrity, data-race freedom, the absence of memory leaks, and the absence of assertion violations. We show that we can view the analysis as generating proofs in our variant of the logic, which enables the use of its results in proof-carrying code or theorem proving systems.

Reasoning principles expressed by program logics are most often formulated for only idealised programming constructs. Our second contribution is to develop logics and analyses for modular reasoning about features present in modern languages and libraries for concurrent programming: storable locks (i.e., locks dynamically created and destroyed in the heap), first-order procedures, and dynamically-created threads.

Full text

PDF (1.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-758,
  author =	 {Gotsman, Alexey},
  title = 	 {{Logics and analyses for concurrent heap-manipulating
         	   programs}},
  year = 	 2009,
  month = 	 oct,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-758.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-758},
  number = 	 {UCAM-CL-TR-758}
}