Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs

Maksym Bortin

TL;DR

The paper presents a framework for modelling, verification, and transformation of concurrent imperative programs by embedding a jump-based concurrent language into simply typed higher-order logic. It develops stepwise program correspondences, a Hoare-style rely/guarantee program logic with a program-correspondence rule, and a relational extension using state relations to strengthen specifications. Through case studies on Peterson's mutual exclusion algorithm, it demonstrates how auxiliary variables and relational postconditions enable robust termination and liveness proofs, including refinement and abstraction of code fragments. The work provides a foundation for sound, mechanisable reasoning about interleaved computations and supports formal verification using proof assistants. Overall, it offers a cohesive suite of techniques for exact reasoning about correctness, termination, and liveness in concurrent imperative programs with interleaving and awaits.

Abstract

The paper gives a detailed presentation of a framework, embedded into the simply typed higher-order logic and aimed at the support of sound and structured reasoning about various properties of models of imperative programs with interleaved computations. As a case study, a model of the Peterson's mutual exclusion algorithm will be scrutinised in the course of the paper illustrating applicability of the framework.

A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs

TL;DR

The paper presents a framework for modelling, verification, and transformation of concurrent imperative programs by embedding a jump-based concurrent language into simply typed higher-order logic. It develops stepwise program correspondences, a Hoare-style rely/guarantee program logic with a program-correspondence rule, and a relational extension using state relations to strengthen specifications. Through case studies on Peterson's mutual exclusion algorithm, it demonstrates how auxiliary variables and relational postconditions enable robust termination and liveness proofs, including refinement and abstraction of code fragments. The work provides a foundation for sound, mechanisable reasoning about interleaved computations and supports formal verification using proof assistants. Overall, it offers a cohesive suite of techniques for exact reasoning about correctness, termination, and liveness in concurrent imperative programs with interleaving and awaits.

Abstract

The paper gives a detailed presentation of a framework, embedded into the simply typed higher-order logic and aimed at the support of sound and structured reasoning about various properties of models of imperative programs with interleaved computations. As a case study, a model of the Peterson's mutual exclusion algorithm will be scrutinised in the course of the paper illustrating applicability of the framework.

Paper Structure

This paper contains 65 sections, 56 theorems, 113 equations, 5 figures.

Table of Contents

  1. Outlining Some Basic Design Decisions
  2. (1a) expressing conditional statements by jumps
  3. (1b) sequential normalisation of conditional statements
  4. (2a) expressing while-statements by jumps
  5. (2b) sequential normalisation of extended while-statements
  6. (3) halting labels for sequential components
  7. Summary
  8. A Generic Concurrent Imperative Language
  9. The syntax
  10. The underlying computational model
  11. The rule
  12. The rules
  13. The rule
  14. The rule
  15. The rule
  16. ...and 50 more sections

Key Result

Proposition 3.2.1

Assume $\rho, \rho^{\prime} \models p\sqsupseteq_{r}\space q$ and $\rho^{\prime}\space \vdash (q,\space \sigma_2) \stackrel{ n}{\mathop{\rightarrow}}_{{\mathcal{P}}} \space(q^{\prime},\space \sigma^{\prime}_2)$ where $n\space \in\space \mathbb{N}$. Furthermore, suppose $(\sigma_1, \sigma_2) \in\spac

Figures (5)

  • Figure 1: Inductive rules for program steps.
  • Figure 2: A transition subgraph of $\mathsfit{parallel\hbox{-}inc}$.
  • Figure 3: Two threads in the mutual exclusion algorithm.
  • Figure 4: The threads augmented by the auxiliary variables.
  • Figure 5: $\mathsfit{thread}^{\mathit{aux}}_0$ 'unfolded' .

Theorems & Definitions (121)

  • Definition 3.1.1
  • Definition 3.1.2
  • Proposition 3.2.1
  • Proposition 3.2.2
  • proof
  • Corollary 3.2.3
  • Proposition 3.2.4
  • proof
  • Proposition 3.2.5
  • proof
  • ...and 111 more