Seminar Katedre za računarstvo i informatiku

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.

Proteini su linearni polimeri izgrađeni od aminokiselina, čiji redosled definiše njihovu prostornu strukturu i biološku funkciju. Iako mnogi proteini usvajaju stabilnu trodimenzionalnu konformaciju, značajan broj proteina ili njihovih delova ostaje delimično ili potpuno neuređen, bez fiksne 3D strukture. Neuređeni delovi proteina predstavljaju izazov za savremene metode predviđanja strukture, ali su istovremeno ključni za razumevanje regulatornih i interaktivnih funkcija u ćelijskim procesima. Trenutni modeli, uključujući različite vrste strukturnih alfabeta kao i AlphaFold program, imaju ograničenu preciznost u ovim regionima, što otvara prostor za dalja istraživanja.

Predlog teme doktorske teze obuhvata istraživanje neuređenih regiona u proteinima i njihovog neposrednog okruženja, kao i razvoj metoda za njihovu precizniju prostornu karakterizaciju. Imajući u vidu da neuređeni proteini (IDP) i njihovi regioni predstavljaju važan biološki fenomen sa značajnom ulogom u regulaciji, signalizaciji i patogenezi, ali da su slabo obuhvaćeni klasičnim modelima u kojima se predviđa struktura, istraživanje će biti usmereno na poboljšanje njihovog strukturnog opisa korišćenjem računarskih metoda.

Biće razvijen model koji kombinuje, za proteine iz DisProt baze, informacije dobijene iz strukturnog alfabeta Protein Blocks, predviđene 3D strukture iz AlphaFold programa, kao i dodatne osobine poput prisustva strukturnih ponovaka i fluktuirajućih granica između uređenih i neuređenih delova. Model će biti treniran i testiran na skupu proteina iz DisProt baze, koji sadrži eksperimentalno utvrđene neuređene regione. Na osnovu formiranog modela biće razvijen i meta-prediktor za određivanje neuređenih regiona proteina. Istraživanje će uključiti primenu različitih metoda istraživanja podataka u cilju pronalaženja karakterističnih obrazaca i prelaznih zona između strukturno različitih regiona proteina.

Očekivani rezultati obuhvataju poboljšanje pouzdanosti predviđanja neuređenih delova proteina i bolju definiciju njihovog trodimenzionalnog konteksta. Pored toga, očekuje se identifikacija strukturnih obrazaca koji mogu poslužiti za funkcionalnu karakterizaciju ovih regiona. Razvijen model i rezultati biće provereni upoređivanjem sa postojećim programima za predviđanje neuređenih regiona.

Доминацијски проблеми на графовима припадају класи НП тешких проблема и интензивно су проучавани, како теоријски, тако и практично, пре свега због њихове широке примене у областима као што су друштвене мреже, биоинформатика, рутирање у мрежама и истраживање података на графовима. Предлог теме докторске тезе обухвата развој метода за ефикасно решавање различитих варијанти доминацијских проблема, са посебном пажњом усмереном на графове великих димензија. Биће решавани следећи проблеми: проблем минималне тежинске тоталне доминације (MWTDS), минималне тежинске независне доминације (MWIDS), к јаке римске доминације (KSRDS), као и основни проблем минималне доминације (MDS). За проблем MWTDS биће развијена метода променљивих околина (VNS) уз инкрементално рачунање функције прилагођености. Биће предложена примена на убрзавање ширења информација на друштвеним мрежама. Код MWIDS проблема је планиран развој два ILP модела и похлепног алгоритма. Проблем KSRDS ће бити решаван применом VNS-а уз статистички приступ провере квазидопустивости на великим инстанцама. Биће предложена примена проблема у оптимизацији распореда ватрогасних ресурса. Код MDS проблема биће развијени хибридни алгоритми засновани на комбинацији различитих приступа међу којима су: проналажење заједница у графовима, ILP модели, пристрасна локална претрага, уз могућност унапређења коришћењем метода машинског учења. Очекивани резултати обухватају побољшање најбољих познатих резултата на разматраним проблемима, поготово на инстанцама великих димензија, као и предлог оригиналних примена. Сви алгоритми ће бити темељно упоређени са резултатима из литературе на постојећим (енг. benchmark) и новоуведеним скуповима инстанци, уз одговарајућу статистичку анализу.

Optimizacije vođene profilima (eng. profiile-guided optimizations) značajno doprinose generisanju efikasnih programa. Profili programa su informacije o izvršavanju programa, na primer broj izvršavanja grana u naredbama grananja, broj poziva funkcija, verovatnoće poziva virtuelnih metoda i slično. Dinamičko profajliranje je standardni način za prikupljanje profila, pokretanjem programa i praćenjem načina na koji se on izvršava. Dinamičkim profjaliranjem prikupljaju se precizni profili, ali je dinamičko prikupljanje profila često vremenski i memorijski zahtevno, kompikuje proces generisanja optimizovanih programa i zahteva odgovarajuće reprezentativne ulaze koje je često veoma izazovno pronaći. Alternativa dinamičkim profajlerima jesu statički profajleri. Statički profajleri predviđaju profile izvršavanja programa bez pokretanja programa, na osnovu statičkih atributa kojima se opisuju delovi progama.

Predlog teme doktorske teze obuhvata razvoj stačkog profjalera GraalSP zasnovanog na tehnikama mašinskog učenja. GraalSP koristi grafovsku međureprezentaciju visokog nivoa za definisanje atributa kojima se karakterišu delovi programa. Uz to, GraalSP polu-automatizuje proces definisanja ovih atributa. GraalSP podržava sve programske jezike koji se kompajliraju na Java bajtkod, na primer jezike Java, Scala i Kotlin. Za predviđanje profila, eksperimentisano je sa različitim modleima mašinskog učenja i najbolji rezultati su dobijeni korišćenjem XGBoost modela koji je zasnovan na stablima odlučivanja koji je stoga i integrisan u GraalSP. Pored toga, GraalSP koristi i dodatne heuristike za korekciju predviđenih profila kako bi korigovao neprecizna predviđanja modela koja mogu biti rezultat odudarajućih podataka (eng. outliers) i voditi do degradacije performansi. GraalSP je implementiran i integrisan u kompajler GraalVM Native Image, čime je ostvareno ubrzavanje vremena izvršavanja programa koji se prevode korišćenjem ovog kompajlera za 7.46% u poređenju sa podrazumevanom konfiguracijom kompajlera.