Deductive Verification of Concurrent Programs with Why3
[ In these notes we refer to https://haslab.github.io/MFP/VF/2324/aula2 for reference. Recall that the focus of that class is the specification in TLA+, and verification with TLC, of concurrent algorithms. ]
Verification Method
Sequential algorithms entail deterministic transition relations and are for this reason easier to verify. In Why3 we do it without having to explicitly mention the transition relation(see first semester MFES course).
Concurrent algorithms are not deterministic. We model their execution by isolating atomic instructions, and allowing for interleaving between instructions of different processes/threads(we use the two words interchangeably). It is useful to consider configurations containing a program counter for each process; the transition relation will be generated by a number of actions that:
correspond to atomic instructions ;
are enabled by the program counter of the process that will execute the instruction ;
advance the program counter of that process
Example: Counter
Consider the concurrent counter example. Each thread executes a single instruction(without looping), incrementing a shared counter.
var x : integer = 0
procedure increment;
begin
0: x := x + 1
1: end;
increment || ... || increment
We will begin by using a simple(but unrealistic) model, which assumes atomic updates, i.e. that the instruction at label 0 is executed atomically, i.e. the value of the counter is read and written(incremented) in a single atomic step.
Each thread executes a single transition, with the PC advancing from label 0 to label 1.
The correctness property of interest is that when all threads terminate, the value of the counter equals the number of threads. We will be able to verify this property for an unbounded number of processes.
moduleCounter_Atomic_Updates
type state = Zero | One
type thread = int
val constant n_threads : int
axiom n_threads_pos : n_threads > 0
(* System configurations *)
type world = { pc : map thread state ; x : int }
Verification Method
Example: Counter
var x : integer = 0
procedure increment; begin0: x := x + 11: end;
increment || ... || increment
module Counter_Atomic_Updates type state = Zero | One type thread = int val constant n_threads : int axiom n_threads_pos : n_threads > 0
(* System configurations *) type world = { pc : map thread state ; x : int }
(* Initial configurations *) predicate initWorld_p (w:world) = w.pc = const Zero /\ w.x=0
(* System action: guard predicate and action function *)