Muutto Suomeen lähestyy. Olen edelleen kovin kiireinen. Viime viikolla lähetimme paperin CAV:iin ja nyt on viimeistelyn alla paperi joka lähtee toiseen hieman vähemmän merkitykselliseen foorumiin. Jos - ja tämä on aika epätodennäköinen "jos" - kaikki tällä hetkellä arvioitavana olevat paperit ja tämä nykyinen menisivät läpi, olisi vuodenvaihteen saldo 5 julkaisua joista kaksi on alan parhaimmistoihin kuuluvissa lehdissä, yksi erittäin kovatasoinen julkaisusarjan julkaisu ja kaksi muutakin ihan OK tasoa näkyvyydeltään.
Tutkimukseni sisältö täällä on ollut pääsääntöisesti ns. kommutatiivisuuteen perustuvat reduktiot. Mitä tämä tarkoittaa? Yksinkertaistaen kyse on siitä, että kun mallinnamme jonkin järjestelmän toimintaa, niin sitä simuloitaessa tai verifioitaessa tilojen ja polkujen määrä räjähtää osaksi siksi, että eri osaset systeemissä liikkuvat asynkronisesti. Erilaiset tapahtumat tapahtuvat mahdollisesti eri järjestyksessä ja lopputulos saattaa riippua (tai olla riippumaton) siitä, missä järjestyksessä ne tapahtuvat. Jos lopputulos on riippumaton järjestyksestä, tapahtumat kommutoivat.
Kommutaatio on tässä siis hieman eri asia kuin algebrassa. Ns. prosessialgebrassa toki näillä on samanlainen yhteys kuin siinä että a*b = b*a. Kahden tapahtuman suorittaminen rinnakkain merkitään usein "|||". Jos siis meillä on osaprosessit P ja Q, niin prosessi P ||| Q käyttäytyy niin, että P ja Q suorittavat kumpikin toimintojaan rinnakkain jossakin järjestyksessä. Esimerkiksi yksinkertainen järjestelmä jossa P = "a;stop" ja Q = "b;stop" voi suorittaa operaatiot a ja b missä tahansa järjestyksessä ja sitten lopettaa toimintansa.
Yleistäen, voidaan ajatella, että meillä on n kappaletta tällaisia osaprosesseja, joista jokainen suorittaa jonkun tapahtuman. Jos tapahtumat ovat riippumattomia, niin kokonaisuudessan näistä tapahtumista saa 2n eri tilaa, sen mukaan moniko tapahtuma on tapahtunut. Lopputuloksen kannalta ei kuitenkaan ole väliä, minkä välitilojen kautta päädytään siihen tilanteeseen, jossa kaikki tapahtumat on tehty. Reduktio toimisi tässä tapauksessa niin, että rakennamme vain yhden edustajan kaikille suorituksille. Tällainen edustaja on jokin suoraviivainen polku alkutilasta (jossa mitään ei ole tapahtunut) lopputilaan, jossa kaikki tapahtumat on suoritettu. Lopputilan ominaisuuksien tuntemiseksi vältämme eksponentiaalisen määrän työtä, koska joudumme tutkimaan vain n eri tilaa.
Emme kuitenkaan yleisessä tapauksessa voi vaikkapa ohjelmakoodista tai kemiallisesta reaktiosta tai mitä ikinä mallinnammekaan, tietää, ovatko jotkin koodirivit, reaktiot, viestin lähettämiset, jne keskenään kommutoivia. Tätä varten tarvitaan sovelluskohtaisia analyysimenetelmiä. Lisäksi tällainen reduktio voidaan muotoilla epäsymmetrisen riippuvuuden käsitteen kautta.
Esimerkiksi, yleensä sanomme, että a ja b ovat riippumattomat jos niiden suoritusjärjestyksellä "ei ole väliä". Mutta mitä "ei ole väliä" tarkoittaa? Pian huomataan, että tämä riippuu siitä kysymyksestä, johon haluamme vastauksen! Ajatellaan, että haluamme selvittää, voiko järjestelmä päätyä tilanteeseen, jossa x = 1 ja y = 1. Alussa x = 0, ja b kasvattaa x:n arvoa yhdellä. b voidaan suorittaa vain, jos y = 0. Ilmaisemme tämän näin: "b: [y ==0]: x:=x + 1". Lisäksi sovitaan, että a kasvattaa y:n arvoa. a:[T]: y:=y+1. a ja b eivät ole riippumattomia perinteisessä mielessä, koska jos suoritamme a:n, niin b:n suorittaminen tämän jälkeen ei ole mahdollista. Kuitenkin, jos suoritamme b:n, ei a:n suorittaminen mitenkään tästä riipu. Riippumattomuus onkin tässä tapauksessa epäsymmetristä.
Tällaista symmetriarikkoa ei yleensä ole otettu huomioon kommutatiivisuusreduktioissa, mutta me olemme kehitelleet menetelmää, jossa se voidaan ottaa huomioon. Menetelmä itsessään on vanhempi mutta olen väitöksenjälkeisenä aikana eli viimeiset noin viisi vuotta tutkinut tapoja saada siitä enemmän irti.
CAV:iin lähettämämme paperi perustuu tälle symmetriarikolle silloin, kun lopputulos on abstrakti. Se tarkoittaa tilannetta, jossa pyrimme vähentämään laskennallista kuormaa poistamalla tarpeettomia yksityiskohtia. Esimerkiksi jonkin muuttujan arvoiksi sovitaan vain "iso" ja "pieni", ja nämä saavat edustaa niitä kaikkia arvoja joita muuttuja voi saada. Tämä pudottaa potentiaalisesti äärettömän esityksen kahdeksi tilaksi. Muitakin tekniikoita on, toki.
Nyt työn alla oleva paperi on maanläheisempi. Siinä pyrimme tutkimaan miten symmetriarikkoa voi käyttää laskennallisesti hyväksi turvallisuusominaisuuksien verifioimisessa. Turvallisuusominaisuudet ovat muotoa "virhettä X ei tapahdu". Verifioinnissa voidaan keskittyä niiden tilojen tutkimiseen, joissa X voi periaatteessa tapahtua. Tähän tarvitaan kolme erillistä osaa. Ensimmäisessä vaiheessa sovelluskohtaista tietoa käytetään hyväksi tapahtumien riippumattomuuden analysointiin. Tämä vaihe riippuu sovelluksesta kaikkein eniten. Ohjelmakoodin osalta yleensä on joukko staattisia sääntöjä, tai sitten käytetään jotain symbolista menetelmää, jolla tapahtumien seurausten ja esiehtojen riippumattomuus analysoidaan. Toisessa vaiheessa lasketaan annetusta tilanteesta se, mitä tapahtumia voidaan kussakin tilassa sivuuttaa. Kolmas vaihe taas on itse tilojen läpikäymiseen tarvittava algoritmi. Tämä voi olla joko syvyyteen ensin- tai leveyteen ensin- tyyppinen haku. Muitakin vaihtoehtoja on.
Tässä viimeisessä paperissa siis tutkin asiaa koko skaalalla. Ensimmäiseen osaan otan melko tavallisen lähestymisen, jossa analyysi tehdään ohjelmakoodista yksinkertaisehkojen nyrkkisääntöjen perusteella. Aritmeettiset operaatiot kommutoivat tietyissä tilanteissa. Esimerkiksi yhteenlasku (ja sen erikoistapaus vähennyslasku) kommutoi toisen yhteenlaskun kanssa vaikka sijoitettava muuttuja olisikin sama, jos lisättävä luku on vakio molempien operaatioiden suhteen. Ja niin edelleen. Näitä sääntöjä on ehkä toistakymmentä, ja työ tehdään kerran, joten se on käytännössä hyvin nopeaa itse verifiointiin verrattuna. Näin saamme neljä relaatioita: Tapahtumat voivat olla riippuvaisia niin, että ne eivät kommutoi, eli jos molemmat suoritetaan, niin lopputulos riippuu suoritusjärjestyksestä. Ne voivat olla (epäsymmetrisesti) riippuvaisia niin, että a tekee b:n suorittamisen mahdottomaksi, mutta ei välttämättä toisin päin. Riippuvuus voi olla myös "vahdin" ja tapahtuman välinen. Vahdilla tarkoitetaan jotakin ehtoa jonka pitää toteutua jotta tapahtuma voidaan suorittaa. Tapahtuma riippuu omasta vahdistaan tällä tavalla ja toisaalta vahti voi riippua tapahtumasta, joka voi muuttaa sen todeksi.
Toisen vaiheen laskenta on tässä pihvi. Nämä relaatiot poikkeavat muodoltaan kirjallisuudessa aiemmin esitetyistä, ja kehitimme menetelmän jolla niistä voidaan laskea "riittävä" joukko. Tässä kohtaa algoritmille voidaan antaa vielä "vaatimus" eli algoritmille voi antaa relaatioiden lisäksi joukon tapahtumia, jotka se takuulla sisällyttää laskemaansa joukkoon. Tätä tarvitaan kolmannessa vaiheessa.
Kolmas vaihe taas on se, jossa turvallisuusvirhettä etsitään. Teemme sen näin: Spesifioidaan virhe, jota etsitään. Se voi olla vaikkapa muotoa "kaksi prosessia on yhtä aikaa muuttamassa kriittistä muuttujaa" tai "kanavassa on viesti ja lukija on lopettanut toimintansa". Olennaista on, että tällainen ominaisuus on jonkin tilan ominaisuus. Merkitään tätä predikaatilla P(x), missä "x" on tila. Jokainen tapahtuma on muotoa (g,e) missä g(x) on vahti, joka kertoo onko tapahtuma vireessä ja e(x) antaa sen tilan johon päädytään. Vaihtoehtoja on karkeastiottaen kaksi, ja ne ovat teoreettisesti lähes yhtäpitäviä. Ensimmäinen on, että koodaamme ylimääräisen "tapahtuman" joka on muotoa (P(x),I), missä I(x) = x on identiteettikuvaus. Sen jälkeen teemme ykkösvaiheen analyysin, ja lopulta laskemme tila-avaruuden niin, että takaamme seuraavan ominaisuuden: Jos jokin tapahtuma on mahdollinen ylipäänsä, niin se suoritetaan kutistetussa tila-avaruudessa. Toinen vaihtoehto on jakaa tapahtumat "näkyviin" ja "näkymättömiin" sen mukaan voivatko ne muuttaa P(x):n arvoa. Valitsimme ensimmäisen, koska se on teoriassa tehokkaampi mutta vain jos relaatiot ovat epäsymmetrisiä.
Reduktio eliminoi tapahtumia tiloista, jos ne ovat riippumattomia niistä jotka tutkitaan. Myöhemmissä tiloissa ne tutkitaan sitten erikseen, ja näin eliminoimme joitain tilanteita joissa kaksi tapahtumaa tutkitaan kahdessa eri järjestyksessä. Tämä johtaa joskus kuitenkin degeneroituneeseen tapaukseen. Voimme esimerkiksi tehdä silmukan joka on riippumaton muista tapahtumista. Tällainen silmukka tutkitaan ja kaikki muu jää tutkimatta. Siksi tarvitsemme ehdon joka takaa että mahdolliset tapahtumat suoritetaan. Ehto on hankala, koska se ei ole paikallinen, vaan riippuu siitä, mitä tulevaisuudessa on tutkittu. Yksi vaihtoehto on tehdä syvyyteen-ensin- haku, ja sallia peruuttaminen annetusta tilasta vain, jos sen seuraajissa on tutkittu "riittävästi" tapahtumia. Me yritimme tehdä enemmän. Tutkimme vahvasti kytketyn komponentin. VKK jakaa kaikki tulevaisuudet, koska se on kokoelma tiloja joissa voidaan kulkea "edestakaisin". Vasta kun koko VKK ollaan julistamassa valmiiksi, tarkistetaan onko "lupa" peruuttaa. Jos ei, niin katsotaan missä määrin on sivuutettu jotain suoritettavaa, ja palautetaan tämä kakkosvaiheen reduktiolle "vaatimuksena".
Tulokset olivat, kuten yleensäkin, todella hyviä niillä esimerkeillä jotka oli valittu niin että niissä esiintyvät erikoiset riippumattomuudet voidaan analyysissä selvittää ja tehokkaasti laskea. Tosielämän esimerkeillä tulokset olivat melko vaatimattomia. Parannuksia kyllä oli, mutta ne eivät olleet eksponentiaalisia, vaan vähäisiä ja inkrementaalisia.
Teoreettinen kontribuutio oli mielestäni mielenkiintoinen. Olen pyrkinyt parantamaan sitä jo kahdesti. Paperi on jo kahdesti hylätty. En ole kovin toiveikas.
Ei kommentteja:
Lähetä kommentti