Specifying and Verifying Safety Properties of Parallel Programming Algorithms Using the TLA+ Toolbox

Abstract

The goal of this Master’s thesis is to specify and verify safety properties of a few classical algorithms taken from the Parallel Programming lectures taught by Prof. Pascal Fontaine by using the TLA+ tool suite. The first chapter of this work lays out the minimal concepts of concurrent programming required to motivate the distinctive significance of software verification in the world of parallel and distributed algorithms. The second one presents all the tools of the TLA+ environment used in the following chapters. A rough methodology is established to turn pseudo-code descriptions of algorithms into unambiguous TLA+ specifications and to consequently identify and express safety properties of interest before checking and proving them.

The next chapters consist in applying the previously described tools and methods to Barz’s algorithm and the Readers-writers. The resulting TLA+ specifications, adjoining definitions and properties as well as TLAPS proofs constitute the original contribution of this Master’s thesis..