pretoceny uptime :)

[Pavel Kankovsky]

On Sat, 13 Apr 2002, Pavel Kankovsky wrote:

> 2. kod, ktery potrebuje obe hodnoty, je muze precist nasledujicimi
> prikazy (v praxi by to muselo byt v asembleru, nebo by se tam muselo
> rozhodit par volatile, aby to kompilator nevyoptimalizoval do
> ztracena):
> 
>          uint32_t jlo, jhi;
>          do {
>              jhi = jiffies_high;
>              jlo = jiffies_low;
>          }
>          while (jhi != jiffies_high);
> 

Uff...tak to se trochu nepovedlo. Omlouvame se ctenemu publiku za
snizenou kvalitu citovaneho prispevku zpusobenou zkratem v mentalnim
procesu autora. Tohle by fungovalo pouze za predpokladu, ze zapisujici
CPU zapisuje dost rychle. Coz je asi ponekud odvazny predpoklad. Spravne
reseni (snad <g>), ktere je o neco slozitejsi, je nasledujici:

A. Mame 32-bitove tri promenne: jiffies_low, jiffies_high a jiffies_low2
   inicializovane na zacatku nulami (pripadne jinymi hodnotami, ale musi
   na zacatku platit, ze j_low == j_low2).

B. Zapis probiha takto:
   1. inkrementuje se jiffies_low,
   2. inkrementuje se jiffies_high, pokud se jiffies_low pretocilo,
   3. inkrementuje se jiffies_low2 (nebo ze zkopiruje hodnota z j_low).

   Pritom musi platit, ze ctenari vidi zapisy provedene ve stejnem poradi,
   v jakem jsou tady uvedeny, coz muze vyzadovat pridani nejakych
   barierovych instrukci zde a mozna i behem cteni (*).

C. Cteni probiha takto:
   1. precte se jiffies_low2 a ulozi do lokalni promenne,
   2. precte se jiffies_high a ulozi do lokalni promenne,
   3. precte se jiffies_low a ulozi do lokalni promenne,
   4. porovnaji se prectene hodnoty jiffies_low a jiffies_low2, a pokud
      jsou ruzne, pak se opakuje od kroku 1.

   Predpoklada se, ze proces provadejici cteni se nemuze zablokovat na
   dost dlouho, aby se mezitim pretocila dolni pulka. Zaroven se
   predpoklada, ze je zanedbatelna pravdepodobnost, ze se opakovane
   strefi do aktualizace jiffies (asi by ale slo zeslabit predpoklad na
   rovnost j_low a j_low2 na neco jako j_low2 <= j_low, aby se opakovalo
   jen v pripade, ze to zrovna preteklo, protoze jindy k zadne zmene
   j_high nedochazi).

Dukaz spravnosti: Oznacme zapisy do jiffies_* pro strucnost wlo, whi, wl2
(low2) a cteni rlo, rhi, rh2. Relace < necht popisuje poradi, ve kterem
jsou operace provadeny (za jiz zminovanych predpokladu atomicnosti a
zachovani poradi zapisu vzhledem ke cteni; pokud nas zaroven nezajima
vzajemne poradi cteni v ruznych procesech, muzeme operace povazovat za
jednoznacne serializovatelne). Pak z popisu zapisu a cteni plati, ze:
a) wlo < whi < wl2, b) rl2 < rhi < rlo. Predpokladejme dale splneni
predpokladu uvedeneho u popisu cteni, tj. toho, ze lze zanedbat moznost,
ze mezi rl2 a rlo dojde k pretoceni jiffies_low*. Pak muze proces cteni
vydat nespravny (nekonzistentni) vysledkem pouze jsou-li vzhledem k zapisu
splneny nasledujici predpoklady: a1) wlo < rlo & wl2 < rl2 (zapisy j_low i
j_low2 probehnout drive nez cteni), a2) rhi < whi (zapis do j_hi probehne
pozdeji nez cteni), nebo b1) rlo < wlo & rl2 < wl2, b2) whi < rhi 
(tj. zrcadlove). V obou pripadech lze snadno dojit ke sporu:
ad a) wl2 < rl2, & rl2 < rhi ==> wl2 < rhi, & rhi < whi ==> wl2 < whi!
ad b) rlo < wlo, & wlo < whi ==> rlo < whi, & whi < rhi ==> rlo < rhi!
Jeste by se melo ukazat, ze problemy nemohou nastat kvuli kolizi jednoho
cteni s vice zapisy (avsak mene nez 2^32), ale to se mi uz nechce delat a
stejne je to intuitivne jasne. :)

Jak vidno, je to trochu komplikovanejsi (zapis vyzaduje dve aritmeticke
operace navic a pripadne i dve bariery), ale porad by to melo byt znatelne
levnejsi nez spinlocky.

(*) Mam ale dojem, ze na i386 (aspon na modelech dost starych, aby 
se tam vyskytoval problem uptime >= 500 dni <g>) nejsou potreba zadne.

--Pavel Kankovsky aka Peak  [ Boycott Microsoft--http://www.vcnet.com/bms ]
"Resistance is futile. Open your source code and prepare for assimilation."