Till innehåll på sidan

Language-based Approaches to Safe and Efficient Distributed Programming

Tid: Ti 2021-02-23 kl 08.30

Plats: F3, Lindstedtsvägen 26, Stockholm (English)

Ämnesområde: Datalogi

Respondent: Xin Zhao , Teoretisk datalogi, TCS

Opponent: Professor Wolfgang De Meuter, Vrije Universiteit Brussel

Handledare: Philipp Haller, Teoretisk datalogi, TCS; Roberto Guanciale, Teoretisk datalogi, TCS

Abstract

Distribuerade system möter den växande efterfrågan på snabb tillgång till resurser och feltolerans för data. Hög konsistens säkerställer att alla klienter observerar konsistenta datauppdateringar atomiskt på alla servrar i ett distribuerat system, och det används ofta i system som relationsdatabaser. Vid synkronisering är dock data otillgängligt. På grund av prestandakrav måste därför mjukvaruutvecklare offra konsistens för prestanda. För det första saknas en omfattande förståelse för hur man väljer en lämplig konsistensmodell. För det andra, konsistensgarantier för specifik data kan försvagas om applikationers korrekthet inte påverkas, men att resonera om korrektheten vid blandad användning av data med olika konsistens är svårt. För det tredje, för en operationssekvens som en transaktion, komplicerar samexistensen av data med blandad konsistens resonemanget om riktigheten i implementeringen.

Denna avhandling undersöker hur man kan hjälpa distribuerade mjukvaruutvecklare av system med blandad konsistens genom språkbaserade metoder. Först föreslår vi ett nytt konsistensprotokoll, det observerbara atomiska konsistensprotokollet (OACP), för att göra skrivdominerande applikationer så snabba som möjligt och så konsistenta som behövs. OACP kombinerar fördelarna med (1) sammansättningsbara datatyper, specifikt konvergerade replikerade datatyper, för att minska synkronisering och (2) tillförlitlig överföring, för att förse hög konsistens när så är nödvändigt. Vi har också ett abstrakt programmeringsgränssnitt för att förbättra effektiviteten och noggrannheten för distribuerad programmering.

För det andra föreslår vi gitterbaserade replikeringsdatakonsistenstyper (CTRD), ett statiskt konsistenstypat språk av högre ordning med replikerade datatyper. CTRD-typsystemet stöder delad data mellan flera klienter och utför statisk icke-störning mellan datatyper med lägre konsistens och datatyper med högre konsistens. Språket kan tillämpas på många distribuerade applikationer och garanterar att uppdatering av data med låg konsistens aldrig påverkar data med hög konsistens.

Slutligen presenterar vi en typbaserad metod för statisk verifiering av transaktioners korrekthet. En standardegenskap för korrekthet är serialiserbarhet, vilket innebär att den utförda exekveringen av transaktioner motsvarar en sekventiell exekvering där instruktionerna för transaktioner inte är sammanflätade med instruktioner från andra transaktioner. Vi formaliserar ett informationsflödessystem, SerialT, för att hålla reda på datakonsistensnivåer och använder isoleringen mellan konsistent och tillgänglig data för att förskjuta tillgängliga operationer inom en transaktion. Dessutom använder vi platsinformation som genereras från typkontroll för att genomdriva transaktionsserialiseringsegenskaper, och vi introducerar också ytterligare två kommutativa åtgärder för att minska onödiga lås.

urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-289461