Design and Analysis of Transport Protocols for Reliable High-Speed Communications
András Oláh · 1997
In the thesis we study three different data transfer protocols.The usage of timestamps in data transfer protocols is analyzed in detail through the example of the PAWS mechanism which was proposed as an extension to TCP.The analysis reveals that the use of timestamps increases the functionality of the transport protocol by facilitating the simple measurement of round-trip delays, but it also reduces the maximum allowable transmission rate as compared to the plain sliding-window protocol.Another data transfer protocol called SNR is analyzed which is based on the idea of periodic state exchange.We start from an earlier specification of SNR and compare it to the plain sliding-window protocol.The analysis reveals that the maximum transmission speed achievable by that SNR specification is higher than that of the plain sliding-window protocol, but it comes with a serious limitation.In the SNR specification it is assumed that no duplicates are generated by either the network or the transport protocol itself.This assumption may seriously limit the effective performance of the protocol in case of losses in the network and demonstrates the importance of considering all the assumptions when selecting a protocol for a certain environment.The use of timestamps is also investigated in the context of connection management protocols.The detailed analysis of the connection setup protocol SCMP is presented which is based on the assumption that clocks of computers can be synchronized relatively cheaply even in a large network.In our verification it is proven that the safety of the protocol does not depend of the synchronization assumption, therefore the protocol can be used safely in cases when there are no absolute guarantees of the clocks being synchronized.Since practical clock synchronization algorithms give only probabilistic guarantees, our result provides an important theoretical support of the applicability of the protocol in practical environments.Based on earlier work by others, a family of connection management protocols is analyzed that use a cache to store information needed to shorten the connection setup latency.We contribute to this work by proposing improvements which allow to reduce considerably the memory usage of these protocols.Furthermore, we show that the correctness of the protocol can be assured without assuming an upper bound on the incarnation lifetime, i.e., the maximum duration of a connection.This result greatly improves the practical applicability of the protocol. SamenvattingHet onderwerp van deze dissertatie is het ontwerpen en analyseren van transportprotocollen voor betrouwbare communicatie.Deze transportprotocollen garanderen het volledig en in de juiste volgorde afleveren van gebruikersdata door netwerken die pakketten kunnen verliezen, dupliceren of van volgorde verwisselen.Zulke betrouwbare diensten worden vereist in een breed scala aan toepassingen zoals het "Worldwide Web", gedistribueerd rekenen en toegang tot "remote" netwerken.Het ontwerpen van deze protocollen is in grote mate afhankelijk van de parameters van de infrastructuur van het betreffende netwerk en de gemaakte aannames over de aangesloten computers en gebruikte toepassingen.Zo heeft de recente vooruitgang in optische transmissie en computertechnologie geleid tot menige nieuwe transportprotocollen. Vele van deze maken gebruik van verwante technieken.Het doel van dit proefschrift is het vergroten van het inzicht in betrouwbare communicatie door de analyse van de protocollen en bij te dragen tot het ontwerp van betrouwbare protocollen.De formele specificatie en verificatie van de onderzochte protocolmechanismen vormt de basis van de analyse.Het gedrag van het protocol wordt beschreven door een toestandsovergangssysteem, waaruit door middel van "assertional reasoning" eigenschappen worden afgeleid.Binnen dit model kan er met onbegrensde en modulo-N toestandsvariabelen worden gewerkt en bovendien kunnen "real-time" aspecten van protocollen meegenomen worden.Dit is essentieel voor het modelleren van realistische systemen.In dit proefschrift worden practische protocollen van aanzienlijke complexiteit gespecificeerd en geverifieerd.Een voordeel van formele verificatie is dat zij het geloof in de correctheid van de protocollen vergroot.Het gebruik van een formalisme dwingt af dat alle details van de werking van het protocol duidelijk worden en dat alle veronderstellingen betreffende het protocol en zijn omgeving expliciet worden gemaakt.Bovendien wordt tijdens de verificatie het inzicht in het protocol vergroot.Het belangrijkste resultaat is misschien wel dat de voorwaarden voor de correctheid van het protocol uitgedrukt blijken te kunnen worden in ongelijkheden in enkele protocolparameters.Deze voorwaarden maken het mogelijk dat verschillende protocolmechanismes kunnen worden vergeleken en gebruikt kunnen worden om de geschiktheid van een protocol voor een bepaalde omgeving te beoordelen.De functionaliteit van transportprotocollen kan op een natuurlijke manier verdeeld woriii iv Samenvatting den in dataoverdracht en connectiemanagement.Dataoverdracht betreft het op volgorde afleveren van gebruikersdata terwijl connectiemanagement te maken heeft met het ordentelijk opzetten en weer afbreken van een verbinding.Drie dataoverdrachtsprotocollen worden in dit proefschrift bestudeerd.Het gebruik van "timestamps" in deze protocollen wordt in detail geanalyseerd aan de hand van het PAWS-mechanisme dat als uitbreiding van TCP is voorgesteld.Uit die analyse komt naar voren dat het gebruik van timestamps de functionaliteit van het protocol vergroot door het vergemakkelijken van het meten van een "round-trip" vertraging.De maximaal toegestane transmissiesnelheid wordt echter verkleind in vergelijking met een gewone "sliding-window" protocol.Een ander protocol, SNR, dat op het periodiek uitwisselen van toestanden is gebaseerd, wordt ook geanalyseerd.Eerst wordt een eerdere versie van SNR bekeken en vergeleken met een gewoon sliding-window protocol.Het resultaat van de analyse is dat de maximaal haalbare transmissiesnelheid van die SNR-versie hoger is dan het sliding-window protocol.Dit gaat echter samen met een ernstige beperking.De SNR-specificatie gaat er namelijk van uit dat noch het netwerk-noch het transportprotocol duplicaten genereert.Deze aanname zou de prestatie van het protocol in het geval van verliezen in het netwerk ernstig kunnen beperken, wat het belang aantoont van het meenemen van alle veronderstellingen bij de selectie van een protocol voor een bepaalde omgeving.Het gebruik van timestamps wordt ook in de context van connectiemanagement protocollen onderzocht.Er wordt een gedetailleerde analyse van het opzetten van een verbinding in SCMP gepresenteerd.Het mechanisme veronderstelt dat de klokken van computers zelfs in een groot netwerk op een relatief goedkope wijze gesynchroniseerd kunnen worden.De verificatie toont aan dat de betrouwbaarheid van het protocol niet van deze veronderstelling afhangt en dat het protocol dus ook gebruikt kan worden in omgevingen waarin de mogelijkheid om klokken te synchroniseren niet absoluut gegarandeerd is.Gegeven het feit dat zo'n garantie praktisch niet te geven is, biedt dit resultaat een theoretische ondersteuning van het protocol in een praktische omgeving.Uitgaande van eerder door anderen uitgevoerde analyses, wordt, ten slotte, een familie van connectiemanagement protocollen onderzocht.Deze familie wordt gekenmerkt door het feit dat de protocollen gebruik maken van een cache voor de opslag van informatie om zo de vertraging bij het opzetten van een verbinding te verkorten.De bijdrage van dit proefschrift hieraan betreft verbeteringen die tot een aanzienlijke vermindering van het geheugengebruik leiden.Bovendien wordt aangetoond dat de correctheid van het protocol kan worden gegarandeerd zonder te veronderstellen dat de maximale duur van een verbinding een bovengrens heeft.Ook dit resultaat vergroot de praktische toepasbaarheid van het protocol in sterke mate.