Fast and Correct Round Elimination

Loading...
Thumbnail Image
Journal Title
Journal ISSN
Volume Title
Perustieteiden korkeakoulu | Master's thesis
Date
2022-07-29
Department
Major/Subject
Computer Science
Mcode
SCI3042
Degree programme
Master’s Programme in Computer, Communication and Information Sciences
Language
en
Pages
51
Series
Abstract
Round elimination is a process used to study the hardness of distributed graph problems. It is available as a computer program. Optimizations to the program have permitted the study of more complex problems. Because no fast algorithm for checking the result of round elimination is known, it must be implemented correctly. In this thesis I present a new algorithm for maximization, the most computationally expensive part of the original Round Eliminator, prove that the new algorithm is asymptotically faster and formally verify the theory behind it in Coq along with a program that checks maximization results using the new algorithm. An implementation based on the new algorithm makes round elimination orders of magnitude faster in practice. Unfortunately, the verified checker is too slow for practical use but that is not a fundamental limitation, only a flaw in the particular way it was written.

Kierroseliminaatio on menetelmä, jota käytetään hajautettujen verkko-ongelmien aikavaativuuden tutkimiseen. Siitä tehdyn tietokonetoteutuksen optimoiminen on mahdollistanut yhä mutkikkaampien ongelmien tutkimisen. Koska kierroseliminaation tuloksen tarkistamiseen ei tunneta nopeaa algoritmia, on hyvin tärkeää, että kierroseliminaatio on toteutettu oikein. Esittelen tässä työssä uuden algoritmin kierroseliminaation hitaimpaan osaan, maksimointiin. Osoitan, että uuden algoritmin aikavaativuus on vanhaa parempi ja todistan Coqilla-teorian, johon se perustuu sekä ohjelman kierroseliminaation tuloksen tarkistamiseen. Käytännössä uutta algoritmia hyödyntävä toteutus kierroseliminaatiosta on yli tuhat kertaa vanhaa nopeampi. Valitettavasti todistettu kierroseliminaation tarkistaja on liian hidas ollakseen hyödyllinen, mutta tämä vika on korjattavissa.
Description
Supervisor
Suomela, Jukka
Thesis advisor
Suomela, Jukka
Keywords
round elimination, Coq, distributed algorithms, formal proof, optimization, locally checkable labeling
Other note
Citation