Viime yönä heräsin hikisenä, ensin luulin sairastuneeni, mutta noustuani istumaan huomasin, että oli vain kuuma ja olin nähnyt jotain painajaista. Minulla on ollut matkalla yskää vaihtelevasti. Ulkona on kostea ja saasteinen ilma, sisäilma puolestaan on viileää ja kuivaa. Näiden välillä vaiheteleminen tuntuu ärsyttävän ylähengistysteitä. Nyt olen saanut vielä pienen nuhankin. Toivottavasti en sairastu vakavammin seuraavan kahden päivän sisällä. Lähden kotiin lauantaiaamuna.
Matka täältä Hong Kongin lentoasemalle ei ole tavattoman pitkä - taksi lauttaterminaaliin, lauttamatka, kävely juna-asemalle ja junamatka - mutta kantamuksia on aika paljon ja lauttaterminaalin passintarkastuksessa joutuu aina vähän jonottamaan, joten se on melko rasittava terveenäkin.
Normaalitavoistani poiketen olen tällä tutkimuskeikalla koodannut aika paljon. Toiminnallisesti koodia ei ole montaa sataa riviä syntynyt, mutta kyse on vaikeahkoista algoritmeistä. Löysimme yhden abstraktin tilanteen, joka toivoaksemme toteutuu usein oikeissa malleissa - varmoja emme tietenkään voi olla - jossa olemassaolevat menetelmät ovat tehottomia, mutta johon meidän lähestymistapamme puree.
Olen ihmetellyt mallintarkastuksen - kaikille lienee jo selvää, että se on tutkimusalani - sitä ominaisuutta, että suurimmassa osassa mallintarkastusalgoritmeja muisti loppuu kesken hyvin nopeasti. Mallintarkastus tässä nyt voidaan ymmärtää laajassa mielessä. Oikeastaan ainoa lähestymistapa, jossa näin ei käy, ovat reduktiot ns. SAT-ongelmaksi, kuten ns. bounded model checkingissä on idea. Tällaisessa tilanteessakin "huijataan", sillä järjestelmän käyttäytyminen mallinnetaan johonkin kiinteään määrään askelia - esimerkiksi prosessorin toimintaa tutkitaan ensimmäisten 64 kellosyklin kohdalla. SAT-ongelma ei kasva eksponentiaalisesti esitystavaltaan, mutta kylläkin -- näin uskotaan -- suoritusajan osalta.
Tavanomaisissa tila-avaruuden esitystavoissa käy niin, että kun koneet tulevat jatkuvasti nopeammiksi ja halvemmiksi, muisti saadaan itseasiassa kulumaan loppuun entistä nopeammin. Muistin määrä ei kasva yhtä nopeasti. Eli kun 80-luvulla saattoi käyttää vuorokauden tai kaksi laskemiseen ennenkuin muisti loppui, nyt siihen kuluu minuutteja. Osa menetelmistä toki vaihtaa muistia ajaksi tekemällä laskentaa, jolla vältetään joidenkin tilojen tallettaminen muistiin, mutta ilmiö on silti olemassa.
Vakavastiottaen en ole ihan varma, onko tällä alalla pahemmin tulevaisuutta. Mallinnosprosessissa ja erilaisissa rinnakkaisten prosessien konfliktien tunnistamisen menetelmissä on paljon sellaista, josta on hyötyä tulevaisuudessa jos ja kun massiivisen parallelismin hyödyntäminen tulevaisuudessa tosissaan aloitetaan. Lisäksi abstraktion teoria yms. ovat luontevia ajattelutapoja tällaisten rinnakkaisista vuorovaikuttavista elementeistä koostuvien järjestelmien suunnitteelussa. Taidan olla kuitenkin liian vanha enää tekemään mitään oikeaa työtä. Mutta ainahan voin opettaa...
Täältä tähän. Saatan käydä tänään etsimässä Magic-kortteja myyvän kaupan. En tosin itse harrasta varsinaisesti, mutta ne saattavat olla halvempia täällä, joten niitä voi trokata.
Ei kommentteja:
Lähetä kommentti