Declarative Networking: Models and Conjectures

Abstract

Deze thesis gaat over declarative networking, een onderzoeksgebied waarin men gedistribueerde programma’s implementeert met beschrijvende talen zoals Datalog [2], waarin men voornamelijk specificeert wat de uitvoer is, en niet zozeer hoe deze uitvoer moet berekend worden. Het voordeel van zulke talen is dat complexe algoritmen kunnen beschreven worden met redelijk korte programma’s [45, 37]. Ter vergelijking, om gegevensbanken te ondervragen gebruikt men standaard de beschrijvende taal SQL in plaats van een imperatieve programmeertaal zoals Java, omdat men voor deze toepassing vaak veel kortere en overzichtelijkere programma’s kan schrijven in SQL. In deze thesis gebruiken we twee bestaande modellen. Het eerste model bestaat uit relational transducers [7, 28, 29, 30, 54]; deze stellen een abstracte computer voor. Wij definiëren zelf netwerken van zulke relational transducers. Het tweede model wordt gevormd door de taal Dedalus [13, 14, 37]; dit is een programmeertaal geïnspireerd door Datalog. Wij veronderstellen in beide modellen dat een netwerk willekeurige vertragingen kan veroorzaken tussen het versturen en aankomen van boodschappen; dit is de zogenaamde asynchrone communicatie zoals typisch voorkomt op het Internet.

Declarative networking is a field in which people implement distributed protocols and applications in high-level declarative languages like Datalog. Such a declarative formalism is believed to help the programmer express complex distributed computations with relatively few lines of code. In this thesis, we investigate many different aspects of declarative networking. The model of networked relational transducers is one main topic, for which we investigate the expressivity; the link between expressivity and distributed coordination; and, the decidability of eventual consistency. Another important topic consists of the language Dedalus, a Datalog-inspired language, for which we define a purely declarative semantics. We also show how this semantics can be used to reason about distributed message causality.