Transmission Control Protocol

Video thumbnail (Frame 0) Video thumbnail (Frame 1553) Video thumbnail (Frame 2517) Video thumbnail (Frame 3532) Video thumbnail (Frame 5732) Video thumbnail (Frame 6646) Video thumbnail (Frame 8895) Video thumbnail (Frame 9682) Video thumbnail (Frame 10527) Video thumbnail (Frame 12097) Video thumbnail (Frame 15153) Video thumbnail (Frame 16681) Video thumbnail (Frame 17439) Video thumbnail (Frame 23119) Video thumbnail (Frame 24395) Video thumbnail (Frame 26425) Video thumbnail (Frame 29226) Video thumbnail (Frame 31868) Video thumbnail (Frame 36298) Video thumbnail (Frame 37951) Video thumbnail (Frame 42243) Video thumbnail (Frame 43028) Video thumbnail (Frame 48493) Video thumbnail (Frame 50117) Video thumbnail (Frame 51775) Video thumbnail (Frame 52715) Video thumbnail (Frame 53514) Video thumbnail (Frame 54476) Video thumbnail (Frame 55602) Video thumbnail (Frame 56624) Video thumbnail (Frame 57850)
Video in TIB AV-Portal: Transmission Control Protocol

Formal Metadata

Title
Transmission Control Protocol
Subtitle
TCP/IP basics
Title of Series
Author
License
CC Attribution 4.0 International:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
2018
Language
English

Content Metadata

Subject Area
Abstract
TCP/IP is the most widely used protocol on the Internet for transmitting data. But how does it work in detail? This talk will explain the TCP protocol, from handshake over established to teardown in detail - and elaborate a bit on protocol adjustments over time and congestion control.
Keywords Science

Related Material

Area Programming language Game controller Software Self-organization Musical ensemble Flow separation Communications protocol Information security Data transmission
Suite (music) Game controller Internetworking Website Bit Musical ensemble Client (computing) Communications protocol Data transmission
Laptop Web page Server (computing) Information Server (computing) Bit Web browser Web browser Web 2.0 Software Network topology Website Communications protocol
Laptop Satellite Server (computing) Satellite Link (knot theory) Physicalism Number Connected space Neuroinformatik Internetworking Software Telecommunication Internetworking Arrow of time Musical ensemble Router (computing) Communications protocol Fiber (mathematics) Router (computing)
Laptop Server (computing) Link (knot theory) Satellite Link (knot theory) Local area network Computer network OSI model Internetworking Software Telecommunication Personal digital assistant Router (computing) Local ring Routing Router (computing) Task (computing)
Multiplication Link (knot theory) Link (knot theory) Source code Computer network IP address Connected space OSI model Internetworking Software Hypermedia Internetworking Order (biology) Diagram OSI model Router (computing) Local ring Abstraction Address space Task (computing) Address space
Source code Game controller Overhead (computing) Streaming media Bit Streaming media Data transmission Connected space Category of being Connectivity (graph theory) UDP <Protokoll> Transportschicht UDP <Protokoll> Communications protocol Abstraction
Anwendungsschicht Direct numerical simulation Focus (optics) Transport Layer Security Transport Layer Security Energy level Cartesian coordinate system Computer worm
Laptop Dataflow Server (computing) Group action Link (knot theory) Web browser Web 2.0 Optical disc drive Telecommunication Internetworking Diagram Router (computing) Satellite Link (knot theory) Dataflow Information Cartesian coordinate system Connected space Process (computing) Internetworking Telecommunication Right angle Fiber (mathematics) Router (computing) Laptop Wide area network
Email Link (knot theory) Internetworking Link (knot theory) Internetworking Single-precision floating-point format Multiplication sign Order (biology) Cartesian coordinate system
Greatest element Email Link (knot theory) Dataflow Internetworking Information Personal digital assistant Internetworking Cartesian coordinate system Fiber (mathematics) Computer worm Wide area network
Email Length Multiplication sign Source code IP address Computer programming Computer configuration Flag Information System identification UDP <Protokoll> Error message Source code Email Bit Entire function Type theory Message passing Computer configuration Order (biology) System identification Laptop Server (computing) Game controller Link (knot theory) Field (computer science) Number Product (business) Revision control Internetworking Operator (mathematics) Computer worm Router (computing) Message passing Data type Multiplication Information Uniqueness quantification Length Counting Total S.A. Cartesian coordinate system Timestamp Frame problem Carry (arithmetic) Word ICMP Error message Communications protocol Computer worm Flag Address space
Source code Email Overhead (computing) Email Overhead (computing) Information Length Robot Source code Client (computing) Bit Client (computing) IP address Field (computer science) Entire function Frame problem Computer programming Connected space Programmer (hardware) Network socket Order (biology) UDP <Protokoll> Computer worm
Dataflow Functional (mathematics) Server (computing) Computer file Variety (linguistics) Keyboard shortcut Client (computing) Maxima and minima Bit Client (computing) IP address Frame problem Type theory Latent heat Software Internetworking Network socket Network socket Buffer solution UDP <Protokoll> Family Communications protocol Sinc function Address space
Email Length Source code Automatic differentiation Field (computer science) Number Sequence Computer configuration Synchronization Single-precision floating-point format Flag Computer worm Window Source code Email Bit Sequence Computer configuration Order (biology) Buffer solution Window Spacetime Computer worm Arc (geometry) Flag
Point (geometry) Broadcast programming Server (computing) Functional (mathematics) Socket-Schnittstelle Thread (computing) Computer file Client (computing) Function (mathematics) Streaming media IP address Number Latent heat Network socket Loop (music) Address space Task (computing) Keyboard shortcut Client (computing) System call Flow separation Connected space Loop (music) Network socket Order (biology) Buffer solution Family
Email Source code Email Implementation Server (computing) Information State of matter Sheaf (mathematics) Mereology Sequence Virtual machine Number Connected space Sequence Latent heat Computer configuration Order (biology) Computer worm Software testing Finite-state machine Flag Window
Point (geometry) Random number Server (computing) Sine Randomization Computer file State of matter Multiplication sign Range (statistics) Client (computing) Mereology 32-bit Number Sequence Synchronization Network socket Flag Integer Selectivity (electronic) Email Block (periodic table) Client (computing) Bit Sequence Connected space Number Sinc function Arc (geometry)
Email Scaling (geometry) Multiplication sign Bit rate Client (computing) Web 2.0 Strategy game Bit rate Semiconductor memory Kernel (computing) Flag Extension (kinesiology) Data recovery Maxima and minima Überlastkontrolle Deadlock Control flow Sequence Measurement Connected space Order (biology) Buffer solution Spacetime Data buffer Point (geometry) Dataflow Game controller Server (computing) Implementation Link (knot theory) Maxima and minima Überlastkontrolle Spyware Web browser Login Field (computer science) Number Read-only memory Program slicing Energy level Spacetime Router (computing) Window Dataflow Information Computer network Denial-of-service attack Cartesian coordinate system Frame problem Voting Kernel (computing) Software Web service Window Extension (kinesiology)
State transition system Socket-Schnittstelle Implementation Game controller Distribution (mathematics) State of matter Interactive television Rule of inference Theory Formal language Data model Latent heat Schwerpunktsystem Diagram Implementation UDP <Protokoll> Socket-Schnittstelle Block (periodic table) Interface (computing) Computer network Complex number Connected space Phase transition Interface (computing) Theorem output Fingerprint Address space
Rule of inference Socket-Schnittstelle State transition system Computer network Stack (abstract data type) Semantics (computer science) Thread (computing) Data model Software Logic Logic Software testing Endliche Modelltheorie Oracle
Web page Socket-Schnittstelle Group action Validity (statistics) Code Computer network Stack (abstract data type) Line (geometry) Tracing (software) Virtual machine Data model Latent heat Logic Logic Software testing Finite-state machine Diagram Endliche Modelltheorie Oracle
Revision control Architecture Group action Closed set State of matter MIDI Bit Finite-state machine Virtual machine
Architecture Latent heat Software Semantics (computer science) Computer architecture
Implementation Latent heat Internetworking Endliche Modelltheorie
Point (geometry) Implementation Group action Latent heat Validity (statistics) State of matter Musical ensemble
Data model Implementation INTEGRAL Different (Kate Ryan album) Computer worm Bit Communications protocol Error message
Latent heat Group action State of matter Logic Order (biology) Maxima and minima Predicate logic Mereology Higher-order logic Reading (process)
Lemma (mathematics) Cartesian closed category Musical ensemble Semiconductor memory
[Music] the next talk is by Hannah's minute you can see him here already it's called transmission control protocol also known as TCP and Hannah's me networks at a nonprofit organization in Berlin it's called Centre for the cultivation of Technology and he also works on an on an open know what is Mirage OS if you don't know it maybe you can find out what it is and here we researchers in several engineering areas such as programming languages network protocols security protocols and many many more so give him a warm applause for his talk
[Applause] [Music] thank you yes today I want to talk a bit
about the transmission control protocol and the Internet Protocol suite so what is it all about its foundation talk here so if you already know tcp/ip by heart then maybe only the last five minutes will be of interest for you otherwise so if you if you want to connect your laptop or if you want to browse to a website somewhere you want to read their website it is that the client on your
laptop so the web browser that sends an HTTP request to the web server host so sends an HTTP request which is specified
by the HTTP protocol it maybe get slash it's a common method of getting the main page of a website but how is this information actually transmitted to the server that is the question and the motivation for this talk so that is something I want to go deep into into that into the answer for the question so let's look a bit about the at the network top topology so on the left hand
side we have the laptop which sends to some server a get request you can see that by the dashed arrow and the laptop itself is connected likely we are wireless network to the Internet but what is actually the Internet well the Internet is a collection of computers and your laptop or anyone's mobile phone is slightly connected to a router router is just a normal computer which has some knowledge about the network and that router is slightly connected we are fiber or satellite or any other link like can also be in a band cable to another router or to several routers and this then this in this picture you can only see two routers in the router a and rota B but there may be any number of routers or nearly any number of rod in between you and the server so here the rota B is connected via ethernet which is just a physical cable to the server and Ethernet is a protocol which has talked over the cable so I won't go into the physical network connectivity like fibers and satellite in Dedham and cables and copper cables in this talk at
all but I will start with the layer which is on top of the physical medium so the first one is a data link layer and well what is the data link layer
what task it is is it has a scope of a network and it's only spent of the local network to which a host is connected so in this picture only the laptop and the
router is she had the same data link layer as well as the router B and rota a they shared the same data link layer
it's also the case that route a B and the server shared the same data link layer what is the task of the data link
layer well it's pretty easy address moose internet layer packets between two different hosts at say on the same link so the data link layers really it's only purpose is to provide an abstraction over the physical thing and how many bytes you can transport on the physical media over the link so the next layer is already the internet layer or the yeah the internet layer which task is to transport packets across multiple networks so as you have seen in the in the diagram there are rota a and wrote a bead they are both connected to several data link layers and they used the internet layer in order to transport packets across them the internet layer solves already the issue of addressing by providing for every host and IP address IP address is actually the Internet Protocol address and the internet layer provides another task or salt another task which is routing so it forwards packets to the next router which is hopefully closer to the final destination that is so toxic the internet layer also has support for fragmentation so if you are higher layer
sends something which is way too big for the data link layer then the internet layer can fragment that and the other side has to reassemble it what is on top of the internet layer is the transport layer so the transport layer establishes host-to-host connectivity it does multiplexing usually using source and destination ports and there are two widely used transport layer protocols
which I will go into more detail in this talk which is the user data bit user Datagram protocol and the transmission control protocol that's UDP and TCP and they have different properties so UDP is unreliable and it is not ordered and it is only an abstraction over datagrams and it has on the advantage side it has a very low overhead but as TCP is reliable and Woodards byte stream so you
have a you have a reliable byte stream which you can work on the downside of TCP is that its connection establishment and teardown is slightly more complex and UDP you just don't have to establish a connection and tear down and connect but on TCP you have to synchronize the two hosts then on top of the transport
layer we have the application layer level and the plication layer just exchanges application data over the transport layer so some examples for application layers are HTTP or TLS or DNS so in the first example we saw there was HTTP and HTTP was used to send the get breakfast so that is all application layer which I won't focus in this talk at all for the lower layers the application layers dressed payload so it's just some arbitrary data so if we look again at
that picture and we draw the different
layers which are supported or which I use by the different devices we end up
with diagram similar to that so here on the Left we have the laptop again which has all four all four layers and then we have the routers in the middle which only which are only using the data link and the internet layer and then on the right hand side we have the server which also has all four layers so the transport layers really hosts two hosts so the TCP we saw earlier the TCP is establish establishing a connection from the laptop to the server and on top of TCP so on top of the transport layer there's the process to process communication so the application layer which is the web browser talking to the web server so only on the highest layer here we have the get request and the routers in the middle they don't have to inspect or they don't have to use information of the transport or application layer from the laptop odds so the routers just for using the internet layer they forward packets to the next router what with the final destination so the laptop first sends the whole TCP segment or a TCP packet to the rotor and the rotor a decides oh yeah I've forwarded to router be-because rata B is more closer to the final destination than myself and the rotor B says oh yeah well I actually know and I'm connected via ethernet to the final destination so I will just forwarded to the server that's how the data flow of such action would look like how does the
packet actually look like so we have
seen that the application layer we have the application data which is here in blue and that one is just the get request and then the transport layer actually prefixes the application data with a header which is a common header that encodes some data we will look into the TCP header in more detail soon then the internet layer also adds a header a prefix the IP header which is just put in front of the TCP header and then the data link layer of all that is the lowest layer we we actually care about and that one will likely prevent the header and append the food in order to synchronize or to make sure that the physical wire only has only sees a single packet at time so as you can see from the layering from those two
pictures on the bond side you have the bottom to up layer and every layer if
you go down from the application to the
transport to the Internet you directly they basically add some header information and the internet layer for example that takes the TCP header so the transport layer and the application layer as payload so it doesn't care that it is TCP it could as well be UDP in this case so what is actually in the
serval not go into the data link layer details at all but here's is the header of an IP version 4 frame or packet and that one is at least 20 bytes it contains of various fields the first one is a 4 bit version which usually is version 4 in our current world then it has a 4 bytes 4 bits header length which is header length in words in multiples of 32 bits then it has some not really used or stuff I went deal with in this talk it has a total length field which is 16 bits and it describes how long the the entire IP frame is then it has an identification which is also a 16 bit unique number and 16 bits for fragmentation Flags and offset and that is crucial so if the IP header decides oh yeah well the take of you the application data you sent me is way too big for this data link I need to fragment it then it will just reuse the very same identification number and then use here the 16 bits in the fragment fragmentation flags and offset in order to portion that application data into multiple IP fragments then it has some field which is 8 by 8 bits so 16 so one entire byte it's the time to live and it's actually not the time stamp but it's only a count so how many routers should this Packard live how long should this packet live and every router decreases that time to live by one then it has a one byte protocol field which specifies what is the type of the payload carried by this up he version four packets don't has a 16 bit header checksum which is a CSE checksum to avoid that some bits got flipped in the on the transport then we can see the source IP address and the destination IP address which is yeah very I mean it the false IP address is the IP address of my laptop and the destination IP address is the IP address of the server and then after after those 20 bytes you have either IP options if the header length was more than 20 bytes or you have directly the payload now for the protocol field here there are various types and various types are predefined one is ICMP which is the internet control message protocol I will talk a bit about that which is the product field near the numbers set of one then for TCP it's set to six and for UDP it's 17 we have other protocols which can be carried of an IP frame or an IP packet but I won't go into the details here as you can see there are at least two hundred fifty five numbers here and the products fields so because it's a bit long you can store up to 256 different numbers in there so ICMP is a protocol I haven't talked about at all but it is the Internet control message protocol so it sits on top of IP and its purpose is on the one side to deliver error messages such as destination host
unreachable or time to live exceeded and on the other side it also can carry operational information like Diagnostics there's one program which you may know which is called ping and ping the the purpose of ping is to send an ICMP echo request to a remote host and the remote host is then supposed to send them to
send very same packet with only one single bit flipped and send that back to you and that is an ICMP issue reply and if you can successfully ping another host you can verify that the other host has at least IP connectivity up and online okay let's look into the next layer which is the
transport layer and at first we will look into a UDP header a UDP had as only eight bytes it contains it consists of a source port destination port then the length of the entire UDP frame and the checksum the checksum is again 16-bit field that's computed its computed over the entire payload and the header plus some IP pseudo header so with this actually carries the information of the source and destination IP address inside of itself UDP as I mentioned there this angry bot unreliable unordered and it's advantage is that's low overhead datagrams as you can see it's it it's eight bytes to the to the payload various IP already added 20 bytes to the payload here's a simple Yonex program which is a UDP client this program does not compile because I left out some bits but in order to see what how do you actually use this whole IP stack so the IP stack the tcp/ip stack is usually embedded in the kernel and as a programmer as an API program you have the API provided by the
UNIX sockets API and that one usually contains of the very same five or seven functions which is the first one is socket socket opens or creates a file descriptor and you specify the address family and the socket type so this is the address family Internet and the socket is a Datagram socket it's called D Grayman UNIX once that is created then you for a UDP flow and you just say oh I will use the function send - which takes a socket file descriptor so just a file descriptor and then some data and will just send it to the other side since it's unreliable it just fire and forget then afterwards we close the socket file descriptor because we are nice here and we try to penalize the other side so if you don't have a UDP client but if you want to implement a UDP server or a UDP listener what do you do is you again create a socket then you have the function which is called bind bind binds into can bind into a specific IP address on your server or on your network stack then you say receive from receive from takes the socket file descriptor and the buffer and some maximum size and an offset and yeah you just receive from will only return once you actually receive the UDP frame on that IP address and port and then you then we print out that we received some packets and we close the socket false Krypton so that's your EP you DB is used for a
variety of protocols and it's crucial to have it tcp on the other hand is a bit
bigger so instead of 8 bytes header tcp ads and other 20 bytes of header what does the TCP header contained
well similar to UDP it contains source port and destination port but again 16 bits then it contains 2 sequence numbers one is the sequence number itself it's a 32-bit number and one is the acknowledgement number which is the last sequence number we have seen from the other side then TCP contains data offset that offset is similar to the header length field so TCP a TCP segment may also contain some options so the header may contain options before a payload that's why we need a data of set fields in order to be able to find out via this actual payload start then TCP has certain flags and some of these flags I know some flags are just single bits values and some of them I mentioned down here which I will go into more detail later which is acknowledgment or arc synchronize or soon and finished orphan there's also reset and some urgent stuff I will not go into detail of that then we have a 16-bit field which is the window size which is the size of the receive buffer then we have again a 16-bit field check them and then we have some space for the original stuff I will not go into detail
it is a big client if you program it in the UNIX way you have a very similar API as we have seen in the UDP so we first
call the first create a file descriptor using the socket system call which we give again the address family eyelets and the sock stream which is the since we are stream oriented it's a it's the name of the TCP it's a name of for TCP socket then as a TC geek fly and we connects using the socket file descriptor to a remote host and then once we are connected so connect will only return once TCP session has been established then we say here receive so we receive on the socket file descriptor the specific buffer buffer then we printed and then we close the sock false good again the tcp listener is very similar so well first we create a socket then we bind it and bind specifies the IP address and also the port number then we use a function called listen on the socket file descriptor and then we enter a loop and so now we wait for client connections which appear at some point and for every client connection we well we call accept and accept returns whenever there was a client which successfully established TCP connection what accept returns is a new file descriptor so another file descriptor not the same as a sacrifice descriptor so the socket file descriptor we call again accept on it's at a later point usually you then handle any work on the client connection on this new FD you handle that in a separate process or set a separate thread or a separate task in order to enable the server to accept another connection while you are handling the the one client connection then we just do some printf output and we send hello world to the client to the client connection so to this new file descriptor then we close it and we start from the while one and we accept a new client socket so that is TCP listener as we have seen it and as you will see it in in in any network program now TCP as I mentioned that it has to do some work
in order to establish a section session and to tear down the main work which
needs to be done is to synchronize the initial sequence numbers because we have
seen in the header that we have this sequence number and somehow we need to transport that information to the other
side so yes the TCP state machine were just which has initially been part of the RFC which is the specification for TCP and also duplicated and books like Stevens design and implementation of the of TCP IP and TCP IP Illustrated and so on so you can see it is test year one specific state which is listen and listen is as we've seen in the server implementation if you call listen then you are in the listen stem in the listen State and you always start well you always end up in the in the close state after you've called close basically I will go into more detail of connection
establishment and teardown right now so on the connection establishment we have seen on the client side we start with the socket in the close state then we say the UNIX connect on that socket and that connect does does send an initial TCP segment to the server side which has the synchronize flag set to true or said one and the sequence number is some artificial number some random 32-bit integer number so I just call it a here the state of the file descriptor goes from closed to sin sent and soon send yeah well we just have sent out the the synchronized segment so TCP segment which doesn't carry any data but only the TCP header on the server side we had prepared previously we started in a closed state then we called listen then we end up in a listen state now in the listened States we call accept and accept blocks until the sin is received and once the sin has received a new socket is a new file descriptor spawned and that one ends up in the sin received state the server sends out the TCP segment again without any data but the sin and acknowledgement flags are said and the sequence number said to Sam B and the acknowledgement numbers set to a plus one so the acknowledgement number acknowledges that the sin was received with the sequence number a plus one upon the client receiving that sin and arc it is in the Select state and it will send out an acknowledgment segment so that the other side the server knows oh yeah my segment has been received and that one is sent with the sequence number of a plus one because a was already used here and the syn flag consumes one one byte or one in the sequence number range and the acknowledgement number is also said to be plus 1 so that is the sequence premiere plus one once that has received the server ends up in the established state sequence numbers yeah well it's a good idea of both house take a random initial sequence number for each connection otherwise we can get into some nasty attacks the acknowledgement number is the next sequence number from
the other hosts and the sequence numbers always increased for each part of data and for the sin and Finan flags which are only single bits each sequence number must be not acknowledged and each sent occurred is retransmitted unless it is acknowledged after a certain time odd and after a certain retransmit time after trying it several times at some point the TCP stack gives up the tiara and since I'm a bit short on time I will skip that this me provides us with the
flow control what does that mean well every network stag has received so the colonel has a receive buffer for each TCP connection and that buffer is size limited to avoid kernel memory exhaustion which means that whenever the application so the web server or the web browser is reading data some buffer space is reclaimed and when TCP segments are arriving some of that buffer is consumed it's a sliding window and we have seen in the TCP Haddad's window slice so there's a 16-bit field called window size which specifies how many more bytes my my TCP stack has for receiving data from the other side to vote dead logs there's also a timer in a timer called the persist timer which is started when the window is when the window size is zero and that then at a timeout try retransmit said TCP segment in order to get information about the new window size from the other side congressional control level also skipper but but the main idea is to control the rate of data entering the network because of you're using multiple routers at some point you you may separate some of the network links and that is avoided and TCP by doing by applying congestion control which measure is for example the time between segments sent and acknowledgment received also has to do with slow start and how your window size even given no buffer gross acknowledgment well there are some strategies the basic one is every segment is acknowledged individually there's a delayed where you collect multiple segments to acknowledge them at a certain time then you have also selective acknowledgments where you can acknowledge discontinuous segments which helps for lowering the amount of retransmissions TCP also carries some maximum segment size to avoid fragmentation actually on the IP layer because it is partially open there's some struggle because you have simultaneous open so what if both parties want to open a connection at the very same time then you have a flag which was called reset in order to terminate a connection there are some extensions like windows scaling and fast open to improve the throughput and also to lower the delay there are some attacks like denial of service so if your server implementation accepts something and allocates a lot of memory for a client which doesn't do a lot but just sending a syn frame that is bad and leads to denial of service connection hijacking if you can predict the sequence numbers then you can hydrect and omit data into an established connection there have been some blind in window attacks what does that mean that even without knowing the sequence number you can do with something on a established TCP connection such as yeah sending a reset
or sending a thin frame and tearing that connection down the specification for
TCP is written in English truth in connection of our C's and there are some widely deployed implementations during
some research work in Cambridge over the
last years me and various colleagues implemented a formal model developed in the interactive theory to valhalla for
which has a precise specification with implementation no looseness and we really use that as an input so the sockets API and interface for getting the TCP control block which is the internal state of the TCP and then the viand phase which is data received and send on that and we used that formal model to validate itself as have we used actual implementations to do that we use it to draw some diagrams where you can see the rules which fires on the
left-hand side when something happened like there was a connect called and then the logical rule connect 1 was used in the labeled transition system then we see here as well some TCP segments which are out going out and in what are the
contributions of the network semantics its we checked we check the model we
validated model by recording traces and executing them we published a paper called engineering that's an logic rigorous historical specification and validation for tcp/ip and the UNIX sockets API the specification itself is typeset in 384 pages that's all the transitions you basically need it's roughly 10,000 lines of for code and a lot of comments will be embedded in lot of latest code and the yonex tcp/ip sig has usually around 15,000 lines of code the TCP state machine we saw earlier is here in this paragraph in
this diagram and we try to draw a more
correct TCP state machine which led us to this picture which is a bit more complicated we have this state non-existing up here and we have much more transitions due to timers and so on so the state machine
use and common literature is actually not complete or not precise and we have
a revision for that conclusion is yeah well TCP RDS what we deployed I hoped I managed to give you some insight how TCP
IP actually works the layered architecture which was agnostic of underlying layers and in the network semantics working we had an executable specification that all I have to say and I welcome you to ask any questions either now or offer
thank you so if you have any questions
just go to the microphones we have two here and two on the right side and do we have some questions from the Internet no questions no more questions yeah one question come on don't be shy
right hi thanks it was a very interesting talk so your model does it allow synthesizing a implementation from the specification or is it used mostly for validating it's at the moment useful
validation because we have the specification looseness so we have implementation looseness so at some point in their invitation you have to choose whether you take one transition or the other one so if you go into a failure state or if you go into a success or if you transmit some piece of data and go into a success state so we don't have synthesized any implementation but there's ongoing work to use it as a implementation as a base for implement implementation okay and do you think that if such a implementation can be made can it be made efficient as well once synthesized yes okay thanks [Music]
yeah your question please thank you how independent is TCP from IP
I mean can you integrate TCP over different protocols like Bluetooth or something that since TCP requires for
error messages a bit of ICMP I'm I haven't seen any TCP implementation on top of any other medium than IP so I don't know but I can think of it good work okay your question please thank you hello
so you used all four for the specification part did you actually need to the higher-order logic part of whole or would it be possible to just use predicate logic see I I will have to
reread I think we need actually some higher order logic for it for the host state and the transitions would be it would be interesting to meet and well the paper has been published a journal of ACM and luckily Sky Harbor is is available and you can download it for free from there ok thanks any more
questions No then thank you Hannah's a warm applause for Hannah's plea [Applause]
[Music] [Applause] [Music] [Music]
Feedback