Fast and Correct Round Elimination

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.