torstai 17. kesäkuuta 2010

Onnekas poika.


Kirjoitin joskus aikaa sitten itsepäisestä joukosta. Se kuuluu ns. osittaisjärjestysreduktioiden menetelmiin. Wikipedian artikkeli on vieläkin puutteellinen, koska en ole sitä korjannut, eikä sitä kukaan muukaan tule tekemään.

Nimitys "partial order" tulee menetelmässä siitä, että rinnakkaisessa järjestelmässä tapahtumilla ei ole totaalista järjestystä, koska eri komponentit toimivat (ainakin osittain) asynkronisesti, ja itsenäisesti toimivat osaset voivat suorittaa omat toimintonsa (tiettyyn rajaan asti) toisistaan riippumatta. Niillä on kuitenkin osittainen järjestys. Esimerkiksi jos meillä on puskurissa jo dataa, ja puskuria lukee (poistaa purkurista) ja kirjoittaa (lisää puskuriin) eri prosessi, on täysin yhdentekevää, missä järjestyksessä nämä toiminnot suoritetaan, jos puskurin kapasiteetti ei täyty, eikä se toisaalta tyhjene. Toisaalta, puskuriin täytyy kirjoittaa ainakin kerran, ennenkuin siitä voidaan lukea. Koska tapahtumien suoritusjärjestys on (pääosin) yhdentekevä, so. niiden suoritusjärjestys ei vaikuta järjestelmän toiminnan "oikeellisuuteen", on missa tahansa verifiointimenetelmässä riittävää tutkia mielivaltainen edustaja tapahtumien tietystä osajoukosta, puskurin tapauksessa siis niiden tapahtumien joukosta, joissa puskuri ei ole tyhjä.

Tämän menetelmän alla on myös muita tapoja hahmottaa reduktio. Esimerkiksi ns. tau-konfluenssi, jossa pyritään tunnistamaan järjestelmän abstrakteja tapahtumia, jotka voidaan ikäänkuin "siivota pois", koska ne eivät vaikuta oikeellisuuteen. Useimmissa näissä on jonkinlainen relaatio eri tapahtumien välillä, joka kertoo milloin tapahtumien suoritusjärjestyksellä on väliä. Menetelmästä riippuen pyritään tunnistamaan joukko tapahtumia (konfluenssin tapauksessa yksi tapahtuma), joka ei "häiritse" ulkopuolelle jätettyjä tapahtumia. Tapahtumien osittaisjärjestyksessä tämä tarkoittaa yleensä sitä, että mikään ulkopuolelle jätetty tapahtuma ei ole vertailukelpoinen minkään sisäpuolisen kanssa. (Varoitus: tämä karakterisointi on liian abstrakti, eikä ole edes täysin totta, mutta kelvatkoon nyt)

Olemme kehittäneet erään kolleegani kanssa teoriaa, jossa pyrimme paitsi hyödyntämään näitä osittaisjärjestysmenetelmiä, myös kehittämään eräänlaisen yhtenäisen teorian, jonka kautta kaikki nämä menetelmät voidaan ymmärtää. Se vähä mitä ymmärrän ja tiedän Galois'n kytkennöistä ikäänkuin kutittaa intuitiotani. Epäilen, että teoria voidaan tehdä sen avulla tavattoman paljon yksinkertaisemmaksi. Jotenkin niin, että voidaan esittää Galois'n kytkentä (ehkä jopa järjestysisomorfismi) eri menetelmien välille. Hylkäsin isomorfismihypoteesin ainakin yleisessä tapauksessa, koska itsepäisen joukon vahva ja heikko formulaatio eivät ole isomorfisia, mikä on helppo osoittaa. Olen itseasiassa liki vakuuttunut, että heikko formulaatio on se oikea rinnakkaisuuden teoria, so. tarkalleen se teoria, josta kaikki muu rinnakaisuuden redundanssi seuraa.

Sanon tämän tässä koska a) en usko, että kukaan voi varastaa tätä tutkimusaihetta kertomani perusteella ja b) jos voisikin, mieluummin näkisin teorian valmiina kuin yrittäisin vuosikaudet muotoilla sitä omin päin siinä onnistumatta. Vain totuudella on väliä.

3 kommenttia:

GM kirjoitti...

Ei muuta kuin onnea ja tarmokkuutta yritykseesi!

IDA kirjoitti...

lukee (poistaa purkurista) ja kirjoittaa (lisää puskuriin).

Merkitseekö tämä sitä, että purkurin tyhjennyttyä puskuri ei enää voi kasvaa?

;)

Tiedemies kirjoitti...

Sori, typo. "Puskuri" piti lukea molemmissa. Korjaan kun jaksan.