IEEE/ACM TRANSACTIONS ON NETWORKING, VOL. 10, NO. 2, APRIL 2002
`
`193
`
`Formal Specification and Verification of Safety and
`Performance of TCP Selective Acknowledgment
`
`Mark A. Smith and K. K. Ramakrishnan, Member, IEEE
`
`Abstract—We present a formal specification of the selective ac-
`knowledgment (SACK) mechanism that is being proposed as a new
`standard option for TCP. The formal specification allows one to
`reason about the SACK protocol; thus, we are able to formally
`prove that the SACK mechanism does not violate the safety proper-
`ties (reliable, at most once, and in order message delivery) of the ac-
`knowledgment (ACK) mechanism that is currently used with TCP.
`The new mechanism is being proposed to improve the performance
`of TCP when multiple packets are lost from one window of data.
`The proposed mechanism for implementing the SACK option for
`TCP is sufficiently complicated that it is not obvious that it is in-
`deed safe, so we think it is important to formally verify its safety
`properties.
`In addition to safety, we are also able to show that SACK can
`improve the time it takes for the sender to recover from multiple
`packet losses. With the additional information available at a SACK
`sender, the round-trip time that a cumulative ACK sender waits
`before retransmitting each subsequent packet lost after the very
`first loss can be saved. We also show that SACK can improve per-
`formance even with window sizes as small as four packets and in
`situations where acknowledgment packets are lost.
`
`Index Terms—Congestion control, formal verification, I/O au-
`tomata, TCP performance, TCP SACK.
`
`I. INTRODUCTION
`
`T RANSMISSION Control Protocol (TCP) offers applica-
`
`tions the semantics of a reliable, flow-controlled channel.
`The acknowledgment (ACK) mechanism of TCP is an impor-
`tant part of what makes the protocol reliable. By reliable, we
`mean data from the sender is not lost, duplicated, or received
`out of order. TCP guarantees these properties, which we refer
`to as safety properties, even though the underlying communica-
`tion medium may lose, duplicate, or reorder packets. We assume
`corrupted packets are dropped.
`Selective Acknowledgments (SACK) [10] have been pro-
`posed as a complement to the traditional approach of using
`cumulative acknowledgments for TCP. SACK is proposed
`as a standard option to be used by cooperating senders and
`receivers. The receiver can take advantage of the SACK option
`to report that it has received multiple packets out of sequence. A
`sender receiving a SACK has the opportunity to retransmit the
`packets that comprise the holes in the sequence number space
`as indicated in the SACK. The new functionality that SACK
`
`Manuscript received May 12, 1999; revised March 7, 2001; approved by
`IEEE/ACM TRANSACTIONS ON NETWORKING Editor K. Calvert.
`M. A. Smith is with Bell Labs, Murray Hill, NJ 07974 USA (e-mail: mas-
`smith@lucent.com).
`K. K. Ramakrishnan is with TeraOptic Networks, Inc., Sunnyvale, CA 94085
`USA (e-mail: kk@teraoptic.com).
`Publisher Item Identifier S 1063-6692(02)03106-0.
`
`introduces is the potential for earlier recovery, especially when
`multiple packets are lost in round-trip time (RTT). This quicker
`recovery may also result in higher throughput because the more
`severe congestion recovery mechanisms are not invoked.
`The SACK mechanism includes sufficient additional com-
`plexity that we believe it is important to examine whether it
`operates correctly. It is not obvious from reading the English
`language specification of [10] that it satisfies the safety proper-
`ties of the ACK mechanism. Simulation experiments have been
`done to understand the performance improvement with SACK
`[1], and while these lend confidence that the protocol operates
`as expected, simulations do not ensure that the protocol is cor-
`rect. Formal specifications and verification help significantly in
`ensuring that protocols operate correctly. Therefore, we feel that
`a formal specification and verification of the safety properties of
`the mechanism is useful. We have developed a formal specifi-
`cation of the SACK mechanism using the I/O automaton model
`of Lynch and Tuttle [7]. The formal specification of the SACK
`mechanism allows one to reason about the protocol in a rig-
`orous manner. For the formal verification of safety, we use in-
`variant assertion and simulation (refinement) techniques. These
`methods are used for proving trace inclusion relationships be-
`tween concurrent systems. Trace inclusion means the external
`behaviors of one system is the subset of the external behaviors
`of another system. For this verification, we use the methods to
`show that the external behaviors of TCP with the SACK option,
`which we refer to simply as SACK, is a subset of the external
`behaviors of a simple abstract specification for end-to-end reli-
`able message delivery. We use the formalization of simulations
`developed by Lynch and Vaandrager [8].
`A key aspect of our formal specification of the SACK mech-
`anisms is that it allows more nondeterminism than the English
`language specification [10]. Our specification focuses on key
`aspects of the protocol needed for safety while leaving certain
`aspects of the protocol, such as retransmission strategy, unspeci-
`fied. This means our correctness proof is quite general and holds
`for any implementation of the protocol that uses a specific re-
`transmission strategy or other specific behaviors that we leave
`nondeterministic in our specification.
`We extend the specification used to prove safety properties
`to include time using the general timed automaton model of
`Lynch [6]. We use this model to calculate the latency of packets
`in a window of data in a worst-case scenario and prove that
`SACK can lead to improved performance relative to the cumula-
`tive ACK mechanism. In fact, we prove that in situations where
`the multiple packet loss comes early in the transmission of a
`window of data, the improved performance with SACK is pro-
`HTT "' (k: - 1)
`portional to
`, where
`is the number of packets
`k:
`
`1063-6692/02$17.00 © 2002 IEEE
`
`IPR2022-00833
`CommScope, Inc. Exhibit 1023
`Page 1 of 15
`
`

`

`194
`
`IEEE/ACM TRANSACTIONS ON NETWORKING, VOL. 10, NO. 2, APRIL 2002
`
`lost in a window. We also show that SACK can improve per-
`formance even when window sizes are small and/or when ac-
`knowledgment packets are lost.
`In the next section, we present an informal description of both
`the cumulative ACK and SACK mechanisms. In Section III, we
`present the abstract requirements of the reliable message de-
`livery service, and we also present a brief description of the
`formal model we use in the paper. In Section IV, we present the
`formal specification of the SACK mechanisms. Section V has
`the proof of safety along with a short description of the proof
`techniques we use. In Section VI, we prove that SACK can lead
`to improved performance, and we conclude in Section VII. The
`paper also contains two appendices. Appendix I gives formal
`definitions for the notation used in the abstract specification of
`the reliable message delivery problem and the formal descrip-
`tion of the SACK mechanism, and Appendix II contains the
`proof of the invariants in Section V.
`
`II. INFORMAL DESCRIPTION OF THE ACKNOWLEDGMENT
`MECHANISMS
`
`TCP uses a sliding window mechanism for its flow control,
`acknowledgment, and retransmission policy. The basic idea is
`n > 0
`that there is a window of size
`, that determines how
`many successive segments of data can be sent in the absence
`of a new acknowledgment. Each segment of data is sequen-
`tially numbered, so the sender is not allowed to send segment
`before segment has been acknowledged. Thus, if
`is the
`i
`i+n
`'t
`largest acknowledgment number received by the sender, there is
`a window of data numbered to
`which the sender can
`i+n-1
`i
`transmit. As successively higher numbered acknowledgments
`are received, the window slides forward. The acknowledgment
`mechanism is cumulative in that if the receiver acknowledges
`segment
`, it means it has successfully received all segments
`k
`k
`k
`up to and including . Segment
`is acknowledged by sending a
`request for segment
`. Data that is transmitted is kept on a re-
`k+l
`transmission buffer until it has been acknowledged. In a simple
`k < n+i
`go-back- protocol, if
`, the sender may retransmit seg-
`n
`ments
`to
`from the retransmission buffer. However,
`k+l n+i
`in TCP the decision to retransmit these segments depends on
`the receipt of duplicate acknowledgments and on timeouts. With
`TCP Reno, only the first packet in the retransmission buffer
`is sent. Subsequently, the sender waits until the retransmitted
`packet is acknowledged. This strategy potentially reduces the
`unnecessary retransmissions compared to the simple go-back-
`n
`protocol.
`Of particular interest are the mechanisms which TCP uses to
`recover from loss, including algorithms for fast retransmit [4].
`With fast retransmit, when the source receives
`duplicate ac-
`d
`knowledgments (e.g.,
`) for the same segment (say,
`), it
`d=3
`k
`determines that segment was lost. The source chooses to re-
`k
`transmit segment
`right away, rather than wait for a retransmis-
`k
`sion timer to expire. It must be noted that the sender retransmits
`one packet (or segment for the purposes of this paper) only.
`The limitation of the cumulative acknowledgment strategy
`is that it can only indicate that every segment up to
`has been
`k
`k + l
`received and
`has not been received. When multiple
`packets are lost from a window, the throughput of TCP can
`
`in the
`suffer greatly. After retransmitting the first packet
`retransmission buffer, the sender may be forced to wait for a
`retransmission timeout to retransmit subsequent “holes” in the
`receiver’s sequence number space.
`To remedy the problem that occurs when multiple packets in
`a round trip are lost, a selective acknowledgment mechanism
`is being proposed as a new standard option for TCP [10]. The
`mechanism allows the receiver of data to acknowledge noncon-
`tiguous and isolated blocks of data that have been received and
`queued, in addition to the cumulative acknowledgment of con-
`tiguous data. By isolated, we mean the segment just below the
`block and just above the block have not been received. Each
`block is defined by a pair of sequence numbers. The first number
`is the left edge of the block and is the sequence number of the
`first segment of data in the block that was received. The second
`number is the right edge of the block and is the number im-
`mediately following the last sequence number of the block that
`was received. The retransmission strategy of the sender also
`changes to use the additional information available with selec-
`tive acknowledgment. Now, in addition to the data segments
`in the retransmission buffer, there is a flag bit which indicates
`whether a segment has been “SACKed.” A segment with the
`SACKed bit turned on is not retransmitted, but segments with
`the SACKed bit turned off and sequence number less than the
`highest SACKed segment are available for retransmission.
`
`A. An Example With Cumulative ACK
`In Fig. 1, we show a simple example that illustrates how the
`(cumulative) ACK mechanism works with TCP Reno [5]. The
`figure shows the retransmission buffer of the sender and the
`buffer at the receiver. Let the window size be 8 for this example.
`The threshold of the number of duplicate acknowledgments that
`need to be received before the fast retransmit algorithm is trig-
`gered is assumed to be 3. The numbers in the buffers and the
`numbers on the segments sent by the sender represents the ac-
`tual segment of data and is the sequence number of that segment
`of data. The variable
`is the sequence number of the seg-
`snd_una
`ment at the head of the retransmission buffer. It is also the oldest
`unacknowledged segment of data. The
`variable is the
`rcv....nxt
`next contiguous segment of data expected by the receiver. This
`variable is the acknowledgment number that the receiver sends
`back to the sender. The execution illustrated in Fig. 1 begins
`with the sender transmitting segment 26. Next, segment 27 gets
`transmitted, but is lost due to, say, congestion. Subsequently,
`segments 28 and 29 are delivered. The acknowledgments gen-
`erated by the receiver on receipt of segments 26, 28, and 29 all
`indicate that the next segment expected is segment 27. In the ex-
`ample, segment 30 is also lost. Thus, two segments 27 and 30 are
`lost in the current window of 8 segments. Subsequently, when
`segment 31 is received, the acknowledgment generated triggers
`the fast retransmit algorithm. This causes segment 27 to be re-
`transmitted without waiting for a retransmit timeout. Notice that
`even after the source retransmits segment 27, acknowledgments
`are received with the next expected segment being 27 (sent in
`response to packets 32 and 33 sent before the retransmission
`of segment 27). This allows the sender to send new segments,
`but not retransmit any more segments from the retransmission
`buffer, since it does not know which segments need to be sent.
`
`IPR2022-00833
`CommScope, Inc. Exhibit 1023
`Page 2 of 15
`
`

`

`SMITH AND RAMAKRISHNAN: SAFETY AND PERFORMANCE OF TCP SELECTIVE ACKNOWLEDGMENT
`
`195
`
`receive buffer
`
`l26I I I I
`rcv_nxt= 27
`
`sender's
`retransmission buffer
`0
`126I I I I I I
`snd_una = 26
`0 0
`
`27
`- - -
`
`---x
`
`loss
`
`receive buffer
`
`l261 I I I I I I I
`rcv_nxt = 27
`
`sender's
`retransmission buffer
`
`snd_una= 26
`
`snd_una = 27
`
`12,12s1w13ij 31I 3zj33I
`snd_una = 27
`
`retransmission timeout
`
`l3ol31l32I 3~ 1 1 I I
`snd_una = 30
`
`l2~
`
`l26I
`
`l2~291
`
`l31I I
`l2slwl 1311321
`
`l26I 12s1w1 I 311321331
`
`I 26I 21I 2sl 291 I 311321331
`rcv_nxt = 30
`
`I 26I 27I 28I 29I 3W 3II 32l331
`rcv_nxt = 34
`
`Fig. 1. Example illustrating the workings of the ACK mechanism of TCP.
`
`If it were to decide to retransmit, it would have to retransmit the
`next segment in the buffer, which is segment 28. But this would
`be a wasteful retransmission. Hence, the sender desists from re-
`transmitting any new packets (but can use the opportunity to
`send new segments if the window allows it). It is only after a
`new acknowledgment is received indicating successful receipt
`of segment 27 can the sender potentially consider retransmit-
`ting another packet from its retransmission buffer. However, the
`second loss in a window is interpreted as a more serious situ-
`ation—hence the fast retransmission algorithm is not invoked
`to recover from this loss. The second segment that was lost
`in this window (30) is not retransmitted until a retransmission
`timeout. Because this timeout is necessarily large, the sender’s
`window is likely to be shut. Thus, during this timeout, the sender
`is unable to make progress, resulting in degraded throughput.
`This timeout also results in the sender dropping the congestion
`window size to 1 based on the congestion control algorithms de-
`scribed in [4].
`
`B. An Example With SACK
`
`Fig. 2 illustrates how the SACK mechanism works on the
`same set of data as in Fig. 1. With selective acknowledgment,
`the receiver sends back the regular cumulative acknowledgment
`number and SACK blocks. In the proposed implementation of
`the SACK mechanism described in [10], there are at most three
`SACK blocks in an acknowledgment packet.
`Initially, when the receiver gets segment 28 (after the loss
`of segment 27), it sends a SACK for segment 27 and a further
`SACK block indicating that segment 28 was received and seg-
`ment 29 was awaited after that. When segment 31 is received
`after the loss of segment 30, the SACK sent indicates that 27
`(the portion representing the cumulative ACK) is awaited, and
`
`snd una = 27
`0 0 0 0
`
`01 10000
`l21l2Bl29l30I 31134331
`01 10100
`121l2Blwl3ol 31)32j331
`0110100
`l21l2Bl29l3ol 31l32j33j
`0110111
`l21l2sl291 aj 31)32)33I
`0 1 1 1
`
`snd_una = 30
`
`l26I
`
`l28l291
`
`l26I
`
`l28l291
`
`j31j I
`l31l32I
`
`l26I 12s12~
`
`l31I 32l33I
`
`12612,1 2sl 291
`f 31132l33I
`rcv_nxt = 30
`
`I 2~21l2Blwl30l31I 321331
`rcv_nxt = 34
`
`Fig. 2. Example illustrating the workings of the SACK mechanism of TCP.
`
`furthermore that two blocks of data were received with an inter-
`vening gap of segment 30. The regular fast retransmit algorithm
`is triggered on receipt of third duplicate SACK indicating that
`segment 27 was lost. The source retransmits segment 27. But at
`the same time, the sender has the information that segment 30
`has also been lost as indicated in the SACK. Since the source
`now has the information of specifically which segments have
`been lost (segment 27 and 30), it has the ability to retransmit
`more than one of the lost segments. Therefore, the sender can
`also retransmit segment 30 and fill the second hole in the se-
`quence number space. The sender does not need to wait for a
`retransmit timeout for retransmitting segment 30.
`A further detail to be observed is the maintenance of the
`SACK flags at the source, associated with the segments still
`in the retransmission buffer. In the figure SACKed segments
`are not removed from the retransmission buffer even though in
`this example, these segments are not retransmitted. However,
`the SACK mechanism allows the receiver to drop segments that
`have been SACKed if it runs out of buffer space. Thus, it is pos-
`sible that these segments may need to be retransmitted. Since
`they are not retransmitted if the SACK flag is set, there must be
`a mechanism for resetting the flags to 0. In the SACK mecha-
`nism proposed for TCP when a retransmission timeout expires
`for any sequence of data, all the SACKed bits in the retransmis-
`sion buffer are reset to 0.
`Thus, the SACK option allows the sender to recover from
`losing multiple packets in a round-trip time, and “fill” all the
`“holes” in the receiver’s sequence number space based on the
`SACK blocks received. Further, it allows for the separation of
`the flow control and congestion control mechanisms from being
`intricately tied to the error recovery procedures, as we illustrated
`in the example. It allows the source the ability to be somewhat
`more aggressive in both retransmitting from the buffer on mul-
`tiple packet losses, and not dropping the congestion window
`down all the way to 1.
`
`IPR2022-00833
`CommScope, Inc. Exhibit 1023
`Page 3 of 15
`
`

`

`196
`
`IEEE/ACM TRANSACTIONS ON NETWORKING, VOL. 10, NO. 2, APRIL 2002
`
`III. FORMAL MODEL AND SERVICE REQUIREMENTS
`
`The safety properties we want to show for TCP with the
`SACK mechanism are that data from the sender is not lost, du-
`plicated, or received out of order. Our model does not capture
`data corruption, and we assume corrupted packets are discarded.
`In this work, we do not try to verify the safety of TCP in its en-
`tirety. We are only concerned with the effects of replacing the
`ACK mechanism with the SACK mechanism. Therefore, we as-
`sume that connection setup and teardown work correctly, and
`that crash recovery works correctly. Consequently, in our mod-
`eling of the SACK mechanism, we assume that the connection
`between the sender and receiver is already established and that
`there are no crashes. Before we present the specification, we
`give a brief description of the formal model we use.
`
`A. Automaton Model
`The formal model we use to describe the acknowledgment
`mechanisms is based on the I/O automaton model of [7]. An
`states(A)
`automaton
`consists of four components: 1) a set
`A
`start(A) C
`states(A)
`of states; 2) a nonempty set
`of
`of start
`steps(A) ~
`acts(A)
`states; 3) a set
`of actions; and 4) a set
`states(A) x acts(A) x states(A)
`acts(A)
`of steps. The set
`, and
`can be partitioned into three disjoint sets,
`in(A), out(A),
`int(A)
`of input actions, output actions, and internal actions, re-
`spectively. The union of the input actions and output actions we
`denote as external actions, those actions visible to the environ-
`ment.
`When an automaton runs, it generates a string representing an
`execution of the system it models. An execution fragment
`of
`a
`automaton
`is a finite or infinite sequence,
`,
`A
`A
`of alternating states and actions of
`starting in a start state,
`and if the execution fragment is finite, ending in a state such
`A
`that
`is a step of
`for every . We denote by
`(si, ai+l, Si+1)
`the first state of the execution fragment, and if it is
`£state( a)
`lstate( cv)
`finite
`denotes the last state. A state
`is said to be
`s
`A
`reachable if there exists a finite execution of
`that includes .
`s
`cv = s 0 , a1, s1, a2, ...
`Suppose
`is an execution fragment of
`trace(a) A
`A
`traceA(a)
`. Then
`is clear, is defined to be
`or
`if
`the subsequence of
`consisting of only the external actions.
`a
`We say that
`is a trace of
`if there exists an execution
`of
`A
`{3
`A
`CV
`trace( cv) = {3
`with
`.
`In specifying a complex distributed system, it is useful to be
`able to specify each process individually and then obtain a spec-
`ification of the entire system as the parallel composition of the
`specifications of the processes. The parallel composition oper-
`ator
`in this model uses a synchronization style where automata
`synchronize on their common actions and evolve independently
`on the others.
`A
`To show that an automaton
`implements another automaton
`, we show a trace inclusion relationship between them. The
`B
`set of traces of an automaton consists of the set of sequences of
`visible actions that the automaton can perform.
`
`B. Service Requirements
`For the formal description of the service requirements, we as-
`sume a very simple user interface—there is an input action from
`the user on the sender side to send data message
`, and on
`send(m)
`
`automaton ReliableQ
`
`signature
`input send(m: Seq[Byte))
`output deliver(m: Seq[Byte))
`
`states
`queue: Seq[Byte)
`
`:= {}
`
`transitions
`input send (m)
`eff queue : = queue II m
`
`output deliver (m)
`pre queue =f- {}
`m E prefixes(queue)
`eff queue := tail(queue, 1ml)
`
`Fig. 3. Model of the requirements of the reliable message delivery problem.
`
`deliver(m)
`
`the receiver side, data is passed to the user with the
`action.
`We define a simple automaton which is an abstract represen-
`tation of the safety properties that we want to show are satis-
`fied by the SACK mechanism. The automaton, which we call
`ReliableQ is shown in Fig. 3. We describe the automaton in
`the style of the IOA language [2] for describing I/O automata,
`but we do not strictly follow the syntax of the formal language.
`In the IOA language, an automaton is described by first giving
`its name followed by the four components of the model men-
`tioned above. That is, we have the action signature (signature),
`the states and start states (states), and the set of steps (transi-
`tions). Transitions are written in a precondition, effect fashion.
`That is, the states in which an action is enabled is given as a pre-
`condition, and the resulting states are given by the effects of the
`action.
`The only state variable of the automaton is queue which has
`type Seq[Byte] and is initially empty. The type Seq[Byte]
`is an ordered list or sequence with elements of type Byte. We
`{}
`denote the empty sequence as
`. The input action
`send(m)
`from the user causes data
`to be added to the tail of the queue.
`m
`II
`The symbol
`is the concatenation operator. The output action
`passes data from the head of the queue to the re-
`deliver(m)
`ceiver side user. The prefixes operator returns the set of pre-
`fixes of the queue, and the
`operation removes
`tail(queue, 1ml)
`the first
`elements from the queue. Since the queue does not
`1ml
`lose, duplicate, or reorder data, it is easy to see that the speci-
`fication ReliableQ gives the safety properties we want. The
`prefixes, tail and all the operators used in subsequent sec-
`tions are formally defined in Appendix I.
`
`IV. FORMAL SPECIFICATION OF SACK
`
`TCP has the basic structure shown in Fig. 4. There is a sender,
`a receiver, a channel for packets from the sender to the receiver,
`and a channel for packets from the receiver to the sender. The
`protocol is only run at the sender and the receiver, but it assumes
`the channels, so the channels must be modeled. We model each
`component as an automaton, and the complete system is the
`parallel composition of the four component automata.
`In our models of the sender and the receiver below, we specify
`certain state variables as unbounded integers. However, in the
`actual protocol, the size
`of these variables is bounded. Cer-
`tain aspects of our proof of the correctness of the protocol relies
`
`IPR2022-00833
`CommScope, Inc. Exhibit 1023
`Page 4 of 15
`
`

`

`SMITH AND RAMAKRISHNAN: SAFETY AND PERFORMANCE OF TCP SELECTIVE ACKNOWLEDGMENT
`
`197
`
`send(m) 0send-pkt (tl I c,,.(T)
`
`s
`
`rev-pkt (t) C (Tl
`rs
`
`I rcv-pkt..,.(t) •
`
`send-pkt,.(t)
`
`automaton c.,. ( T: type)
`
`signature
`input send-pkt.,. ( t: Tl
`internal drop.,.(t: T)
`Internal duplicate.,.(t: T)
`output rcv-pkt.,.(t: Tl
`
`states
`in_transit.,.: Mset(TJ :a{}
`
`transitions
`
`input send-pkt.,.(t)
`in_transit.,. := in_transit.,. U {t}
`elf
`
`Internal drop.,.(t)
`pn t e in...transit.,.
`in_transit.,. := in_transit.,. \ {t}
`elf
`
`output rcv-pkt.,.(t)
`pn t E in_transit.,.
`in_transit.,. := in...transit.,. \ {t}
`elf
`
`internal duplicate,,.(tl
`pre t E in_transit ...
`in_transitor := in_transit,,. U {t}
`elf
`
`Fig. 5. Model for the channel for packets from the sender to the receiver.
`
`to be retransmitted. Each byte of data is grouped with its se-
`quence number and a flag indicating whether the byte of data
`has been selectively acknowledged. Both buffers are initially
`empty. The segment variable is the current segment being
`sent,
`is the sequence number of the oldest unacknowl-
`snd_una
`edged byte,
`is the sequence number of the next byte to
`snd__nxt
`be sent, and
`is a flag that enables the sending
`ready_to_send
`of segments when the transmission window is open.
`Input action
`is the action by the user that passes data
`send(m)
`to the sender, and
`-
`-
`prepares a new seg-
`prepare new seg(s)
`ment to be sent. It is only enabled if the sender is not currently
`enabled to send a segment
`, the send buffer
`( ,ready _to_send)
`is not empty, and the available window size is greater than 0 (we
`assume a constant window size of WS). This action nondeter-
`ministically chooses the portion of data to be sent. This portion
`of data,
`, must be a prefix of the send buffer and its length,
`s
`Isl
`written
`, must be less than or equal to the minimum of the
`maximum segment size (MSS) and the available window size.
`The effect of this action is to remove
`from the send buffer,
`s
`and then to pair each element of with its sequence number.
`s
`This pairing is done by the
`s snd nxt operation. The new
`enum( ,
`list forms the segment to be sent and is assigned to the vari-
`able segment. A SACK flag that is initialized to false is added
`to each pair in the segment sequence before it is concatenated
`to the retransmission buffer. The
`operator performs
`init_flag
`this initialization.
`The
`action places a segment on the
`-
`send pktsr(seg)
`outgoing channel,
`, of the sender, and
`-
`rev pktrs(aek)
`Csr(T)
`takes a simple ACK packet from
`. First ack is
`Crs(T)
`checked to see that
`it acknowledges data that was sent,
`snd_una < aek ::; snd__nxt
`. If this condition is true, the
`acknowledged data is removed from the retransmission
`buffer, and
`is updated. When a SACK packet
`snd_una
`is
`received,
`,
`the
`sender
`-
`rev pktrs(aek, bl, b2, b3)
`sets the SACK flag of the bytes indicated by the SACK
`blocks to true with the assignment of
`to
`retran_buf
`.
`set_saek(retran_buf, bl, b2, b3)
`
`Fig. 4. Structure and the four basic components of the model for SACK.
`
`on being able to make accurate comparisons of the relative size
`of some of these variables. When the variables are unbounded, it
`is easy to see that these comparisons are accurate. However, with
`a bounded number space that may wrap around, it is not so clear
`that these comparisons, which must now be made modulo
`,
`232
`can be done accurately. TCP uses various timing mechanisms
`coupled with the relatively large number space to ensure that
`the relative size of variables are not confused. For further de-
`tails and formal proofs as to why the timing mechanisms work,
`see [11]. The mechanisms do not vary between standard TCP
`and SACK TCP, so we do not focus on them here. Instead, we
`use unbounded counters to simplify our models and proofs.
`
`A. Channel Automaton
`The channels in our model can lose, duplicate, and reorder
`packets, but they do not corrupt or create spurious packets. The
`I/O automaton model for the channel from the sender to the re-
`ceiver,
`, is shown in Fig. 5. The model for the channel
`Csr(T)
`from the receiver to the sender is essentially the same, so we do
`not show it here. The basic difference is that the subscripts in
`the names of the state variable and the actions in the signatures
`are different and reflect the directional flow of packets in the
`channels. The channels have a packet type that is the channel pa-
`rameter
`. The state variable
`(for the receiver to
`in_transitsr
`T
`sender channel the variable is
`) holds the packets
`in_transitrs
`placed on the channel. Since the channels may have duplicate
`copies of a packet, this variable is a multisets of type
`. The
`T
`fact that it is a multiset means the packets are not ordered. Thus,
`packets may be received in a different order from the way they
`were sent.
`The
`input action places a packet in the mul-
`-
`send pktsr(t)
`tiset. The complementary output action
`-
`removes
`rev pktsr(t)
`the packet from the channel. The internal action
`d.r0 Psr(t)
`nondeterministically removes an element from the multiset. The
`set minus operator for the multiset only removes one copy of an
`element. The internal action
`adds one addi-
`duplieatesr( t)
`tional copy of an element to the multiset.
`
`B. Sender Automaton
`In this section, we present a formal I/O automaton model for
`s
`the sender protocol of the SACK mechanism. The automaton,
`,
`is shown in Fig. 6. We first specify the type definitions needed
`to describe some components of the automaton. The ByteInt
`type is the set of pairs that has a byte as the first element, and
`an integer as the second element. The type Sbyte is the set
`of triples formed by a byte, an integer sequence number, and a
`Boolean flag. The type Blk is a pair of integers, and indicates
`the left and right edges of a block of data.
`The states of the sender includes
`which is a se-
`send_buf
`quence of bytes, and it holds data received from the user. The
`retransmission buffer,
`, holds data that may need
`retran_buf
`
`IPR2022-00833
`CommScope, Inc. Exhibit 1023
`Page 5 of 15
`
`

`

`198
`
`IEEE/ACM TRANSACTIONS ON NETWORKING, VOL. 10, NO. 2, APRIL 2002
`
`type Byteint = tuple of Msg: Byte, Seqnum: Int
`type Sbyte = tuple of Msg: Byte, Seqnum: Int, Flag: Bool
`type Blk = tuple of Left: Int, Right: Int
`
`automaton s
`
`signature
`Input send(m: Seq[Byte)), rcv-pktr.(ack: Int),
`rcv-pktr.(ack:Int, bl:Blk, b2:Blk, b3:Blk)
`Internal prepare-new-seg(s: Seq[Byte])
`prepare-retran-seg(s: Seq[Sbyte]), reset-sack
`output send-pkt•r (seg: Seq[Byteint])
`
`states
`sencl._buf: Seq[Byte) := {}
`retran_buf: Seq[Sbyte] := {}
`segment: Seq[Byteint] := {}
`sncLuna, snd_nxt: Int := 0
`ready_to_send: Bool := false
`
`transitions
`
`Input send(m)
`sencl._buf : = send...buf II m
`elf
`
`Internal prepare-new-seg(s)
`pre -, ready_to_send
`send...buf -::/= {}
`snd_nxt < sncLuna + WS
`s E prefixes ( send...buf)
`1 ::5 Isl :S min(MSS, sncLuna + WS - snd_nxt)
`send...buf : = tail ( sencl._buf, I s I )
`segment:= enum(s, sncLnxt)
`retranJmf := retran.Jmf II init_flag(segment)
`snd_nxt := snd_nxt + Isl
`ready_to_send := true
`
`elf
`
`output send-pkt.r(seg)
`pre ready_to_send
`seg = segment
`ready_to_send := false
`
`elf
`
`input rcv-pktr• (ack)
`if sncLuna < ack ::5 snd_nxt then
`elf
`retran_llUf := delete(retran_lmf, ack)
`sncLuna := ack fi
`
`input rcv-pktr• (ack, bl, b2, b3)
`if sncLuna < ack < sncLnxt then
`elf
`retran_buf := delete(retran_buf, ack)
`retran_buf := set_sack(retran_buf,bl,b2,b3)
`sncLuna := ack fi
`
`Internal prepare-retran-seg ( s)
`pre -, ready_to_send
`retran_lmf -::/= {}
`s E holes(retran.Jmf)
`::5 Isl :S MSS
`l
`elf segment:= remove_flag(s)
`ready_to_send :• true
`
`internal reset-sack
`pre true
`eff
`retran_buf := unsack(retran_buf)
`
`Fig. 6. SACK sender automaton.
`
`In TCP Reno, a segment is retransmitted if the retransmis-
`sion timeout expires, or a certain number of duplicate acknowl-
`edgments are received. In our model of the sender, we sim-
`plify the mechanism by allowing the sender to generate retrans-
`mission segments nondeterministically. Since the sender can
`nondeterministically choose between retransmitting a segment
`or sending a new one whenever it is enabled to send a seg-
`ment, our model accommodates the TCP Reno retransmission
`policy and any other implementation policy for retransmission.
`The internal action that generates retransmission segments is
`-
`-
`. Since the SACK protocol does not
`prepare retran seg(s)
`
`type Blk = tuple of Left: Int, Right: Int
`type Byteint = tup