Verifying concurrent programs: Refinement, synchronization, sequentialization

B. Kragl, Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization, IST Austria, 2020.

Download
OA kragl-thesis.pdf 1.35 MB

Thesis | Published | English
Department
Series Title
IST Austria Thesis
Abstract
Designing and verifying concurrent programs is a notoriously challenging, time consuming, and error prone task, even for experts. This is due to the sheer number of possible interleavings of a concurrent program, all of which have to be tracked and accounted for in a formal proof. Inventing an inductive invariant that captures all interleavings of a low-level implementation is theoretically possible, but practically intractable. We develop a refinement-based verification framework that provides mechanisms to simplify proof construction by decomposing the verification task into smaller subtasks. In a first line of work, we present a foundation for refinement reasoning over structured concurrent programs. We introduce layered concurrent programs as a compact notation to represent multi-layer refinement proofs. A layered concurrent program specifies a sequence of connected concurrent programs, from most concrete to most abstract, such that common parts of different programs are written exactly once. Each program in this sequence is expressed as structured concurrent program, i.e., a program over (potentially recursive) procedures, imperative control flow, gated atomic actions, structured parallelism, and asynchronous concurrency. This is in contrast to existing refinement-based verifiers, which represent concurrent systems as flat transition relations. We present a powerful refinement proof rule that decomposes refinement checking over structured programs into modular verification conditions. Refinement checking is supported by a new form of modular, parameterized invariants, called yield invariants, and a linear permission system to enhance local reasoning. In a second line of work, we present two new reduction-based program transformations that target asynchronous programs. These transformations reduce the number of interleavings that need to be considered, thus reducing the complexity of invariants. Synchronization simplifies the verification of asynchronous programs by introducing the fiction, for proof purposes, that asynchronous operations complete synchronously. Synchronization summarizes an asynchronous computation as immediate atomic effect. Inductive sequentialization establishes sequential reductions that captures every behavior of the original program up to reordering of coarse-grained commutative actions. A sequential reduction of a concurrent program is easy to reason about since it corresponds to a simple execution of the program in an idealized synchronous environment, where processes act in a fixed order and at the same speed. Our approach is implemented the CIVL verifier, which has been successfully used for the verification of several complex concurrent programs. In our methodology, the overall correctness of a program is established piecemeal by focusing on the invariant required for each refinement step separately. While the programmer does the creative work of specifying the chain of programs and the inductive invariant justifying each link in the chain, the tool automatically constructs the verification conditions underlying each refinement step.
Publishing Year
Date Published
2020-09-03
Page
120
ISSN
IST-REx-ID

Cite this

Kragl B. Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization. IST Austria; 2020. doi:10.15479/AT:ISTA:8332
Kragl, B. (2020). Verifying concurrent programs: Refinement, synchronization, sequentialization. IST Austria. https://doi.org/10.15479/AT:ISTA:8332
Kragl, Bernhard. Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization. IST Austria, 2020. https://doi.org/10.15479/AT:ISTA:8332.
B. Kragl, Verifying concurrent programs: Refinement, synchronization, sequentialization. IST Austria, 2020.
Kragl B. 2020. Verifying concurrent programs: Refinement, synchronization, sequentialization, IST Austria, 120p.
Kragl, Bernhard. Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization. IST Austria, 2020, doi:10.15479/AT:ISTA:8332.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Main File(s)
File Name
Access Level
OA Open Access
Date Uploaded
2020-09-04
MD5 Checksum
26fe261550f691280bda4c454bf015c7

Source File
File Name
Access Level
Restricted Closed Access
Date Uploaded
2020-09-04
MD5 Checksum
b9694ce092b7c55557122adba8337ebc

Material in IST:
Part of this Dissertation
Part of this Dissertation
Part of this Dissertation
Part of this Dissertation

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar