Tarkvarateaduse instituudi doktorant Hendrik Maarand kaitseb oma doktoritööd "Operational Semantics of Weak Sequential Composition" ("Nõrga jadakompositsiooni operatsioonsemantika") reedel, 26.06.2020 kell 10:00 ruumis ICT-507 A/B (Akadeemia tee 15A) ja zoomi vahendusel.

Programm on kogum juhiseid arvutile mingi ülesande täitmiseks ning üks oluline konstruktsioon programmides on juhiste andmine jadamisi: esmalt tee seda ning alles seejärel toda. Kaasaegsed arvutisüsteemid aga ei pruugi sellist järjestikulisuse tingimust rangelt järgida. Nad tagavad vaid, et meile jääb mulje, nagu oleks kõike tehtud jadamisi ning just antud järjekorras. See kõik toimub ressursikasutuse optimeerimiseks (näiteks, et programmi täitmine võtaks vähem aega). Kui meil aga on mitmelõimeline programm, mida me käitame mitmetuumalisel protsessoril, siis ainuüksi sellest, et meile jääb mulje, nagu igat lõime täidetakse jadamisi, enam ei piisa. Teisisõnu, kui me tõlgendame jadakompositsiooni mitterangelt ehk lõdvalt, siis meie mitmelõimeline programm võib anda lõpptulemusi, mis ei ole võimalikud jadakompositsiooni range tõlgenduse korral. Käesolevas doktoritöös uuritaksegi sellist lõtva jadakompositsiooni ning arendatakse vahendid programmide sammsammulise täitmise formaalseks kirjeldamiseks taolise lõdva jadakompositsiooni korral. Niisugused kirjeldused on programmide usaldusväärse analüüsi aluseks.

Juhendaja juhtivteadur Tarmo Uustalu (Tallinna Tehnikaülikool).

Oponendid:

• vanemlektor Brijesh Dongol (Surrey Ülikool, Ühendkuningriik)
• professor Peter Thiemann (Freiburgi Ülikool, Saksamaa).

Doktoritöö on avaldatud tehnikaülikooli raamatukogu digikogus.