Invariants and Model-checking for Parallel Programs
Virg Wallentine
Mizuno’s
approach:
Construct the program structure with all functions in
threads
Develop global invariants (this is the difficult part)
Implement global invariants as “await() ->S” statements
Translate await(boolean
condition) into correct synchronization statements
Model-checking:
derive global invariants and specify correctness
criteria for checking completeness of global invariants
build and test model, using correctness criteria to
check global invariants
Promela/spin and test – then recode in real language
Java JPF test
Verisoft test and recode for shared memory
Hard parts
deriving global invariants
developing correctness criteria (looking at the
problem in another way)
building a realistic test harness
balancing realism with size of state space
Example:
disk head scheduler: (from Andrews’ book pages 228-229)
DISK invariant: C and N are ordered sets and
all elements in C are >= head position and
all elements in N are <= head position and
(head position = -1 ==> (C is empty and
N is empty)
monitor diskScheduler
var position: int := -1;
var C, N: ordered set of int
:= empty;
procedure request(cyl[i]:int)
if position =-1 then position := cyl[i];
or if position != -1 and cyl[i] > position
then {
insert(N, cyl[i])
await(position = cyl[i])
}
or if position
!= -1 and cyl[i]
<= position
then { insert(N,
cyl[i]);
await position
= cyl;
}
end
if
procedure release()
if
C not empty then position :=
delete(C)
or
if C empty and N not empty then
{
interchange(C,N);
position:= delete(C);
}
or C
is empty and N is empty then position :=-1;
end
if
end
end