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

Abstract

The goal of this Master's thesis is to continue the effort of specifying and verifying safety properties of the different algorithms presented in the Parallel Programming course given by Professor Pascal Fontaine. This endeavor is motivated by the creation of a formal companion to the course for students interested in the material. This companion will contain alternative descriptions of the algorithms presented, as well as their properties. This effort will also aim to identify potential errors or prove the correctness of the different algorithms presented in the lecture. Additionally, the lecture notes mention being able to exchange equivalent pieces of code when they have the same properties. The validity of this claim is also verified on an example.

The first chapter describes the principles of concurrent programming, the motivation behind its usage, and the challenges that come with it. The second chapter describes the Temporal Logic of Actions and the TLA+ Toolbox. The TLA+ environment allows the creation of specifications, their verification of properties on finite models, and the writing proofs. A description of all the different tools in the Toolbox is provided.

After the description of the tools, the barrier synchronization mechanism shown in the course is first specified. Several invariant properties are described and proven invariant using the \TLAplus Toolbox. It is also shown that it behaves like an abstract barrier where processes advance synchronously. Secondly, by extending the specification of the abstract lock with auxiliary variables and using the refinement mechanism present in \TLAplus, it is shown that the abstract lock and Peterson's algorithm are equivalent.