Akademska 2025/26. godina

Platforme za izvršavanje u oblaku pružaju različite servise (eng. services) korisnicima koristeći razne modele isporuke usluga. Savremena istraživanja ovih modela dovela su do široke primene bezserverskog izvršavanja (eng. serverless), paradigme u kojoj se softver sastoji od funkcija — brzih, ponovno iskoristivih jedinica koda koje se izvršavaju unutar izolovanih, virtualizovanih okruženja. Vodeće platforme za izvršavanje u oblaku, uključujući Amazon Web Services (AWS), Microsoft Azure i Google Cloud, izveštavaju da značajan deo njihovih korisnika koristi bezserverska rešenja.

Većina pružalaca servisa izvršavanja u oblaku primenjuje model naplate po principu „plati koliko koristiš”. Neefikasno korišćenje računarskih resursa, naročito procesorskih jezgara i radne memorije, koji predstavljaju dva najskuplja resursa, dovodi do značajnog povećanja troškova. Dodatno, potreba za virtualizacijom negativno utiče na vreme inicijalizacije i povećava potrošnju procesorskog vremena i radne memorije. Izolovana bezserverska okruženja se tipično implementiraju nad okruženjima koja zahtevaju velike količine radne memorije, kao na primer virtualne mašine za jezike Java, JavaScript ili Python i odgovarajuci prateći radni okviri.

Savremene arhitekture za izvršavanje u oblaku koriste tehnike snimanja stanja inicijalizovanih okruženja u nastavljivom obliku (eng. Checkpoint/Restore). Ove tehnike omogućavaju optimizaciju iskorišćenja resursa, kao i deljenje koda i podataka između više okruženja za izvršavanje. Međutim, postojeća rešenja funkcionišu u fazi izgradnje aplikacija i, kao takva, ne omogućavaju ranu inicijalizaciju i deljenje podataka koji postaju dostupni u toku izvršavanja aplikacija. Takvi podaci se iznova obrađuju i dupliraju u svakom pojedinačnom izolovanom okruženju za izvršavanje.

Ova disertacija predstavlja Doss, sistem za snimanje i deljenje podataka koji omogućava snimanje i deljenje podataka tokom izvršavanja aplikacije. Doss direktno snima objekte koji sačinjuju podatke, bez njihove transformacije, u obliku ponovno iskoristivih i deljivih snimaka (eng. snapshot). Takav pristup omogućava Doss-u da postigne konstantno vreme deserijalizacije podataka, čime se značajno unapređuje vreme inicijalizacije aplikacija i smanjuje potrošnja računarskih resursa. Arhitektura sistema Doss omogućava deljenje snimaka između više instanci aplikacije, čime se eliminiše memorijsko zauzeće povezano sa ponovnom obradom i dupliranjem podataka i poboljšava vreme inicijalizacije aplikacije.

Implementacija sistema Doss, pod nazivom GraalDoss, realizovana je u programskom jeziku Java i integrisana u ekosistem GraalVM. GraalDoss je evaluiran pomoću 106 testova korektnosti i robustnosti, kao i korišćenjem novog skupa referentnih programa namenjenih testiranju aplikacija u oblaku. Rezultati evaluacije pokazuju konzistentno vreme deserijalizacije, uz brzinu serijalizacije uporedivu sa savremenim Java bibliotekama za JSON i binarnu serijalizaciju. U mikroservisnim veb aplikacijama, GraalDoss eliminiše memorijsko zauzeće privremenih skladišta podataka deljenjem snimaka popunjenih skladišta između instanci mikroservisa, čime se postiže povećanje odnosa brzine i memorijeskog zauzeća sistema od 41% za osam instanci mikroservisa, uz smanjenje vremena odziva aplikacije od 34%. U aplikacijama koje koriste obradu prirodnih jezika, GraalDoss unapređuje vreme izvršavanja za šest redova veličine snimanjem modela za obradu teksta i rezultata njegove primene na ulazni tekst.

Cloud-computing platforms provide services to consumers through multiple service-delivery models. Recent advances in these models have led to the emergence of serverless computing, or simply serverless, a paradigm in which software systems are composed of functions - reusable, lightweight units of code executed within isolated sandboxed environments. Major cloud-computing platforms, including Amazon Web Services (AWS), Microsoft Azure, and Google Cloud, report that a substantial proportion of their customers employ serverless solutions.

Most cloud-computing providers employ a pay-as-you-go billing model. Inefficient utilization of computing resources, particularly CPU time and working memory, which constitute the most costly resources, leads to increased overall operational costs. Moreover, the requirement for sandboxing adversely affects initialization latency and results in additional CPU and working-memory overhead. Serverless sandboxes are typically deployed on top of heavyweight virtualization stacks, further increasing working-memory consumption.

Modern cloud-computing architectures use Checkpoint/Restore techniques to freeze initialized sandboxes into a continuable form. Such techniques, in combination with cloud-native deployments, allow the virtualized environment to optimize resource consumption and share code and pre-initialized data across multiple sandboxes. However, such solutions operate at application-build time and cannot pre-initialize and share data available during application execution. Such data is processed multiple times and duplicated in each sandbox.

This dissertation presents Doss, a direct object snapshotting and sharing system that performs data c/r during application execution. Doss persists data directly, without transformations, into reusable and shareable snapshots. Direct snapshotting allows Doss to achieve near-constant data deserialization, greatly improving initialization times and reducing CPU usage. Doss architecture enables snapshot sharing across application instances, eliminating the excess memory footprint associated with data re-processing and duplication.

GraalDoss, a Doss implementation for Java, is integrated into the GraalVM ecosystem. GraalDoss is evaluated using 106 correctness and robustness tests and a novel set of cloud-native micro and macro benchmarks that exercise real-world scenarios. A comprehensive evaluation of GraalDoss shows a consistent near-constant data-deserialization overhead with serialization times comparable to state-of-the-art Java JSON and binary serialization libraries. GraalDoss eliminates the memory footprint of web API microservice caches by sharing populated cache snapshots across microservice instances, improving the overall density by 41% for 8 microservice instances and improving first-response times by 34%. In NLP applications, GraalDoss improves the pipeline execution times by six orders of magnitude by snapshotting pipeline results and subsequently loading the snapshots.

Žirovektorski prostori predstavljaju algebarske strukture koje opisuju hiperboličku geometriju na isti način na koji vektorski prostori opisuju Euklidsku geometriju. Iako same operacije žirovektorskih prostora nisu ni komutativne ni asocijativne, uvođenje pojmova žirokomutativnosti i žiroasocijativnosti obezbeđuje stabilan okvir unutar koga se fundamentalne teoreme mogu formulisati u obliku koji je sintaksno i strukturno veoma blizak euklidskim analogonima. Ova paralela ne samo da olakšava razumevanje hiperboličkih konstrukcija, već otvara i mogućnosti za primenu klasičnih algebarskih metoda u novom, hiperboličkom kontekstu.

Ajnštajnovo sabiranje brzina nije komutativno ni asocijativno kao sabiranje brzina u klasičnoj mehanici. Međutim, jeste žirokomutativno i žiroasocijativno (na način na koji su ova svojstva i opisana, dodavanjem specifičnog korekcionog faktora koji u ovom slučaju nije apstraktni pojam, već izraz koji modeluje relativističke efekte – tzv. Tomasovu precesiju) i dovodi do izgradnje Ajnštajnovog žirovektorskog prostora, koji, kako je formalno pokazano u ovoj disertaciji, zadovoljava aksiome Tarskog i negaciju aksiome paralelnosti, tj. modeluje hiperboličku geometriju.

Predmet ove disertacije je formalna verifikacija svojstava žirovektorskih prostora i njihove generalizacije normiranih žirolinearnih prostora u dokazivaču teorema Isabelle/HOL. Kroz formalnu verifikaciju dolazi se često do otkrivanja previda u dokazima pisanim rukom – bilo da su oni neispravna tvrđenja ili tvrđenja koja se moraju dopuniti određenim pretpostavkama da bi bila ispravna – ali i do otkrivanja novih teorema. Sa razvojem interaktivnih dokazivača teorema (Isabelle/HOL, Lean, Coq, itd.) formalizacija postaje sve važnija u matematici i njen cilj je da se gradi “digitalna biblioteka” matematike, gde je svaka lema i teorema proverena do najsitnijeg detalja. Za mlade oblasti kao što je “žiromatematika”, formalizacija donosi poverenje da će se budući radovi nadovezivati na čvrst temelj, bez bojazni da se oslanjaju na neproverene algebarske manipulacije.

Posebna pažnja u disertaciji posvećena je formalizaciji dva centralna planarna žirovektorska prostora: Mebijusovog, inspirisanog hiperboličkom geometrijom, i Ajnštajnovog, zasnovanog na specijalnoj teoriji relativiteta. Njihova izomorfnost je ne samo matematički dokazana već i potpuno formalno verifikovana u Isabelle/HOL, što predstavlja značajan doprinos jer su ti dokazi u literaturi bili izostavljeni zbog složene algebarske prirode. Dodatno, dopunjena je i u potpunosti formalizovana teorema o žiroizomorfizmu, kojom se potvrđuje da je svaka struktura izomorfna žirovektorskom prostoru takođe žirovektorski prostor, čime je ova oblast dobila potpuniju i pouzdaniju teorijsku osnovu, ali i efikasniji način utvrđivanja da li neka struktura zadovoljava aksiome žirovektorskog prostora.

Dalje, formalno je dokazano da je Mebijusov žirovektorski prostor ekvivalentan Poinkareovom disk modelu, a u ranijim radovima je pokazano da je Poinkareov disk model model hiperboličke geometrije, što znači da je i Mebijusov žirovektorski prostor model hiperboličke geometrije. Time je razvijen novi formalni model Poinkareovog diska unutar Isabelle/HOL, koji je sintaksno znatno jednostavniji od klasičnih pristupa zasnovanih na projektivnoj geometriji, pa samim tim pogodniji za buduću upotrebu u verifikaciji složenijih geometrijskih teorija. Konačno, u ovom okviru formalno su rekonstruisane i verifikovane žirovektorske verzije poznatih geometrijskih rezultata, poput Pitagorine i kosinusne teoreme, čime je demonstrirana primenljivost razvijenog formalizma.

Svi iznad pomenuti rezultati su publikovani. Od nepublikovanih rezultata značajno je pomenuti da je u Isabelle/HOL postavljena dobra osnova za formalnu verifikaciju dokaza Mazur-Ulamove teoreme u slučaju normiranih žirolinearnih prostora i da je u jednom od dokaza same teoreme otkriven previd – deo koji potencijalno nije ispravan ili nije ispravan bez dodatnih uslova. Drugi potencijalni pravci rada su uopštenje na 3D slučaj i formalizacija teorema koje govore o vezi žirovektorskih i normiranih žirolinearnih prostora, kao i formalni dokaz njihovih mnogih topoloških i metričkih svojstava.