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