maanantai 1. syyskuuta 2014

Massakausi

Kuten lukijani tietävät, olen harrastanut hieman kestävyysjuoksua viimevuosina, ja viime syyskaudella osallistuin Tampereen puolimaratonille ja Lanzarote Maratonin 10 km matkalle (joka osoittautuikin 9 kilometriksi, mutta ei siitä enempää)

Vasenta jalkaani on vaivannut plantaarifaskiitti jo vuosia, mutta juoksua se ei haitannut, sillä vaikka vaiva on äärimmäisen tuskallinen liikkeelle lähdettäessä, lämmittelyn jälkeen jalka on täysin oireeton. Toisin on oikean polven vaivan kanssa, ja epäilen vaivan olevan ITBS. Se taasen kipeytyy noin viiden-kuuden kilometrin juoksun jälkeen lähes poikkeuksetta. Noin puolentoista vuoden ajan olen harjoitellut myös lasten kanssa Taekwondoa pari kertaa viikossa.

Päätin jättää juoksun hyllylle toistaiseksi, lukuunottamatta viikottaista muutaman kilometrin lenkkiä. Sensijaan päätin käydä pitkästä aikaa ns punttisalilla, ja aloitinkin pari viikkoa sitten harjoittelun.

Koska pidän systeemeistä ja systemaattisuudesta, laadin itselleni ohjelman, joka kiertää neljää eri harjoitusta; kaksi ala- ja kaksi ylävartalolle. Alavaltaron ensimmäiseeen treeneiin kuuluvat maastaveto ja jalkaprässi, plus pari pienempää liikettä, ja toiseen kyykkyjä ja pari pienempää. Ylävartalon ensimmäisessä treenissä on penkkipunnerrus ja soudut, jotain hartioille ja koukistajille eristävät, ja toisessa dipit, leuanvedot, jotain muut harteille ja ojentajille eristävät. Ohjelma on periaatteessa hypertrofinen, ja kokeilen melko yksinkertaista progressiota: Jokaisen liikkeen kohdalla tehdään kolme varsinaista sarjaa (+ lämmittelyt tarvittaessa). Kussakin sarjassa tehdään toistoja maksimissaan 12, samalla painolla. Sarjojen "tavoitevälit" ovat 10-12, 8-12 ja 6-12 toistoa. Merkitsen ylös sen, miten hyvin tavoiteväliin osutaan. Alarajalle osuminen tuottaa yhden plussan ja jos menee vähintään kaksi yli alarajan, niin tulee kaksi plussaa. Alarajan alittaminen (jos ei jaksa) tuottaa miinuksen, ja jos alittaa kahdella, tulee kaksi miinusta. Jos siis teen liikettä kolme sarjaa, 11 + 10 + 7, niin tuloksena on neljä plussaa. Jos toistot ovat 10, 6, 5, niin tuloksena on yksi plussa ja kolme miinusta.  Seuraavalla kerralla lasken edellisen kerran plussat ja vähennän tästä miinukset. Jos tulos on enemmän kuin yksi plussalla, niin rasitusta nostetaan niin vähän kuin on mahdollista. Jos plussia on kuusi, niin nostetaan kaksi pykälää. Miinuksiin ei reagoida muuten kuin että niiden määrän pitäisi vähentyä joka kerta, jos ei ala vähentyä, tai jos lisääntyvät, niin täytyy pudottaa painoa tai levätä.

Olin yllättänyt siitä, miten kovan nälän pari- kolme kertaa viikossa harjoittelu tuottaa. Syön yleensä aamiaiseksi kolme kananmunaa, raejuustoa ja paahtoleipää, mutta se ei tunnu riittävän enää mihinkään. Lounaalla söin tänäänkin parikymmentä lihapulla ja runsaasti salaattia. Olen lisäksi vaihtanut juomakseni valion Plus-kaakaojuoman, ja silti mässäilen iltaisin aika tavalla. Esimerkiksi perjantaina kävin tuttavien kanssa Plevnassa, ja söin kaksi erillistä annosta, ensin Bratwurstia ja sitten vielä currywurstin.

Paino lähti harjoittelun alettua välittömästi raketin lailla nousemaan vain noudattamalla periaatetta "syö sen verran kuin nälättää, lisää hieman proteiinia". Otin viikon verran kreatiina, mutta lihasturvotus oli aika-ajoin kivuliasta, joten lopetin sen. Painoni nousi (oletettavasti pitkälti kreatiinin tuoman nesteen kertymän vuoksi) yli neljä kiloa kahdessa viikossa, tosin nousu vaikuttaa nyt hidastuneen.  Painondeksini on ollut tyypillisesti alle 20, nyt se on jo lähellä 22:ta. Normaalipainon rajoissa pysyminen ei tuota ongelmia, koska voisin lihoa vielä n 11 kiloa ennenkuin ylipainon raja tulisi vastaan. En aio kuitenkaan nostaa painoani merkittävästi tästä; massakausi saa kohta loppua.

On mahdotonta sanoa, miten systeemi tulee toimimaan ja miten se tulee vaikuttamaan. Nuorempana kävin kuntosalilla ja harjoittelin lähinnä voimanostolajeja tarkoituksenani saada mahdollisimman suuria maksimituloksia. Tekniikkani oli pielessä ja tukilihaksisto heikko, joten sain selkäni lopulta kipeäksi ja luovuin. Lisäksi noudatin pitkälti vegaanista ruokavaliota; se ei sinänsä olisi haitannut kehitystä, mutta ruokavalio oli muuten niin kasvis- ja erityisesti kuitupitoinen, etten yksinkertaisesti jaksanut syödä riittävästi. Nyt näyttäisi alustavasti siltä, että massan hankkiminen ei ainakaan vielä ole tässä iässä kovin vaikeaa, tosin lieneekö tämä lisäys lähinnä läskiä, sitä on vaikea sanoa. Kolmessa viikossa *voi* tapahtua lihasmassan kasvua, mutta tuskin neljää kiloa.

Koska treeniä on jatkunut vasta näin vähän aikaa, ei koko ohjelma ole ehtinyt pyörähtää ympäri kuin kaksi kertaa. Lähes jokaisessa liikkeessä olen edelleen päässyt lisäämään painoa, useimmissa kaksi pykälää. Tässäkin aion ottaa hyvin rauhallisesti, koska kun mennään lähelle maksimaalisia suorituksia, loukkaantumisen riski kasvaa aina. Yhden uuden ilmiön olen huomannut, eli lihasjäykkyyden lisääntymisen. Taekwondon vuoksi täytyy venytellä paljon, ja se on muuttunut kivuliaammaksi näiden treenien myötä. Käsivarren ojentajat ovat esimerkiksi melko jäykät, samoin reiden koukistajat.


maanantai 25. elokuuta 2014

Todiste islamisaatiosta?

Aamulla kun katsoin blogini etusivulta, josko joku olisi kommentoinut aiempia kirjoituksiani, havahduin sivupalkissa pyörivän mainoksen sisältöön: Siinä mainostettiin muslimien omaa deittipalvelua, ja mainoksessa oli luonnollisesti useammat hymyilevät naisen kasvot, hiukset huivin peittämänä jokaisella.

En ole blogissani juuri aihetta käsitellyt, koska se on epämiellyttävä. En pidä oikeastaan mistään ko. aiheeseen liittyvästä. En pidä uskontojen näkyvästä roolista kulttuurissa tai politiikassa lainkaan, riippumatta uskonnosta, enkä erityisesti pidä vanhoillisuuteen ja aggressiiviseen "oikeassaolemiseen" kehottavista oppijärjestelmistä, jollainen islam pitkälti on. En pidä keskustelusta, jota aiheesta Suomessa käydään, koska en pidä niiden tahojen tyylistä, jotka kritiikkiään esittävät. En pidä siitä, että koen ettei asiasta voi sanoa mitään järkevää ilman että leimautuu joko vaahtosuiseksi rasistiksi tai silmät ja korvat poliittisen korrektiuden nimissä sulkevaksi punaviherhipiksi. En pidä siitä miten islamia kritisoidaan, enkä pidä siitä, miten sitä puolustellaan tai miten kritiikkiin reagoidaan. En pidä oikeastaan mistään koko aiheessa. Toivoisin että asia menisi pois kokonaan ilman että minun pitäisi sanoa siitä mitään.  Aihe on kiusallinen, koska tunnen henkilökohtaisesti muslimiksi identifioituvia ihmisiä, joita vastaan minulla ei ole yhtään mitään, mutta joiden tiedän kokevan loukkaavana sellaisenkin kritiikin joka mielestäni on aiheellista. Se on kiusallinen, koska tunnen aivan mukavia ja myötätuntoisia ihmisiä jotka eivät epäröi laajentaa kaikkea kritiikkiä joka islamia kohtaan voidaan jossakin tilanteessa esiittää, koskemaan lähes jokaista muslimiksi tunnustautuvaa.

En pidä aiheesta. Enkä pidä siitä, miltä ko. mainos minusta näyttää. En pidä yhtään.


lauantai 23. elokuuta 2014

Rage against the Machine

Sukuni on kohtuullisen suuri, tai ikäluokkaani nähden ehkä noin keskitasoa, sillä minulla on noin kaksikymmentä serkkua. Suvussa ei ole mitään valtavan suuria perheitä, mutta vanhempani kuuluivat ns suuriin ikäluokkiin, joten heillä on yhteensä kymmenen sisarusta. Isovanhempien kuoltua olen pitänyt vain harvakseltaan yhteyttä serkkuihini, paria poikkeusta lukuunottamatta. Yhteydenpitoon on sukulaisuuden  lisäksi ollut näissä tapauksissa "syynä" jokin yhteinen intressi. Yksi serkuistani on tällä hetkellä taloustieteen tenure trackillä New Yorkin Columbia yliopistossa, ja hänen äitinsä asuu muutaman kilometrin päässä, joten tapaamme kun hän käy Suomessa. Toinen asuu Tampereella ja harrastaa tietokoneita.

Pari vuotta sitten - juuri ennen päätöstä lähteä Singaporeen - aloitin kotiprojektia, jossa oli tarkoitus rakentaa pienimuotoinen klusteri vanhoista tietokoneista. Idea oli hauska, ja pääsin projektissa sellaiseen vaiheeseen, jossa ns head-nodella pyöri tarvittavat palvelut ja teoriassa MPICH2 oli asennettuna, jotain säätämistä jäi vielä ssh:n ja avainrenkaiden kanssa. Jätin projektin siihen, koska ns muut kiireet tulivat eteen. Aloin viritellä ideaa uudelleen hiljattain, kun tein vähän siivousta ja löysin osan koneista (ison osan olin jo vienyt kierrätykseen).

Serkullani oli ylimääräistä rautaa, sillä hän harrastuksensa vuoksi hankkii koneita kotiinsa ja hankkiutuu vanhemmasta päästä eroon. Tällä kertaa kategoriassa "hyötykäyttöön halvalla" oli vanhempi neliydinprosessorilla varustettu kone ja kaksi GeForce GTX 580- näytönohjainta. Mooren laki on toisinaan hieman hämmentävä: yksi tällainen näytönohjain, joka nykyisin on vakavalle käyttäjälle "ei tee mitään"- tasoa, sisältää (tosin hyvin rajoitetulla käskykannalla) laskentatehoa saman verran kuin top500- supertietokoneet 90-luvun puolivälissä, ja kahdella tällaisella olisi ennen vuotta 1990 voinut rakentaa maailman suorituskykyisimmän tietokoneen.

Kasasimme tästä raudasta minulle konetta, jonka tarkoitus olisi lämmittää (kyllä, lämmittää) olohuonetta kylminä talviaamuina. Idea oli suunnilleen seuraavanlainen: Kone laskisi kahdella näytönohjaimellaan ja neljällä prosessorillaan aamuyöllä Boinc:ia, ja muina aikoina toimisi pääosin mediaserverinä.

Ongelmat alkoivat heti alussa, sillä virtalähteessä ei ollut riittävästi piuhoja. Vaihdoimme virtalähteen, mutta kone ei herännyt juuri lainkaan kun kaksi näytönohjainta oli kytkettynä. Koetimme kombinatorisesti eri vaihtoehdot ja totesimme että vain yksi kerrallaan voi olla asennettuna. Sen jälkeen kävi ilmi, että osa muistikammoista ei läpäissyt testejä, joten muistin määrä tipahti neljään gigatavuun. Asensin Xubuntun, ja kaikki näytti menevän hyvin. Kotona kuitenkin huomasin että näytönohjain ilmeisesti toisinaan v*****lee ja kone hyytyy. Sen verran sain toimimaan, että tiedostojen jakaminen toimii vaimon Windows-koneen kanssa niin päin, että "serveri" näkee jaetut hakemistot. Vaihdoin näytönohjaimen ajurin ja kaatuilu näytti loppuvan, mutta ääni lakkasi toimimasta. Yöllä luovutin ja jätin boincin pyörimään, nyt aamulla kone oli kaatunut; Boinc pyöri vielä, mutta hiiren kursori oli jumissa, ja kun yritin avata konsolin, sain hetkeksi ruudulle virheilmoituksen joka näytti viittaavan  näytönohjainvikaan. Sain ajettua koneen alas semi-hallitusti, sillä jotain oli vielä sen verran pystyssä että virta katkesi parinkymmenen sekunnin päästä kun olin painanut kytkintä, eli en joutunut vetämään powerista sähköjä pois.

Nyt haasteet jatkuvat. Olin unohtanut miten hauskaa, sellaisella kummallisen masokistisella tavalla, tämä säätäminen on.


maanantai 18. elokuuta 2014

Ajolähtö

Kuten lukijat suureksi osaksi tietävätkin, määräaikainen "virkani" päättyy vuoden vaihteessa ja akateeminen urani mahdollisesti päättyy. Olen lueskellut vuosien saatossa erinäisiä kirjoitelmia akateemisen uran ankeudesta, vaikeuksista, vaativuudesta, ja huonosta palkkauksesta. Osan näistä kirjoitelmista olen kirjoittanut myös itse.

Systeemisiä ongelmia on, sitä en voi kieltää, mutta suurin osa valituksesta on itseasiassa turhaa ja perustuu vääriin käsityksiin ja vääränlaiseen asenteeseen; oletan tämän johtuvan siitä että ihmisillä on idealisoitu kuva akateemisesta urasta ja tätä idealisaatiota on ylläpidetty vielä 20 vuotta sitten julkisin varoin. Muutos on kuitenkin jo tapahtunut ja edessä olisi jo kauan aikaa sitten ollut sopeutuminen. Oma tragediani on oikeastaan se, että olen elänyt murroksen kynnyksellä oikeastaan koko elämäni. Lama-aika oli Suomessa huipussaan kun olin itse vielä koululainen. Kirjoitin ylioppilaaksi samana vuonna kuin Suomi liittyi Euroopan unioniin, ja lamasta toipuminen oli kovassa vauhdissa Nokian vetämänä opiskeluaikoinani. 

Opiskelijamäärien kasvattaminen tekniikan alalla alkoi juuri kun aloitin opintoni. Sinä vuonna kun itse pyrin opiskelemaan, useat varsin menestyneet lukiotoverini jäivät ilman tavoittelemaansa opiskelupaikkaa silloisessa Tampereen teknillisessä korkeakoulussa. Apukoulun priimuksena tieni oli jotenkin vähän turhan sileä, sillä työmarkkinat opiskelemillani aloilla vetivät hurjasti väkeä ja saatoin ylläpitää illuusiota siitä, että valitsin useiden vaihtoehtojen joukosta juuri sen mitä aloin tehdä. Tämä oli ensimmäinen väärinkäsitykseni. Tosiasiassa ajauduin akateemiselle uralle, koska en oikeasti edes viitsinyt miettiä mitä teen. Paria teollisuuspalveluiden parissa viettämääni kesätyötä lukuunottamatta en edes ole allekirjoittanut kuin yhden työsopimuksen, kun virkasuhteet muutettiin työsuhteiksi. Valintani olivat aina tosiasiassa helpoimpia, ns default-valintoja.

Tein väitöskirjaani viisi vuotta sillä idealla, että se syntyy "siinä sivussa", kun muulta elämältä ehtii; koin pääasialliseksi työkseni luennoinnin, ja tämä pitikin tavallaan paikkaansa koska vaativammilla algoritmikursseilla oli paljon väkeä ja kukaan muukaan ei niitä oikeastaan halunnut pitää. Tätä ei pidä ymmärtää väärin: Pidän kyllä tutkimuksesta, mutta teoreettinen tutkimukseni ei tapahtunut minkään tutkimusryhmän ja/tai projektin puitteissa vaan ainoastaan kirjoitin ideoitani paperille ja julkaisin ne. Tällainen ajattelu sopii ehkä matemaatikoille, mutta olin valitettavan tietämätön, uppiniskainen ja sinisilmäinen, ja ajattelin että jos vain tuotan tasaisesti papereita, niin urani etenee ilman sen kummempaa pähkäilyä. Näin se oli toiminut edellisellä sukupolvella, joten miksi minä olisin ollut poikkeus? Tämä oli kuitenkin virhe, johon havahduin ensimmäisen kerran viisi vuotta sitten, kaksi vuotta väittelyn jälkeen: Jotain pitäisi tehdä.

Siinä vaiheessa "strateginen" painopiste oli että tutkimuksessa pitäisi olla kansainvälistä yhteistyötä. Silloisen yliassistentuurini alkaessa tavoitekeskustelussa esitettiin "dosentin pätevyyden" saavuttaminen. Perinteisesti tämä on tulkittu niin, että tutkimusvolyymin tulisi vastata toista korkeatasoista väitöskirjaa. Kaksi vuotta väittelemisen jälkeen käärin vihdoin hihat ja aloin tuottaa, ja parin vuoden päästä minulla oli kasassa vaadittava volyymi vaikka kahteen uuteen nippuväitöskirjaan, ja kaikki tutkimus oli tehty nimekkäiden ulkomaisten tutkimusryhmien kanssa.

Tässä kohtaa kuitenkin kävi ilmi että maalitolppia oli siirretty parin vuoden aikana: Dosentuureja ei enää myönnettäisi yliopiston omille kasvateille elleivät nämä tuo sisään rahaa. Tämä oli sikäli kummallinen linjaus, että esimerkiksi Akatemian hankkeita ei voi hakea, jos ei ole dosentuuria. Ensimmäisenä totesin, että stop, nyt täytyy vetää henkeä, joten lähdin vuodeksi Singaporeen. Päätin että OK, aletaan sitten tykittää hakemuksia.

Nyt toinen viisivuotiskauteni on päättymärrä. Vuoden 2010 jälkeen olen tehnyt laskujeni mukaan 13 erilaista rahoitushakemusta, joista tasan yksi (1), Tekniikan edistämissäätiön post-doc- avustus, sai myönteisen päätöksen. Yliopiston virallinen kanta on, että minun työni ei ole vaatimustasoltaan sellainen jossa rahoituksen hankkiminen on omalla vastuullani; kuitenkin työni arvioidaan sen mukaan, onnistunko rahoituksen hankkimaan. Tämä on mielenkiintoinen tilanne. En kuitenkaan protestoi sitä, että tämä kuuluu työhöni, ainoastaan sitä, että se mitä tehtäväksi väitetään ja se mitä tosiasiassa edellytetään eivät ole sama asia. Tämä väärinkäsitys on se, minkä korjaaminen korjaisi paljon ja säästäisi paljolta valittamiselta. Koska työnantaja todellisuusessa edellyttää asiaa X, mutta väittää edellyttävänsä asiaa Y, niin tekemällä asiaa Y, ura tyssää siihen mitä on tekemässä, ja seuraavissa YT-neuvotteluissa tällaiset ihmiset laitetaan ulos tai heidän määräaikaisuuttaan ei uusita.

Akateemisen uran varsinaisia edellytyksiä ja odotuksia yksittäisissä tilanteissa minusta ei ole juurikaan syytä kritisoida. Olisi toki mielekästä, jos työtä voisi "vain tehdä", eli kun löytää sen tason jolla omaa työtään haluaa jatkaa, sitä voisi jatkaa ja antaa niiden siirtyä muihin tehtäviin joita se kiinnostaa. Tutkimus (ja mielestäni myös yliopistotason opetus) on kuitenkin luonteeltaan sellaista, että pysähtyminen vanhan hyväksi havaitun tekemiseen on itseasiassa takapakkia,  joten voidaan perustella sitä että uusiin asioihin tulisi aika-ajoin siirtyä. Parhaat tutkijat eivät kuitenkaan ole usein hyviä johtajia, ja kuitenkin, mitä parempi tutkija yksilö on, sitä nopeammin hänen oletetaan siirtyvän johtotehtäviin. Tiedän muutamiakin tapauksia joissa nuorena "menestynyt" henkilö on mennyt parhaiden tutkijavuosiensa osalta jossain määrin hukkaan, koska ei ole päässyt keskittymään tutkimukseen vaan joutunut manageroimaan muiden tutkimusta. Kuten eräs kolleegani -- aikanaan saman ikäinen ja samassa uravaiheessa kuin minä nyt -- totesi, akateemisen uran suurin ongelma on siinä, että jos todella pidät tutkimuksesta, niin työnantajan näkökulmasta se asia jolla sinut "palkitaan" kun teet sen mahdollisimman hyvin, on työtehtävä jossa et saa tehdä sitä, missä ole hyvä ja mistä pidät.

Itse en ole kaksinen tutkija, jos sillä tarkoitetaan kammiossaan itsenäisesti ideoivaa neroa. Itseasiassa, olen paljon parempi  kehittämään eteenpäin muiden ideoita. Ajatukseni ja analyysini etenee liiaksi syvyyteen ensin- tyylisesti, jotta olisin oikeasti hyvä miettimään mitään suuria linjoja tai tekemään merkittäviä avauksia. Pidän ongelmanratkaisusta, ja kun muilla on uusia ongelmia, heitän mielelläni kaiken ja alan generoida ratkaisuideoita. Toimin siksi parhaiten ryhmässä; ryhmässä jota minulla ei ole juuri nyt.

Haen tämän syksyn haussa Akatemiatutkijan rahoitusta viideksi vuodeksi. Lisäksi toimin haamukirjoittajana yhdelle akatemiahankkeelle. On todennäköistä, että joudun vuodenvaihteessa puolen vuoden pätkälle, jota ei jatketa mikäli kumpikin hakemuksista kariutuu. Mikäli näin käy, lopetan tämän bloginkin kokonaan, koska en ole enää "tiedemies", eli en tee tutkimusta työkseni.

Jos taas rahoitus myönnetään, joudun manageroivaan rooliin, enkä silloinkaan oikeastaan saa enää tehdä sitä, mistä tutkimuksessa eniten pidän. Tilanne on hieman kiusallinen.

torstai 31. heinäkuuta 2014

Logiikka ja laskenta.

Olettakaamme että olemme tutkimassa jonkinlaisen systeemin S käyttäytymistä. Systeemissä on erilaisia muuttujia, joita voimme ehkä mitata, emme ehkä täydellisesti mutta voimme kuitenkin saada jotain tietoa. Oletetaan että nämä muuttujat ilmaistaan symbolilla x. Tämä on siis periaatteessa vektori kaikesta siitä, mikä systeemissä on olennaista. Oletan tässä että meillä on lisäksi käsite aika, joka on yksi muuttuja, mutta yksinkertaisuuden vuoksi oletan että se ei ole mukana mainitussa x:ssä.

Systeemin tila on jollakin ajanhetkellä muuttujan x arvo. Jos tunnemme systeemin tilan kahtena ajanhetkenä, niin oletamme että systeemi on siirtynyt ensimmäisestä tilasta toiseen; se, miten systeemi siirtyy tilasta toiseen, määrittää systeemin dynamiikan. Melko yleisiä systeemien dynamiikan kuvaamiseen käytettyjä formalismeja ovat esimerkiksi differentiaaliyhtälöt. Jos x koostuu komponenteista x1, x2, ..., xn, niin meillä on tyypillisesti useampia differentiaaliyhtälöitä jotka kuvaavat sitä miten muuttujien kehitys ajan suhteen riippuu toisistaan. Esimerkiksi voisi olla vaikkapa kahden muuttujan systeemi, jossa x1' = x2 ja x2' = -x1. Tämä on hyvin yksinkertainen systeemi, jossa siis x1 kasvaa sitä nopeammin mitä suurempi x2 on ja x2 taas pienenee sitä nopeammin mitä suurempi x1 on; tällainen systeemi on oskilloiva, mutta se ei nyt ole olennaista.

Differentiaaliyhtälöillä kuvataan järjestelmiä, jotka ovat jatkuvia. Jatkuvuus viittaa siis siihen, että aika etenee tasaista tahtia ja muuttujat ovat tyypillisesti reaali- tai kompleksilukuja. Differentiaaliyhtälöillä kuvataan lisäksi järjestelmiä jotka ovat deterministisiä, eli niiden toiminta on tarkalleen määrätty kun tila tunnetaan. Deterministisen sijaan järjestelmä voi olla esimerkiksi stokastinen, jolloin sen toimintaan liittyy jokin satunnainen komponentti, esimerkiksi differentiaaliyhtälössä voi esiintyä satunnaismuuttujia, jolloin saatu yhtälö ei kuvaakaan järjestelmän tilaa ajan funktiona vaan ainoastaan tilan jakaumaa. Kolmas vaihtoehto on, että järjestelmä on epädeterministinen, mikä tarkoittaa että sillä on aidosti useita eri polkuja; tätä käytetään erotuksena stokastisesta siten, että epädeterminismi tulee esimerkiksi mukaan malliin tuntemattomien vuorovaikutusten kautta.

Jatkuvan sijaan järjestelmä voi olla myös diskreetti. Diskreetin järjestelmän tilan määrittämät muuttujat saavat diskreettejä arvoja kuten kokonaisluku- tai boolean arvoja (tosi/epätosi). Järjestelmää jossa on sekä diskreettejä että jatkuvia muuttujia nimitetään hybridijärjestelmiksi. Diskreetin järjestelmän dynamiikkaa voidaan aina kuvat tilasiirtymärelaatiolla, joka kertoo mihin muihin tiloihin jostakin tietystä tilasta voidaan päätyä. Tämä relaatio on funktio jos järjestelmä ei ole epädeterministinen, ja jos järjestelmä on stokastinen, niin funktion arvoina ovat jakaumat tilojen yli. 

Predikaattiabstraktio viittaa siihen, että osa muuttujista korvataan predikaateilla. Predikaatti on totuusarvoinen väittämä joka koskee muuttujaa tai muuttujajoukkoa. Esimerkiksi jos meillä on muuttujat x ja y, niin väittämät x < y, x+y > 3, x < 0 jne ovat predikaatteja jotka puhuvat muuttujista x ja y. Tyypillisesti jos me käsittelemme jatkuvaa järjestelmää, predikaattiabstraktio on yksi tapa muuttaa järjestelmä diskreetiksi. Jos esimerkiksi x ja y ovat jatkuvia muuttujia, järjestelmän tilaa saatettaisiin abstrahoida esittämällä se kolmen predikaatin avulla: x < 0, y < 0 ja x2 + y2 < 9. Tällöin meillä olisi kahdeksan erilaista "tilaa" sen mukaan, missä kvadrantissa x ja y ovat ja sen mukaan ovatko ne 3-säteisen ympyrän sisällä vai eivät. Predikaattiabstraktio tuottaa epädeterminismiä vaikka alkuperäinen järjestelmä olisi kuvattu deterministisellä differentiaaliyhtälöllä. Esimerkiksi kun x = 5 ja y = 1, järjestelmä kehittyy niin, että y muuttuu negatiiviseksi, mutta pysyy ympyrän ulkopuolella ja kun x = 1 ja y = 5, y pienenee mutta pysyy positiivisena niin, että järjestelmä siirtyy ympyrän sisäpuolelle. Kumpikin arvoiyhdistelmä on kuitenkin mainittujen predikaattien kannalta "sama", eli abstraktio samastaa eri tavoin käyttäytyviä tiloja.

Jos tunnemme järjestelmän "riittävän hyvin" ja meillä on "riittävän hyvät" abstraktiot siten, että laadullisesti abstraktion tuottama malli kertoo meille "riittävästi", voimme luoda järjestelmän toiminnasta diskreetin mallin ja ennustaa, onko alkuperäisellä systeemillä jokin tietty abstrakti tila johon se päätyisi. Esimerkiksi voiko käydä niin, että sekä x että y ovat negatiivisia ja ympyrän ulkopuolella.

Sivuutan tässä nyt sen problematiikan joka liittyy tilasiirtymärelaation esittämiseen. Huomautan lisäksi että yleisessä tapauksessa tällaiset abstraktiot sisältävät potentiaalisesti satoja tai tuhansia predikaatteja siten, että järjestelmän diskreettienkin tilojen määrä on suurempi kuin koko maailmankaikkeudessa olevien atomien määrä; tällaisen järjestelmän kaikkien tilojen tutkiminen on yksinkertaisesti mahdotonta.

Voimme kuitenkin käyttää tähän logiikkaa, niin erikoiselta kuin se kuulostaakin. Yksi takavuosien menestyksekäs metodi oli niin kutsuttu rajoitettu mallintarkastus eli bounded model checking. Sen ideana on, että me esitämme järjestelmän alkutilan predikaattien avulla, esimerkiksi p1 & p2 & not p3 jne. Tämän lisäksi esitämme tilasiirtymärelaation logiikan kaavana siten, että jos tämänhetkisessä tilassa puhutaan predikaatista p, niin jälkimmäisessä puhutaan predikaatista p'. Esimerkiksi jos p on predikaatti joka vaihtaa totuusarvoaan jokaisessa siirtymässä, tätä merkitään p -> p', joka taas sievenee muotoon  not p or p'.

Oletetaan, että "virheellinen tila" voidaan ilmaista kaavalla Y. Jos meillä on jotakin tilajoukkoa kuvaava kaava X ja tilasiirtymän kaava P( ), niin sitä tilajoukkoa joka saavutetaan joukosta X käsin, voidaan ilmaista P(X). (Tämä on siis taas kaava). Kaikki predikaatit esiintyvät tässä kaavassa (se voi olla hyvinkin suuri) pelkkinä propositioina. alkutilan ollessa x, tarkistamme onko kaava X = (x tai P(x) tai P(P(x)) tai ....) yhdessä kaavan Y kanssa mahdollista tehdä todeksi, eli onko kyseinen kaava X ja Y satisfiable eli SAT. Valitettavasti X voi kuvata vain äärellisen määrän askelia (siitä nimitys "bounded") joten tämä menetelmä voi kyllä löytää virheitä, muttei voi todistaa että järjestelmässä ei sellaisia ole.

SAT on NP-täydellinen ongelma, mutta modernit SAT-ratkaisijat ovat niin tehokkaita, ja todellisista järjestelmistä peräisin olevat mallit ovat niin strukturoituja että SAT-ratkaisijat kykenevät ratkomaan tuhansien ja jopa miljoonien klausuulien mittaisia kaavoja, joissa on kymmeniä tuhansia tai satoja tuhansia muuttujia. Toki on aina patologisia tapauksia jotka tyystin tukahduttavat ratkaisijat, mutta ne ovat todellisen maailman malleissa hyvin harvinaisia.

Meidän ei ole kuitenkaan aivan pakko tyytyä siihen ettemme koskaan saisi todistettua järjestelmää täysin oikeaksi. On nimittäin mahdollista toisinaan löytää induktiivisia invariantteja jos sovelletaan abstraktiota luovasti.

Ensimmäinen, yksinkertainen tapa on yrittää löytää ns kiintopiste. Jos kaava X kuvaa kaikkia niitä tiloja joihin voidaan päästä n:llä tai sitä pienemmällä määrällä askelia, ja jos kaava (P(X) tai X) on yhtäpitävä kaavan X kanssa, tiedämme, että kaava X itseasissa kuvaa jo kaikki mahdolliset saavutettavat tilat; jos kaava (X ja Y) on ristiriitainen, ei järjestelmä voi saavuttaa tilaa jossa Y pätee. 

Tällainen kiintopiste voi olla kuitenkin niin monen askeleen päässä -- tai mikä pahempaa, järjestelmällä voi olla ääretön määrä mahdollisia tiloja (mikä tosin ei ole mahdollista jos käytämme tiukkaa predikaattiabstraktiota, mutta sivuutan sen nyt) -- että meiltä loppuu muisti tai aika ennenkuin löydämme kiintopisteen. Jos olemme nyt -- jonkin askelmäärän jälkeen -- todenneet että X kuvaa siihen mennessä saavutettavia tiloja, ja X ja Y ei ole SAT, voimme aina löytää tälle kaavalle niinsanotun interpolantin. Interpolantti on kaava Z, joka sisältää vain X:lle ja Y:lle yhteisiä symboleja, X implikoi Z:n ja Z on ristiriidassa Y:n kanssa.

Interpolantti Z voidaan nyt abstrahoida, siis tehdä siitä heikompi, kunhan se on edelleen ristiriidassa Y:n kanssa. Jos tätä merkitään kaavalla Z' niin sopivalla abstraktion valinnalla saatamme esimerkiksi pystyä osoittamaan että kaava Z' onkin kiintopiste -- se on siis induktiivinen invariantti, kaava joka kerran todeksi tultuaan pätee vaikka tekisimme kuinka tilasiirtymiä. Jos tällainen abstraktio löydetään, olemme kertakaikkisesti osoittaneet että Y ei voi toteutua järjestelmässä.


tiistai 29. heinäkuuta 2014

Pohjanmaan roadtrip.

Kävimme perheen kanssa pienellä pohjanmaa-roadtripillä viikonloppuna. Tarkalleenottaen matkasta suurin osa taittui Etelä-Pohjanmaalla ja Pohjanmaalla.  Ajoimme kolmostietä Vaasaan, missä vietimme päivän Tropiclandiassa. Käyskentelimme vähän aikaa Vaasan keskustassa ja yövyimme leirintäalueella. Aamusta lähdimme verkkaiseen tahtiin ajamaan kohti PowerPark- huvipuistoa Alahärmässä, joka on nykyisin osa Kauhavaa. PowerParkista suuntasimme takaisin Tampereelle Alavuden Tuurin kautta, missä pysähdyimme jäätelölle kuuluisan Kyläkaupan luona.

Pohjanmaan maakunnat ovat syntyvyyden puolesta Suomen hedelmällisimpiä maakuntia. Keski- ja Pohjoispohjanmaan maakuntien nettohedelmällisyysluku on ainoina maakuntina selvästi yli uusiutumisrajan, ja Etelä-Pohjanmaa on siinä hilkulla (samoin Kainuu, mutta en ole tottunut laskemaan sitä osaksi "Pohjanmaata", vaikka moni muu niin tekeekin). Eteläpohjalainen murre jakaa mielipiteitä. Siinä kuuluu joitakin piirteitä hämäläismurteista, mutta siinä selkeästi myös pohjoisempia piirteitä, jopa ripaus itämurteita. Yleisesti eteläpohjalainen murre assosioidaan ns häjyihin eli puukkojunkkareihin, jotka olivat eräänlainen suomalainen vastine gangsta-kulttuurille 1800-luvun Suomessa, bling-blingeineen kaikkineen. Huumekaupan sijaan poltettiin viinaa, ja kromattujen pyssyjen sijaan oli koreasti helattuja puukkoja. Eteläpohjalaiseen kulttuuriin liittetään merkityksiä kuten kunniantunto, väkivaltaisuus, pelottomuus ja tietynlainen korskeus ja suurieleisyys. Tästä kielivätkin nykypäivänä vieläkin niin PowerPark kuin Keskisten kyläkauppakin. Ilmiö ja kulttuuri on joillekin vastenmielinen, mutta esimerkiksi Pohjanmaan, Keski-Pohjanmaan ja Etelä-Pohjanmaan talousluvut ovat useimpina vuosina olleet selkeästi muuta maata paremmat ja työttömyys alhaisempi kuin maassa keskimäärin.

 Pidin Pohjanmaan maisemista. Teitä oli miellyttävä ajaa pääsääntöisesti. Pysähdyimme matkalla PowerParkista Alavudelle erään maatilan pihaan, koska tien varressa mainostettiin kahvilaa. Tuvassa oli termospullosta ihan hyvää kahvia euron take-away-pahvimuki, ja ihmiset vaikuttivat tavattoman ystävällisiltä. Muutoinkin kotimatka sujui pahemmitta ongelmitta. Pirkanmaalle saavuttuamme tie 65 oli hivenen ruuhkainen ja muutamat kuljettajat tekivät hieman vaarallisenoloisia ohituksia.

Voin suositella näitä kohteita lapsiperheille. Tropiclandia oli hieman pettymys kun on tottunut Singaporen tarjontaan, ja PowerParkissa ongelmaksi tuli se, että nuorempi poika on hivenen alle 130 senttiä, joten iso osa hurjimmista laitteista jäi häneltä väliin. Lapsen temperamentistä, hurjapäisyydestä, ja koosta riippuu, kannattaako siellä käydä; hurjapäinen mutta alle 130 senttinen pettyy kyllä.

Tänään podenkin sitten ensimmäistä kertaa vuosikausiin kesäflunssaa. Hiostava ilma, kuumeinen olo, kurkkukipu ja nivelsärky ovat varsin epämiellyttävä yhdistelmä.

sunnuntai 20. heinäkuuta 2014

Terveiset Wienistä.

Olen parhaillaan Wienissä, Itävallassa, osallistun Vienna Summer of Logic- konferenssikollektiiviin. Wien on miellyttävä kaupunki, mutta juuri tällä hetkellä täällä on melko kuuma; päivämaksimi on 33 astetta. Ilma ei ole kostea kuten Singaporessa, joten se ei ole yhtä tukala (jos pysyttelee varjossa), ja TU-Wienin konferenssitilat ovat ilmastoituja.

Eilen entinen ohjaajani palkittiin tutkimuksestaan yhdessä kolmen kilpailijan kanssa. Päätin väitöskirjaa tehdessäni että pysyttelen tästä nimenomaisesta aiheesta erossa, mutta post-doc vaiheessa ajauduin siihen kuitenkin. Aihe on kokenut eräänlaisen renessanssin liki 20 vuoden tauon jälkeen, ja täällä olen törmännyt useampaankin ryhmään joka haluaa soveltaa teorioitamme.

Toivoa sopii että pienestä kiinnostuksesta tulee isompi "uusi aalto", sillä olen viimeisen viiden vuoden aikana penkonut aihepiirin jotakuinkin kokonaan ja epäilen että olen tällä hetkellä maailman johtava asiantuntija tällä kovin kapealla saralla. En julkaisujen määrässä, mutta väittäisin tietäväni aiheesta oikeasti enemmän kuin kukaan muu. Olen viime vuodet tosin yrittänyt pyristellä aiheesta eroon, koska koen kolunneeni sen kokonaan jo läpi, mutta se vähäinen maine mitä minulle on kertynyt, on valitettavasti leimannut minut jo nyt.

Esitelmä on tänään iltapäivällä, ja koska konferenssi on alan numero ykkönen ja kaikki isommat nimet ovat paikalla, tänään leimaudun lopullisesti joko aihetta tutkivinaan olevaksi pelleksi tai sitten asiantuntijaksi. Välimuotoa tuskin on olemassa...

Lisäpöytäkirja: Hauskana yhteensattumana mainittakoon, että ensimmäisen kerran CAV-award myönnettiin vuonna 2008 kahdelle tutkijalle jotka kehittivät reaaliaikajärjestelmien formalismit sille tasolle että niitä voitiin alkaa algoritmisesti verifioida. Tänä vuonna palkinto myönnettiin osittaisjärjestysreduktioiden kehittäjille. Mikä tekee yhteensattuman on, että meidän tämänpäiväinen esitelmämme (ja paperimme) käsittelee sitä, miten osittaisjärjestyreduktiot saadaan toimimaan reaaliaikajärjestelmien formalismeille; tätä ei ollut kukaan todella aiemmin tehnyt.