Dmytro Traytel

Projekttitel

Discover: Distributed Streaming Computations, Verified

Hvad handler dit projekt om?

Moderne it-systemer producerer enorme mængder af data. Såkaldte “stream processing frameworks" er vigtige værktøjer, der sørger for, at tusindvis af softwareudviklere og data scientists kan tæmme og udnytte disse data. Disse frameworks kommer med praktiske programmeringsabstraktioner, der giver deres brugere mulighed for at udtrykke den ønskede dataanalyse. På trods af deres succes er modne stream processing frameworks som Apache Flink eller Google Cloud Dataflow enorme og traditionelt udviklede softwaresystemer: de har tusindvis af kendte fejl, der bringer deres tilgængelighed i fare eller kan forårsage tab af data. Vi vil i dette projekt udvikle et nyt, effektivt, udtryksfuldt og troværdigt stream processing framework. For at give det højeste niveau af troværdighed vil vi bruge en bevisassistent til at designe og implementere frameworket og til at bevise dets korrekthed.

Hvordan opstod din interesse for dit forskningsfelt?

Bevisassistenter er vidunderlige softwareværktøjer. De tjekker omhyggeligt menneskeskrevne matematiske beviser og hjælpe deres brugere med at konstruere disse beviser. De bruges i dag til at verificere dybe matematiske resultater og meget kritiske software, som ikke kan tolererer korrekthedsfejl. Mit første møde med den populære Isabelle bevisassistent skete under min B.Sc. uddanelse på TU München. Jeg blev "afhængig" kort efter og er Isabelle-udvikler og Isabelle-bruger i dag. Disse aktiviteter udføres tit af forskellige forskere, men de er i høj grad symbiotiske. At være bruger lader mig finde ud af, hvor godt bevisassistenter fungerer, og giver inspiration til nye funktioner. Og at forstå hvordan bevisassistenten arbejder "under motorhjelmen", hjælper mig med at bruge den effektivt.

Hvad er de forskningsmæssige udfordringer og perspektiver ved dit projekt?

Udvikling af distribuerede streamingalgoritmer, der kan køres i datacentre for at forbedre skalerbarheden er udfordrende. Beviset for at sådanne algoritmer gør, hvad de skal, er i endnu højere grad udfordrende. Og at skulle overbevise en bevisassistent om gyldigheden af korrekthedsbeviset gør bestemt ikke opgaven nemmere. Men der er håb: stream processing frameworks håndhæver en programstruktur, der har en høj grad af parallelitet. Algoritmer udtrykt ved hjælp af sådanne frameworks kan således distribueres naturligt, mens programmøren for det meste har illusionen af at arbejde med en ikke-distribueret beregning. Den centrale forskningshypotese for DISCOVER er, at det samme gælder for korrekthedsbeviser: beviser for en ikke-distribueret beregning kan overføres til det distribuerede miljø.

Hvilke perspektiver vurderer du selv, at din forskning på sigt kan have for det omgivende samfund?

DISCOVER vil producere det første formelt verificerede system til pålidelig analyse af store mængder af data. De stærke korrekthedsgarantier muliggør brugen af den udviklede stream processing framework i sikkerheds- eller forretningskritiske scenarier, der ikke kan tolerere fejl i resultaterne af dataanalyse. Derudover er målet med DISCOVER at gøre det nemmere for brugerne at bevise korrektheden af de applikationer, der er udviklet ved hjælp af frameworket. Så projektet vil give det nødvendige solide grundlag for softwareudviklere og data scientists arbejde og derved bidrage til den bredere brug af bevisassistentteknologi.

Hvad vil det betyde for din forskerkarriere, at du indgår i Sapere Aude-programmet?

Den generøse DFF-finansiering vil på kort sigt give mig mulighed for at fokusere på et ambitiøst, åbent forskningsspørgsmål, frem for at plukke lavthængende frugter. Sapere Aude bevillingen vil på lang sigt hjælpe mig med at konsolidere min position som forskningsleder inden for forskningsområdet "interactive theorem proving", videnskaben om bevisassistenter. Med dette projekt går jeg også ind i et nyt forskningsområde, "data stream processing", som jeg hidtil kun er stødt på i min forskning fra en brugers perspektiv. Min ambition for DISCOVER er at ændre måden, hvorpå man tænker på korrekthed på dette forskningsområde, hvilket minder om den dybe indvirkning det første formelt verificerede operativ system, seL4, havde på forskning i operativsystemer.

Lidt om mennesket bag forskeren

Jeg er født i Kharkiv i Ukraine og voksede op, studerede og tog min ph.d. i München i Tyskland. Efter en fem års ophold som postdoc i Zürich, Schweiz, flyttede jeg til København, lige i mellem to Covid-bølger. Når jeg ikke er på jagt efter den næste "qed" med Isabelle, nyder jeg at cykle og spille brætspil. I weekenderne kan man ofte finde mig sammen med min søn og kone på Bastard Café, vores yndlingssted i København.