Dekkeruv algoritmus v smv

Potřebné informace o smv najdete na adrese http://www.cs.cmu.edu/~modelcheck/smv.html.
Poměrně pěkně srozumitelný manuál najdete na adrese http://www.cs.cmu.edu/~modelcheck/smv/smvmanual.ps

Kompilace smv pod linuxem suse 10.1

Problém byl, že mi binárky z výše uvedené stránky nechtěli chodit, a zdrojové kódy nešli přímo zkompilovat. Vyřešil jsem to následovně:


     $ tak -xzf smv.r2.5.3.tar.gz
   $ cd smv/
   $ repalce malloc __malloc -- storage.h
   $ replace  malloc __malloc -- *.c *.h
   $ make

Dekkerův algoritmus

Dekerův algoritmus je jeden z algoritmů zajišťující vzájemné vyloučení. Uvedu verzi pro dva procesy:


     //promenne spolecne pro vsecky procesy
   bool b1 = false; // o vstup do kriticke sekce zada proces 1 
   bool b2 = false; // o vstup do kriticke sekce zada proces 2
   int k = 1; // cislo procesu, ktery je pusten tim druhym k lizu, cislo procesu, ktery priste bude na rade
    
   //kod pro proces 1 
	while (1){ // tohle predstavuje nejak program, ktery porad dokola zada o vstup do ks.
		ncs(); 				//nekriticka sekce
		b1 = true; 			//pozadame o vstup do kriticke sekce
		while (b2) { 		// pokud i druhy proces ma zaregistrovanou zadost
			if (k = 2){ 	// pokud ma ted narok jit do kriticke sekce ten druhy
				b1 = false; //tak mu dame sanci (pustime ho)
				while (k = j) { 	//a cekame, nez skonci
					/* nic, aktivni cekani */
				}
				b1 = true; //pozadame o vstup do kriticke sekce
			}
		}
		
		cs(); //kriticka sekce
		k := 2; // priste mame pustit toho druheho
		b1 := false; // odregistrovat si vstup do kriticke sekce
	} //cely cyklus pres vsecko
	
	pro proces dva je kod analogicky

Realizace v modecheckeru smv

V smv musime nainplementovat modul main, ktery to spusti, pak modul pro kazdy proces (program, ktery) bude zadat o vstup do cs(); potom podmikny, ktere chceme kontrolovat a taky fairnes constraints, aby se nam jeden proces nezasil v kriticke sekci pro vzdy.

Podminky ke kontrole

Fairness constraint

Ověřujeme nekonečný model, takže je třeba některé fakty zadat pomocí fairnes constraint. Chceme, aby každý proces přišel k lizu nekonečně mnohokrát, pak aby procesy nemohly zůstat v kritické sekci na věky a také aby enmohly zůstat v nekritické sekci na věky.

Jak to naprogramovat

Modul p


     
	MODULE proc(k, bi, bj, i) -- 
   
	VAR
		-- stavy: kriticka/nekriticka sekce, testujeme jestli ma druhy proces 
		-- nastavenou zadost, testujem jestli jse
		-- na rade v if a ve while, viz popis algortimu.
		state : {critical,noncritical, test_bj, ftest_k, stest_k}; 
	DEFINE
	-- nastavit si jak se jmenuje ten druhy
	j := 
	case
		i = 1 : 2;
		i = 2 : 1;
	esac;
	
	ASSIGN
	-- inicializace stavu
	init(state) := noncritical;
	-- prechody mezi stavy
	next(state) :=
	case
		state = noncritical : {noncritical, test_bj};
		state = test_bj & (bj = false) : critical;
		state = test_bj & (bj = true) : ftest_k;
		state = ftest_k & (k = j) : stest_k;
		state = ftest_k & (k != j) : test_bj;
		state = stest_k & (k = j) : stest_k;
		state = stest_k & (k !=j) : test_bj;
		state = critical : {critical, noncritical};
	esac;
	-- prechody mezi zadostmi
	next(bi) :=
	 case
		state = noncritical & next(state) = test_bj : true;
		state = ftest_k & (k = j) : false;
		state = stest_k & (k != j) : true;
		state = critical &
		next(state) = noncritical : false;
		1 : bi;
	 esac;
	 -- prechody mezi tim, kdo je na rade
	next(k) :=
	 case
		state = critical &
		next(state) = noncritical : j;
		1 : k;
	 esac;

Modul main


     
	MODULE main
	VAR
		b1 : {true, false};
		b2 : {true, false};
		k : {1, 2};
		pr1 : process proc(k, b1, b2, 1);
		pr2 : process proc(k, b2, b1, 2);
	ASSIGN
		init(b1) := false;
		init(b2) := false;
		init(k) := {1, 2}; -- vybere smv

Specifikace podmímenek


     
	

-- Safety
SPEC
	AG !((pr1.state=critical)&(pr2.state=critical))

-- Liveness property
SPEC
	AG ((pr1.state=test_bj)->AF(pr1.state=critical))
SPEC
	AG ((pr2.state=test_bj)->AF(pr2.state=critical))
-- Non-blocking
SPEC
	AG ((pr1.state=noncritical)->EX(pr1.state=test_bj))
SPEC
	AG ((pr1.state=noncritical)->AF(pr1.state=test_bj))
-- No strict sequencing 
SPEC
	EF ( (pr1.state=critical) & E[ pr1.state=critical U (!(pr1.state=critical) 
	& E[!(pr2.state=critical) U (pr1.state=critical)])])

Specifikace Fairness constraint


     
	

FAIRNESS
	running
FAIRNESS
	!(state = critical)
FAIRNESS
	!(state = noncritical)

Program ke stažení

Poznámky a problémy při programování

Je to programování stzlem GOTO. Než si člověk zvykne takhle realizovat třeba cykly, tak to chvíli trvá. Spacifikaci mutal exclusion jsem opsal z prednasek.

Příslušné fairness constraint a podmínky je třeba mít v příslušném modulu

Ověření modelu Dekkerova algoritmu za pomoci modecheckeru SMV

Program ke stažení pro netrpělivé

Informace o smv