Department of Computer Science and Technology

Technical reports

Formal verification-driven parallelisation synthesis

Matko Botinčan

March 2018, 163 pages

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

Abstract

Concurrency is often an optimisation, rather than intrinsic to the functional behaviour of a program, i.e., a concurrent program is often intended to achieve the same effect of a simpler sequential counterpart, just faster. Error-free concurrent programming remains a tricky problem, beyond the capabilities of most programmers. Consequently, an attractive alternative to manually developing a concurrent program is to automatically synthesise one.

This dissertation presents two novel formal verification-based methods for safely transforming a sequential program into a concurrent one. The first method — an instance of proof-directed synthesis — takes as the input a sequential program and its safety proof, as well as annotations on where to parallelise, and produces a correctly-synchronised parallelised program, along with a proof of that program. The method uses the sequential proof to guide the insertion of synchronisation barriers to ensure that the parallelised program has the same behaviour as the original sequential version. The sequential proof, written in separation logic, need only represent shape properties, meaning we can parallelise complex heap-manipulating programs without verifying every aspect of their behaviour.

The second method proposes specification-directed synthesis: given a sequential program, we extract a rich, stateful specification compactly summarising program behaviour, and use that specification for parallelisation. At the heart of the method is a learning algorithm which combines dynamic and static analysis. In particular, dynamic symbolic execution and the computational learning technique grammar induction are used to conjecture input-output specifications, and counterexample-guided abstraction refinement to confirm or refute the equivalence between the conjectured specification and the original program. Once equivalence checking succeeds, from the inferred specifications we synthesise code that executes speculatively in parallel — enabling automated parallelisation of irregular loops that are not necessary polyhedral, disjoint or with a static pipeline structure.

Full text

PDF (2.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-917,
  author =	 {Botin{\v c}an, Matko},
  title = 	 {{Formal verification-driven parallelisation synthesis}},
  year = 	 2018,
  month = 	 mar,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-917.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-917}
}