"Eesti Teadusfondi uurimistoetus" projekt ETF9398
ETF9398 "Paralleeltarkvara kontrollitavad garantiid (1.01.2012−31.03.2016)", Silvio Capobianco, Tallinna Tehnikaülikool, TTÜ Küberneetika Instituut.
ETF9398
Paralleeltarkvara kontrollitavad garantiid
Verifiable guarantees for concurrent software
1.01.2012
31.03.2016
Teadus- ja arendusprojekt
Eesti Teadusfondi uurimistoetus
ETIS klassifikaatorAlamvaldkondCERCS klassifikaatorFrascati Manual’i klassifikaatorProtsent
4. Loodusteadused ja tehnika4.6. ArvutiteadusedP170 Arvutiteadus, arvutusmeetodid, süsteemid, juhtimine (automaatjuhtimisteooria)1.1. Matemaatika ja arvutiteadus (matemaatika ja teised sellega seotud teadused: arvutiteadus ja sellega seotud teadused (ainult tarkvaraarendus, riistvara arendus kuulub tehnikavaldkonda)100,0
PerioodSumma
01.01.2012−31.12.201211 610,00 EUR
01.01.2013−31.12.201311 610,00 EUR
01.01.2014−31.12.201411 610,00 EUR
01.01.2015−31.12.201511 610,00 EUR
46 440,00 EUR

Paralleelprogrammide kirjutamine on märkimisväärselt raske, kuid järjest kasvava praktilise tähtsusega. Käesolev projekt arendab matemaatilist alusaparatuuri ohutus- ja korrektsusgarantiidega efektiivse paralleelse arvutitarkvara tootmiseks, kasutades keelepõhist lähenemist. Reaalse elu poolelt nõuavad mitmeprotsessori arvutite kasvav dominants ja veebirakenduste kõikjalolek uusi tehnikaid ohutute (ajastusanomaaliate ning protsessoririkete suhtes robustsete) ja korrektsete (spetsifikatsioonile vastavate) programmide arendamiseks, mis ei ohverda efektiivsust. Tehniliselt poolt on tõestusassistentide, automaatsete teoreemitõestajate, mudelkontrollijate jm verifitseerimistööriistade drastiline edenemine teinud nad hõlpsasti kasutatavaks minimaalse õppimise järel ning neist on saanud moodsate integreeritud arenduskeskkondade komponendid. Projektis uurime uute paralleelkeelte primitiivide semantikat ja formaliseerime tulemused tõestusassistentidega. Kasutades koinduktiivseid meetode, arendame paralleelarvutamise programmiloogikaid, mis vahetult käsitlevad spetsiifilisi programmide käitumiste aspekte nagu mittetermineeruvus, interaktiivne sisend/väljund ja mittedeterminism. Nende loogikatest tuletame tüübisüstemaatilisi kompositsioonilisi programmianalüüse, uurime nende koostoimet valikuliselt sisselülitatavate programmianalüüside ühetaolises raamistus. Nende alusuuringute konkreetse rakendusena uurime dünaamilist moodulite süsteemi, kus moodulite laadimine toimub asünkroonselt.
Writing concurrent programs is notoriously difficult and is of increasing practical importance. The project develops mathematical infrastructure for producing highly efficient concurrent software programs and their correctness/safety guarantees, using formal methods and language-based technologies. On the real world side, the growing dominance of multiprocessor machines and the ubiquity of Web applications call for new technologies of building and maintaining safe (e.g., robust against timing anomalies and processor failures) and correct (i.e., compliant with specifications) concurrent programs that do not sacrifice efficiency. On the technical side, dramatic advances in the development of verification tools, including proof assistants, automatic theorem provers and model checkers, have made verification tools usable after minimal training and integrated into modern IDEs. The project aims at applying these language-based verification technologies to emerging issues in concurrent/parallel programming. In the project, new concurrency language primitives will be scrutinized and the results will be formalized in proof assistants. Coinductive methods will be used to develop program logics for concurrency that can explicitly deal with particular behaviours of program runs, such as nontermination, input/output and nondeterminism. Type-based compositional program analyses will be derived from these logics, in order to investigate interplay between different analyses in a unifying framework in anticipation of "pluggable" program analyses. As an application of these foundational works, the project also studies a dynamic module system with asynchronous module loading.
Arendasime kompilaatori hajusarvutamiseks mõeldud konkurentsest objektorienteeritud keelest ABS Scala keelde, mis on sekventsiaalne objektorienteeritust ja funktsionaalsust kombineeriv programeerimiskeel. Meie kompileerimisskeem kasutab Agda jätkude mehhanismi ja aktorite teeki Akka. Kompilaator toetab koodi hajuskäivitamist paljudel protsessoritel. Abstraheerides kummastki keelest välja idealiseeritud tuumkeele tõestasime, et meie kompilaator on semantikat säilitav ja formaliseerime osad sellest tõestusest tõestussassistendiga Agda. Arendasime MLi moodulite süsteemile sarnase moodulite süsteemi ABS keelele. Töötasime välja tüübisüsteemi MLi-laadsele keelele, mis ühekorraga toetab rekursiivseid tüüpe, tüübiparameetreid ja abstraktseid tüüpe. Selleks läks vaja mittetriviaalset definitsiooni ja mittetriviaalset kontrolli. Lahendasime probleemi kasutades kombineeritud induktiivset ja koinduktiivset lähenemist. Uurisime jätkude semantikat call-by-need väärtustamise kontekstis võrreldes sekventsiarvutusel põhinevat lähenemist, kus juhtimine on eksplitsiitne, teisega lähenemisega, mis põhineb jätkuedastusstiili teisendusel. Näitasime, et need kaks lähenemist viivad erinevate semantikateni. Võrdlesime piiritletud jätkude ja lahtise induktsiooni võimsust. Uurisime lahtise induktsiooni arvutuslikku interpretatsiooni Cantori ruumis. Kasutasime rakuautomaate funktsionaalprogrammeerimise keele ja tõestusassistendi Agda võimaluste ja piiride uurimiseks, formaliseerides selles mittetrivaalse fragmendi ühedimensiooniliste rakuautomaatide teooriat. Tõime sisse rakuautomaatide uue omaduse, mis on tugevdab sürjektiivsust. Näitasime, et koos teatud teise (eelinjektiivsuse) omadusega garanteerib nn järelsürjektiivsus pöördrakuautomaadi olemasolu, ning formuleerisime duaalse versiooni kauasest kinnitamata hüpoteesist.