123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912913914915916917918919920921922923924925926927928929930931932933934935936937938939940941942943944945946947948949950951952953954955956957958959960961962963964965966967968969970971972973974975976977978979980981982983984985986987988989990991992993994995996997998999100010011002100310041005100610071008100910101011101210131014101510161017101810191020102110221023102410251026102710281029103010311032103310341035103610371038103910401041104210431044104510461047104810491050105110521053105410551056105710581059106010611062106310641065106610671068106910701071107210731074107510761077107810791080108110821083108410851086108710881089109010911092109310941095109610971098109911001101110211031104110511061107110811091110111111121113111411151116111711181119112011211122112311241125112611271128112911301131113211331134113511361137113811391140114111421143114411451146114711481149115011511152115311541155115611571158115911601161116211631164116511661167116811691170117111721173117411751176117711781179118011811182118311841185118611871188118911901191119211931194119511961197(* (c) 2017-2019 Hannes Mehnert, all rights reserved *)letsrc=Logs.Src.create"tcp.input"~doc:"TCP input"moduleLog=(valLogs.src_logsrc:Logs.LOG)openStateletguardpe=ifpthenOk()elseErrorelet(let*)=Result.bind(* input rules from netsem
deliver_in_1 - passive open (listener, receive SYN) - handle_noconn
deliver_in_1b - drop bad for listening (listener, receive anything else) - handle_noconn
deliver_in_2 - active open (Syn_sent, receive SYN+ACK) - handle_conn
deliver_in_2a - bad or boring, RST or ignore (Syn_sent, receive RST) - handle_conn
deliver_in_2b - simultaneous open (Syn_sent, receive SYN) - handle_conn
deliver_in_3 - data, fin, ack in established - handle_conn
deliver_in_3a - data with invalid checksum - validate_segment fails
deliver_in_3b - data when process gone away - not handled
deliver_in_3c - stupid ack or land in (Syn_received + bad ACK) - handle_conn and validate_segment fails
deliver_in_3d - valid ack in (Syn_received + ACK -- normal 3WS) - handle_conn
????deliver_in_3y/z - fast path (Established, header prediction, (y) seq = rcv_nxt and data [delack] OR (z) ack [window update/opened ~> may send data])
deliver_in_4 - drop non-sane or martian segment - validate_segment fails
deliver_in_5 - drop with RST sth not matching any socket - handle_noconn
deliver_in_6 - drop sane segment in CLOSED - not handled (no CLOSED, handle_noconn may reset)
deliver_in_7 - recv RST and zap non-CLOSED/LISTEN/SYN_SENT/SYN_RECEIVED/TIME_WAIT - handle_conn
deliver_in_7a - recv RST and zap SYN_RECEIVED state
deliver_in_7b - recv RST and ignore in LISTEN
deliver_in_7c - recv RST and ignore in SYN_SENT/TIME_WAIT
deliver_in_7d - recv RST and zap SYN_SENT
deliver_in_8 - recv SYN in yy - handle_conn
deliver_in_9 - recv SYN in TIME_WAIT (in case there's no LISTEN) - not handled
??deliver_in_10 - stupid flag combinations are dropped (without reset)
*)letdropwithreset(src,_,dst,_)seg=Option.map(funx->src,dst,x)(Segment.dropwithresetseg)letdeliver_in_1mk_notifymstatsnowidseg=(* there's a difference from the model, namely that we don't care about
sockets in TIME_WAIT - this is handled in handle_conn explicitly (allowing
port reusage with strictly higher sequence numbers - RFC1122 4.2.2.13).
this rule carries less complexity in this way, and is called via
handle_noconn (if there's no flow in the connection table),
or via handle_conn if in time_wait, and a syn, and the seq > rcv_nxt. *)m"deliver-in-1";letconn=letadvmss=Subr.tcp_mssoptidinletrcvbufsize,sndbufsize,t_maxseg',snd_cwnd'=letbw_delay_product_for_rt=NoneinSubr.calculate_buf_sizesadvmss(Segment.mssseg)bw_delay_product_for_rtParams.so_rcvbufParams.so_sndbufinletrcv_wnd=rcvbufsizeinlettf_doing_ws,snd_scale=matchSegment.wssegwith|Somexwhenx<=Params.tcp_maxwinscale->true,x|_->false,0inletrequest_r_scale,rcv_scale=iftf_doing_wsthenSomeParams.scale,Params.scaleelseNone,0inletiss=Sequence.of_int32(Randomconv.int32Mirage_crypto_rng.generate)andack'=Sequence.incrseg.Segment.seq(* ACK the SYN *)inlett_rttseg=Some(now,iss)inletcontrol_block={initial_cbwithtt_rexmt=Subr.start_tt_rexmtnow0falseinitial_cb.t_rttinf;t_idletime=now;iss;irs=seg.Segment.seq;rcv_wnd=rcvbufsize;tf_rxwin0sent=(rcv_wnd=0);rcv_adv=Sequence.addiack'rcv_wnd;rcv_nxt=ack';snd_una=iss;snd_max=Sequence.incriss;snd_nxt=Sequence.incriss;snd_cwnd=snd_cwnd';t_maxseg=t_maxseg';t_advmss=advmss;tf_doing_ws;snd_scale;rcv_scale;request_r_scale;last_ack_sent=ack';t_rttseg}inconn_statenowmk_notify~rcvbufsize~sndbufsizeSyn_receivedcontrol_blockinletreply=Segment.make_syn_ackconn.control_blockidinLog.debug(funm->m"%a passive open %a"Connection.ppid(pp_conn_statenow)conn);Stats.incr_passivestats;conn,replyletdeliver_in_2mstatsnowidconnsegack=m"deliver-in-2";letcb=conn.control_blockinlet*()=guard(Sequence.equalackcb.snd_nxt)(`Drop(fun()->"ack = snd_nxt"))inlettf_doing_ws,snd_scale,rcv_scale=matchSegment.wsseg,cb.request_r_scalewith|None,_->false,0,0|Somex,Somey->true,x,y|Somex,None->(* may our 3rd time retransmitted SYN hits them, and we don't know what
we sent (use Params.scale for now) *)true,x,Params.scaleinletrcvbufsize,sndbufsize,t_maxseg,snd_cwnd=letbw_delay_product_for_rt=NoneinSubr.calculate_buf_sizescb.t_advmss(Segment.mssseg)bw_delay_product_for_rtconn.rcvbufsizeconn.sndbufsizeinletrcv_wnd=Subr.calculate_bsd_rcv_wndconninlett_softerror,t_rttseg,t_rttinf,tt_rexmt=(*: update RTT estimators from timestamp or roundtrip time :*)letemission_time=matchcb.t_rttsegwith|Some(ts0,seq0)whenSequence.greaterackseq0->Somets0|_->Nonein(*: clear soft error, cancel timer, and update estimators if we successfully timed a segment round-trip :*)lett_softerror',t_rttseg',t_rttinf'=matchemission_timewith|Somets->None,None,Subr.update_rtt(Mtime.spannowts)cb.t_rttinf|_->cb.t_softerror,cb.t_rttseg,cb.t_rttinfin(*: mess with retransmit timer if appropriate :*)lettt_rexmt'=ifSequence.equalackcb.snd_maxthen(*: if acked everything, stop :*)None(*: [[needoutput = 1]] -- see below :*)elsematchcb.tt_rexmtwith|Some((RexmtSyn,_),_)->(*: if partial ack, restart from current backoff value,
which is always zero because of the above updates to
the RTT estimators and shift value. :*)Subr.start_tt_rexmt_synnow0truet_rttinf'|None|Some((Rexmt,_),_)->(*: ditto :*)Subr.start_tt_rexmtnow0truet_rttinf'|Some((Persist,_),_)whenemission_time<>None->(* hannes 2019-07-15 looked a bit longer at the further conditionals,
and Persist when emission_time was the only case left (and now its
very symmetric...) *)Subr.start_tt_persistnow0t_rttinf'|c->cint_softerror',t_rttseg',t_rttinf',tt_rexmt'inletrcv_nxt=Sequence.incrseg.seqinletcontrol_block={cbwithtt_rexmt;t_idletime=now;tt_conn_est=None;tt_delack=None;snd_una=Sequence.incrcb.iss;(*: ack ; = cb.iss + 1, or +2 if full ack of SYN,FIN :*)snd_nxt=ifconn.cantsndmorethenackelsecb.snd_nxt;snd_max=ifconn.cantsndmore&&Sequence.greaterackcb.snd_maxthenackelsecb.snd_max;snd_wl1=Sequence.incrseg.seq;snd_wl2=ack;snd_wnd=seg.window;(* this is a SYN segment, so window scaling is ignored *)snd_cwnd;rcv_scale;snd_scale;tf_doing_ws;irs=seg.seq;rcv_nxt;rcv_wnd;tf_rxwin0sent=(rcv_wnd=0);rcv_adv=Sequence.addircv_nxt((Int.min(rcv_wndlsrrcv_scale)Params.tcp_maxwin)lslrcv_scale);t_maxseg;last_ack_sent=rcv_nxt;t_softerror;t_rttseg;t_rttinf;}inStats.incr_establishedstats;Ok({connwithcontrol_block;tcp_state=Established;rcvbufsize;sndbufsize},Segment.make_ackcontrol_block~fin:falseid)letdeliver_in_2amconnsegf=m"deliver-in-2a";(* well well, the remote could have leftover state and send us a ack+fin... but that's fine to drop (and unlikely to happen now that we have random)
server.exe: [DEBUG] 10.0.42.2:20 -> 10.0.42.1:1234 handle_conn TCP syn sent cb snd_una 0 snd_nxt 1 snd_wl1 0 snd_wl2 0 iss 0 rcv_wnd 65000 rcv_nxt 0 irs 0 seg AF seq 3062921918 ack 1 window 65535 opts 0 bytes data
server.exe: [ERROR] dropping segment in syn sent failed condition RA *)matchf,seg.Segment.ackwith|Some`Rst,Someack->ifSequence.equalackconn.control_block.snd_nxtthenOk()elseError(`Drop(fun()->"ACK in-window"))|_->Error(`Drop(fun()->"RA"))letdeliver_in_3c_3dmstatsnowconnseg=m"deliver-in-3c-3d";(* deliver_in_3c and syn_received parts of deliver_in_3 (now deliver_in_3d) *)(* TODO hostLTS:15801: [[SYN]] flag set may be set in the final segment of a
simultaneous open (does this change anything for us?) *)(* yes: seq may be cb.irs and flags = syn+ack (simultaneous open!) *)letcb=conn.control_blockin(* what is the current state? *)(* - we acked the initial syn, their seq should be rcv_nxt (or?) *)(* - furthermore, it should be >= irs -- that's redundant with above *)(* if their seq is good (but their ack isn't or it is no ack), reset *)let*()=guard(Sequence.equalseg.Segment.seqcb.rcv_nxt)(`Drop(fun()->"seq = rcv_nxt"))in(* - we sent our syn, so we expect an appropriate ack for the syn! *)(* - we didn't send out more data, so that ack should be exact *)(* if their seq is not good, drop packet -- TODO allow syn *)matchseg.Segment.flag,seg.Segment.ackwith|Some`Rst,_->Error(`Reset(fun()->"received valid reset"))|_,None->Error(`Drop(fun()->"ACK flag"))|Some_,_->Error(`Drop(fun()->"S|F"))|_,Someack->(* hostLTS:15828 - well, more or less ;) *)(* auxFns:2252 ack < snd_una || snd_max < ack -> break LAND DoS, prevent ACK storm *)(* TODO what is an acceptable ack? snd_nxt, if <> what to do? *)let*()=guard(Sequence.equalackcb.snd_nxt)(`Reset(fun()->"ack = snd_nxt"))in(* not (ack <= tcp_sock.cb.snd_una \/ ack > tcp_sock.cb.snd_max) *)(* TODO rtt measurement likely *)(* expect (assume for now): no data in that segment !? *)letcontrol_block={cbwithsnd_una=ack;snd_wnd=seg.Segment.windowlslcb.snd_scale;snd_wl1=seg.Segment.seq;(* need to check with model, from RFC1122 4.2.2.20 *)snd_wl2=ack;t_idletime=now;}in(* if not cantsendmore established else if ourfinisacked fin_wait2 else fin_wait_1 *)Stats.incr_establishedstats;Ok{connwithcontrol_block;tcp_state=Established}letin_windowcbseg=(* from table in 793bis13 3.3 *)letseq=seg.Segment.seqandmax=Sequence.addicb.rcv_nxtcb.rcv_wndinmatchseg.Segment.payload_len,cb.rcv_wndwith|0,0->Sequence.equalseqcb.rcv_nxt|0,_->Sequence.less_equalcb.rcv_nxtseq&&Sequence.lessseqmax|_,0->false|dl,_->letrseq=Sequence.addiseq(preddl)in(Sequence.less_equalcb.rcv_nxtseq&&Sequence.lessseqmax)||(Sequence.less_equalcb.rcv_nxtrseq&&Sequence.lessrseqmax)(* TODO are we missing (from di3_topstuff) the window probe
("segment_off_right_hand_edge" and rcv_wnd' is <> 0) *)letdi3_topstuffnowconn=(* we're not doing PAWS (no timestamp), and already checked in_window *)letrcv_wnd=Subr.calculate_bsd_rcv_wndconninletcb=conn.control_blockinlett_idletime=nowandtt_fin_wait_2=Option.map(fun_->Timers.timernow()Params.tcptv_maxidle)cb.tt_fin_wait_2in{cbwitht_idletime;tt_fin_wait_2;rcv_wnd}(* this is more or less andThen! (no bndlm though) *)let(>>>=)((conn,out),cont)f=ifcontthenlet(conn',out'),cont'=fconnin(conn',out@out'),cont'else(conn,out),contletdi3_newackstuffnowidconnourfinisackedack=(*: Pull some fields out of the segment :*)letcb=conn.control_blockinletconn',out=ifcb.t_dupacks<3then(*: If there have been fewer than 3 duplicate [[ACKS]] then clear the
duplicate [[ACK]] counter. If there were more than 3 duplicate [[ACKS]]
previously then the congestion window was inflated as per RFC2581 so
retract it to [[snd_ssthresh]]
-- hannes, 20231027: not needed to retract cwnd, since we do new reno,
and thus t_dupacks will never be >= 3 here :*)letcontrol_block={cbwitht_dupacks=0}in{connwithcontrol_block},[]elseifcb.t_dupacks>=3&&Sequence.lessackcb.snd_recoverthen(*: The host supports NewReno-style Fast Recovery, the socket has received
at least three duplicate [[ACK]]s previously and the new [[ACK]] does
not complete the recovery process, \ie, there are further losses or
network delays. The new [[ACK]] is a partial [[ACK]] per
RFC2582. Perform a retransmit of the next unacknowledged segment and
deflate the congestion window as per the RFC. :*)letsnd_nxt'=cb.snd_nxtinletcontrol_block={cbwith(*: Clear the retransmit timer and round-trip time measurement
timer. These will be started by [[tcp_output_really]] when the
retransmit is actioned. :*)tt_rexmt=None;t_rttseg=None;(*: Segment to retransmit starts here :*)snd_nxt=ack;(*: Allow one segment to be emitted :*)(* TODO hannes 2019-07-19 ABC? *)snd_cwnd=cb.t_maxseg}in(* Attempt to create a segment for output using the modified control block *)letconn',out=Segment.tcp_output_perhapsnowid{connwithcontrol_block}in(*: Finally update the control block: :*)letcb'=conn'.control_blockinletcontrol_block={cb'with(*: RFC2582 partial window deflation: deflate the congestion window by
the amount of data freshly acknowledged and add back one maximum
segment size :*)snd_cwnd=cb'.snd_cwnd-Sequence.windowackcb'.snd_una+cb'.t_maxseg;snd_nxt=snd_nxt'(*: restore previous value :*)}in{conn'withcontrol_block},outelseifcb.t_dupacks>=3&&Sequence.greater_equalackcb.snd_recoverthen(*: The host supports NewReno-style Fast Recovery, the socket has received
at least three duplicate [[ACK]] segments and the new [[ACK]]
acknowledges at least everything upto [[snd_recover]], completing the
recovery process. :*)letsnd_cwnd=ifSequence.windowcb.snd_maxack<cb.snd_ssthreshthen(*: If [[snd_ssthresh]] is greater than the number of bytes of data
still unacknowledged and presumed to be in-flight, set [[snd_cwnd]]
to be one segment larger than the total size of all the segments in
flight. This is burst avoidance: [[tcp_output]] is only able to
send upto one further segment until some of the in flight data is
acknowledged. :*)Sequence.windowcb.snd_maxack+cb.t_maxsegelse(*: Otherwise, set [[snd_cwnd]] to be [[snd_ssthresh]], forbidding any
further segment output until some in flight data is
acknowledged.:*)cb.snd_ssthreshinletcontrol_block={cbwitht_dupacks=0;(*: clear the duplicate [[ACK]] counter :*)(*: Open up the congestion window, being careful to avoid an RFC2582
Ch3.5 Pg6 "burst of data". :*)snd_cwnd}in{connwithcontrol_block},[]elseinvalid_arg"di3_newackstuff"(*: impossible :*)in(*: Check [[ack]] value is sensible, \ie, not greater than the highest
sequence number transmitted so far :*)ifSequence.greaterackcb.snd_maxthen(*: Drop the segment and possibly emit a [[RST]] segment :*)(* hannes 2019-07-19 dropafterack used to be called, which does:
- if state = SYN_RCVD and ACK and ack < snd_una || snd_max < ack
~> dropwithreset (break loop in LAND, prevent ACK storm from two
listening ports that have been sent forged SYN segments)
--> we're already post-SYN_RCVD here (3c_3d handles SYN_RCVD)
- else: tcp_output_really arch F ticks ifds sock (sock1,[msg])
so, this is very similar to a challenge ack, no? *)letconn'',out'=Segment.tcp_output_reallynowidfalseconn'in(Someconn'',out@[out']),falseelse(*: continue processing :*)(*: If the retransmit timer is set and the socket has done only one
retransmit and it is still within the bad retransmit timer window, then
because this is an [[ACK]] of new data the retransmission was done in
error. Flag this so that the control block can be recovered from
retransmission mode. This is known as a "bad retransmit". :*)letrevert_rexmt=(matchcb.tt_rexmtwith|Some((Rexmt,1),_)|Some((RexmtSyn,1),_)->true|_->false)(* /\ timewindow_open cb'.t_badrxtwin) *)in(*: Attempt to calculate a new round-trip time estimate :*)letemission_time=matchcb.t_rttsegwith|Some(ts0,seq0)->(*: Or if not, by the control blocks round-trip timer, if it covers the
segment(s) being acknowledged :*)ifSequence.greaterackseq0thenSomets0elseNone|None->(*: Otherwise, it is not possible to calculate a round-trip update :*)Nonein(*: If a new round-trip time estimate was calculated above, update the round-trip information
held by the socket's control block :*)lett_rttinf'=matchemission_timewith|Somets->Subr.update_rtt(Mtime.spannowts)cb.t_rttinf|None->cb.t_rttinfin(*: Update the retransmit timer :*)lettt_rexmt'=ifSequence.equalackcb.snd_maxthenNone(*: If all sent data has been acknowledged, disable the timer :*)elsematchmode_ofcb.tt_rexmtwith|None->(*: If not set, set it as there is still unacknowledged data :*)Subr.start_tt_rexmtnow0truet_rttinf'|SomeRexmt->(*: If set, reset it as a new acknowledgement segment has arrived :*)Subr.start_tt_rexmtnow0truet_rttinf'|_->(*: Otherwise, leave it alone. The timer will never be in [[RexmtSyn]]
here and the only other case is [[Persist]], in which case it
should be left alone until such time as a window update is received
:*)cb.tt_rexmtin(*: Update the send queue and window :*)letsnd_wnd',sndq=ifourfinisackedthen(*: If this socket has previously emitted a [[FIN]] segment and the
[[FIN]] has now been [[ACK]]ed, decrease [[snd_wnd]] by the length of
the send queue and clear the send queue.:*)cb.snd_wnd-Rope.lengthconn.sndq,Rope.emptyelse(*: Otherwise, reduce the send window by the amound of data acknowledged
as it is now consuming space on the receiver's receive queue. Remove
the acknowledged bytes from the send queue as they will never need to
be retransmitted.:*)letacked=Sequence.windowackcb.snd_unaincb.snd_wnd-acked,Rope.shiftconn.sndqackedin(*: Update the control block :*)letcb'=ifrevert_rexmtthen(*: If [[revert_rexmt]] (above) flags that a bad retransmission occured,
undo the congestion avoidance changes :*)letcb=conn'.control_blockin{cbwithsnd_cwnd=cb.snd_cwnd_prev;snd_ssthresh=cb.snd_ssthresh_prev;snd_nxt=cb.snd_max;(* t_badrxtwin = TimeWindowClosed ; *)}elseconn'.control_blockinlett_softerror,t_rttseg=(*: If the [[ACK]] segment allowed us to successfully time a segment (and
update the round-trip time estimates) then clear the soft error flag
and clear the segment round-trip timer in order that it can be used on
a future segment. :*)matchemission_timewith|None->cb'.t_softerror,cb'.t_rttseg|Some_->None,Noneandsnd_cwnd=(*: Update the congestion window by the algorithm in {@link
[[expand_cwnd]]} only when not performing NewReno retransmission or the
duplicate [[ACK]] counter is zero, \ie, expand the congestion window
when this [[ACK]] is not a NewReno-style partial [[ACK]] and hence the
connection has yet recovered :*)ifcb'.t_dupacks=0then(* TODO cb unclear, some used to be tcp_sock0.cb *)Subr.expand_cwndcb.snd_ssthreshcb.t_maxseg(Params.tcp_maxwinlslcb.snd_scale)cb.snd_cwndelsecb'.snd_cwndandtt_2msl=(*: Reset the [[2MSL]] timer if in the [[TIME_WAIT]] state as have
received a valid [[ACK]] segment for the waiting socket :*)matchconn'.tcp_statewith|Time_wait->Some(Timers.timernow()(Int64.shift_leftParams.tcptv_msl1))|_->cb'.tt_2msl(* should be equivalent to None *)inletcb''={cb'with(*: Update the round-trip time estimates and retransmit timer :*)t_rttinf=t_rttinf';tt_rexmt=tt_rexmt';t_softerror;t_rttseg;snd_cwnd;snd_wnd=snd_wnd';(*: The updated send window :*)snd_una=ack;(*: Have had up to [[ack]] acknowledged :*)snd_nxt=maxackcb'.snd_nxt;(*: Ensure invariant [[snd_nxt >= snd_una]] :*)tt_2msl}in(*: The send queue update :*)letconn''={conn'withcontrol_block=cb'';sndq}inmatchconn''.tcp_statewith|Last_ackwhenourfinisacked->(* If the socket's [[FIN]] has been acknowledged and the socket is in the
[[LAST_ACK]] state, close the socket and stop processing this segment *)(None,[]),false|Time_waitwhenSequence.greaterackcb.snd_una->(* hannes check which cb! *)(* data acked past FIN *)(*: If the socket is in [[TIME_WAIT]] and this segment contains a new
acknowledgement (that acknowledges past the [[FIN]] segment, drop
it---it's invalid. Stop processing. :*)letconn''',out'=Segment.tcp_output_reallynowidfalseconn''in(Someconn''',out@[out']),false|_->(*: Otherwise, flag that [[deliver_in_3]] can continue processing the
segment if need be :*)(Someconn'',out),trueletdi3_ackstuffnowidconnsegourfinisackedfinack=letcb=conn.control_blockinletwin=seg.Segment.windowlslcb.snd_scalein(*: The segment is possibly a duplicate ack if it contains no data, does not
contain a window update and the socket has unacknowledged data (the
retransmit timer is still active). The no data condition is important: if
this socket is sending little or no data at present and is waiting for some
previous data to be acknowledged, but is receiving data filled segments
from the other end, these may all contain the same acknowledgement number
and trigger the retransmit logic erroneously. :*)letmaybe_dup_ack=seg.payload_len=0&&win=cb.snd_wnd&&matchcb.tt_rexmtwithSome((Rexmt,_),_)->true|_->falsein(* It turns out since some time the first FIN(+ACK) doesn't account for
dupacks this is simultaneous close, see rev261244 (and rev239672 and
rev258821) for details *)ifSequence.less_equalackcb.snd_una&&maybe_dup_ack&&fin&&matchconn.tcp_statewithClose_wait|Closing|Last_ack|Time_wait->false|_->truethenletcontrol_block={cbwitht_dupacks=0}in(Some{connwithcontrol_block},[]),trueelseifSequence.less_equalackcb.snd_una&&maybe_dup_ackthen(*: Received a duplicate acknowledgement: it is an old acknowledgement
(strictly less than [[snd_una]]) and it meets the duplicate
acknowledgement conditions above. Do Fast Retransmit/Fast Recovery
Congestion Control (RFC2581 Ch3.2 Pg6) and NewReno-style Fast Recovery
(RFC2582, Ch3 Pg3), updating the control block variables and creating
segments for transmission as appropriate. :*)lett_dupacks'=cb.t_dupacks+1inift_dupacks'<3then(*: Fewer than three duplicate acks received so far. Just increment the
duplicate ack counter. We must continue processing, in case [[FIN]] is
set. :*)letcontrol_block={cbwitht_dupacks=t_dupacks'}in(Some{connwithcontrol_block},[]),trueelseift_dupacks'>3||(t_dupacks'=3&&Sequence.lessackcb.snd_recover)then(*: If this is the 4th or higher duplicate [[ACK]] then Fast
Retransmit/Fast Recovery congestion control is already in progress.
Increase the congestion window by another maximum segment size (as the
duplicate [[ACK]] indicates another out-or-order segment has been
received by the other end and is no longer consuming network resource),
increment the duplicate [[ACK]] counter, and attempt to output another
segment. :*)(*: If this is the 3rd duplicate [[ACK]], the host supports NewReno
extensions and [[ack]] is strictly less than the fast recovery
"recovered" sequence number [[snd_recover]], then the host is already
doing NewReno-style fast recovery and has possibly falsely
retransmitted a segment, the retransmitted segment has been lost or it
has been delayed. Reset the duplicate [[ACK]] counter, increase the
congestion window by a maximum segment size (for the same reason as
before) and attempt to output another segment. NB: this will not cause
a cycle to develop! The retransmission timer will eventually fire if
recovery does not happen "fast". :*)lett_dupacks=ift_dupacks'=3then0(* false retransmit, or further loss or delay *)elset_dupacks'andsnd_cwnd=cb.snd_cwnd+cb.t_maxsegin(* TODO hannes 2019-07-19 increment by cb.t_maxseg changes due to ABC *)letcontrol_block={cbwitht_dupacks;snd_cwnd}inletconn'={connwithcontrol_block}inletconn'',out=Segment.tcp_output_perhapsnowidconn'in(Someconn'',out),falseelseift_dupacks'=3&¬(Sequence.lessackcb.snd_recover)then(*: If this is the 3rd duplicate segment and if the host supports NewReno
extensions, a NewReno-style Fast Retransmit is not already in progress,
then do a Fast Retransmit :*)(*: Update the control block before the retransmit to reflect which data
requires retransmission :*)letsnd_ssthresh=(*: Set to half the current flight size as per RFC2581/2582 :*)(* TODO hannes still true in respect of ABC? *)Int.max2((Int.mincb.snd_wndcb.snd_cwnd)/2/cb.t_maxseg)*cb.t_maxseginletcontrol_block={cbwitht_dupacks=t_dupacks';snd_ssthresh;snd_recover=cb.snd_max;(*: Clear the retransmit timer and round-trip time measurement
timer. These will be started by [[tcp_output_really]] when
the retransmit is actioned. :*)tt_rexmt=None;t_rttseg=None;(*: Sequence number to retransmit---this is equal to the [[ack]]
value in the duplicate [[ACK]] segment :*)snd_nxt=ack;(*: Ensure the congestion window is large enough to allow one
segment to be emitted :*)snd_cwnd=cb.t_maxseg}in(*: Attempt to create a segment for output using the modified control
block (this is all a relational monad idiom) :*)letconn'={connwithcontrol_block}inletconn'',out=Segment.tcp_output_perhapsnowidconn'in(*: Finally, update the congestion window to [[snd_ssthresh]] plus 3
maximum segment sizes (this is the artificial inflation of RFC2581/2582
because it is known that the 3 segments that generated the 3 duplicate
acknowledgments are received and no longer consuming network
resource. Also put [[snd_nxt]] back to its previous value. :*)letcontrol_block={conn''.control_blockwithsnd_cwnd=control_block.snd_ssthresh+cb.t_maxseg*t_dupacks';snd_nxt=Sequence.maxcb.snd_nxtcontrol_block.snd_nxt}in(Some{conn''withcontrol_block},out),falseelseinvalid_arg"di3_ackstuff"(*: Believed to be impossible---here for completion and safety :*)elseifSequence.less_equalackcb.snd_una&¬maybe_dup_ackthen(*: Have received an old (would use the word "duplicate" if it did not have
a special meaning) [[ACK]] and it is neither a duplicate [[ACK]] nor the
[[ACK]] of a new sequence number thus just clear the duplicate [[ACK]]
counter. :*)letcontrol_block={cbwitht_dupacks=0}in(Some{connwithcontrol_block},[]),trueelse(*: Must be: [[ack > cb.snd_una]] :*)(*: This is the [[ACK]] of a new sequence number---this case is handled by
the auxiliary function {@link [[di3_newackstuff]]} :*)di3_newackstuffnowidconnourfinisackedackletdi3_datastuff_reallynowthe_ststuffconnseg_bsd_fast_pathourfinisackedfin=(* hannes 2019-07-19: there used to be let seq = seg.seq + if SYN then 1 else
0, but we'll never execute this code with a segment that has SYN *)(* hannes 2023-08-28: this used to compute the sender's advertised window and
shift by scale, but that value was never used. *)letcb=conn.control_blockin(*: Trim segment to be within the receive window :*)(*: Trim duplicate data from the left edge of [[data]], \ie, data before
[[cb.rcv_nxt]]. Adjust [[seq]], [[URG]] and [[urp]] in respect of left
edge trimming. If the urgent data has been trimmed from the segment's data,
[[URG]] is cleared also. Note: the urgent pointer always points to the
byte immediately following the urgent byte and is relative to the start of
the segment's data. An urgent pointer of zero signifies that there is no
urgent data in the segment. :*)lettrim_amt_left=ifSequence.greatercb.rcv_nxtseg.Segment.seqthenInt.min(Sequence.windowcb.rcv_nxtseg.seq)seg.payload_lenelse0inletdata_trimmed_left=Rope.of_stringsseg.payloadinletdata_trimmed_left=Rope.shiftdata_trimmed_lefttrim_amt_leftinletseq_trimmed=Sequence.addiseg.seqtrim_amt_leftin(*: Trimmed data starts at [[seq_trimmed]] :*)(*: Trim any data outside the receive window from the right hand edge. If all
the data is within the window and the [[FIN]] flag is set then the [[FIN]]
flag is valid and should be processed. Note: this trimming may remove
urgent data from the segment. The urgent pointer and flag are not cleared
here because there is still urgent data to be received, but now in a future
segment. :*)letdata_trimmed_left_right=letlen=Int.mincb.rcv_wnd(Rope.lengthdata_trimmed_left)inRope.chopdata_trimmed_leftleninletfin_trimmed=fin&&Rope.lengthdata_trimmed_left_right==Rope.lengthdata_trimmed_leftin(*: Build trimmed segment to place on reassembly queue. If urgent data is in
this segment and the socket is not doing inline delivery (and hence the
urgent byte is stored in [[iobc]]), remove the urgent byte from the
segment's data so that it does not get placed in the receive queue, and set
[[spliced_urp]] to the sequence number of the urgent byte. :*)(*: Processing of non-urgent data. There are 6 cases to consider: :*)(*: Case (1) The segment contains new in-order, in-window data possibly with a
[[FIN]] and the receive window is not closed. Note: it is possible that the
segment contains just one byte of OOB data that may have already been
pulled out into [[iobc]] if OOB delivery is out-of-line. In which case, the
below must still be performed even though no data is contributed to the
reassembly buffer in order that [[rcv_nxt]] is updated correctly (because a
byte of urgent data consumes a byte of sequence number space). This is why
[[data_trimmed_left_right]] is used rather than [[data_deoobed]] in some of
the conditions below. :*)letrseq_trimmed=Sequence.addiseq_trimmed(Rope.lengthdata_trimmed_left_right+(iffin_trimmedthen1else0))inlet(conn',fin_reass,out),cont=ifSequence.equalseq_trimmedcb.rcv_nxt&&Sequence.greaterrseq_trimmedcb.rcv_nxt&&cb.rcv_wnd>0then(*: Only need to acknowledge the segment if there is new in-window data
(including urgent data) or a valid [[FIN]] :*)lethave_stuff_to_ack=Rope.lengthdata_trimmed_left_right>0||fin_trimmedin(*: If the socket is connected, has data to [[ACK]] but no [[FIN]] to
[[ACK]], the reassembly queue is empty, the socket is not currently
within a bad retransmit window and an [[ACK]] is not already being
delayed, then delay the [[ACK]]. :*)letdelay_ack=is_connectedconn.tcp_state&&have_stuff_to_ack&¬fin_trimmed&&Reassembly_queue.is_emptycb.t_segq&¬cb.tf_rxwin0sent&&cb.tt_delack=Nonein(*: Check to see whether any data or a [[FIN]] can be
reassembled. hannes (2023-08-30 nothing non-deterministically here,
also not dealing with oob (as does this stack) :*)lett_segq,r=Reassembly_queue.maybe_takecb.t_segqrseq_trimmedin(* Length (in sequence space) of reassembled data, counting a [[FIN]] as
one byte and including any out-of-line urgent data previously removed *)letdata_reass,fin_reass0=Option.value~default:(Rope.empty,false)rinletdata=Rope.concatdata_trimmed_left_rightdata_reassinletfin_reass_trimmed=fin_trimmed||fin_reass0inletdata_len=Rope.lengthdata+iffin_reass_trimmedthen1else0in(*: Add the reassembled data to the receive queue and increment [[rcv_nxt]]
to mark the sequence number of the byte past the last byte in the
receive queue:*)(*: Prune the receive queue of any data or [[FIN]]s that were reassembled,
keeping all segments that contain data at or past sequence number
[[cb.rcv_nxt + len_reass]]. :*)(*: Reduce the receive window in light of the data added to the receive
queue. Do not include out-of-line urgent data because it does not store
data in the receive queue. :*)(*: Hack: assertion used to share values with later conditions :*)(* assert (FIN_reass = FIN_reass0) andThen *)(*: Update the socket state :*)lettt_delack=(*: Start the delayed ack timer if decided to earlier, \ie, [[delay_ack = T]]. :*)ifdelay_ackthenSome(Timers.timernow()Params.tcptv_delack)elseNoneandtf_shouldacknow=(*: Set if not delaying an [[ACK]] and have stuff to [[ACK]] :*)notdelay_ack&&have_stuff_to_ackandrcv_nxt=Sequence.addicb.rcv_nxtdata_lenandrcv_wnd=cb.rcv_wnd-(Rope.lengthdata)inletcontrol_block={cbwithtt_delack;tf_shouldacknow;t_segq;(*: updated reassembly queue, post-pruning :*)rcv_nxt;rcv_wnd;}andrcvq=Rope.concatconn.rcvqdatain({connwithcontrol_block;rcvq},fin_reass_trimmed,[]),true(*: Case (2) The segment contains new out-of-order in-window data, possibly
with a [[FIN]], and the receive window is not closed. Note: it may also
contain in-window urgent data that may have been pulled out-of-line but
still require processing to keep reassembly happy. :*)elseifSequence.greaterseq_trimmedcb.rcv_nxt&&Sequence.lessseq_trimmed(Sequence.addicb.rcv_nxtcb.rcv_wnd)&&Rope.lengthdata_trimmed_left_right+(iffin_trimmedthen1else0)>0&&cb.rcv_wnd>0then(*: Hack: assertion used to share values with later conditions :*)letfin_reass=falsein(* it is out-of-order *)(*: Update the socket's TCP control block state :*)lett_segq=Reassembly_queue.insert_segcb.t_segq(seq_trimmed,fin_trimmed,data_trimmed_left_right)inletcontrol_block={cbwithtf_shouldacknow=true;t_segq}in(* since it is out-of-order, we do not (yet) handle the fin *)({connwithcontrol_block},fin_reass,[]),true(*: Case (3) The segment is a pure [[ACK]] segment (contains no data) (and
must be in-order). :*)(*: Invariant here that [[seq_trimmed = seq]] if segment is a pure
[[ACK]]. Note: the length of the original segment (not the trimmed
segment) is used in the guard to ensure this really was a pure [[ACK]]
segment. :*)elseifSequence.equalseq_trimmedcb.rcv_nxt&&seg.payload_len+(iffinthen1else0)=0then(*: Hack: assertion used to share values with later conditions :*)letfin_reass=falsein(* Have not received a FIN *)(conn,fin_reass,[]),true(*: Case (4) Segment contained no useful data---was a completely old
segment. Note: the original fields from the segment, \ie, [[seq]],
[[data]] and [[FIN]] are used in the guard below---the trimmed variants
are useless here! :*)(*: Case (5) Segment is a window probe. Note: the original fields from
the segment, \ie, [[data]] and [[FIN]] are used in the guard
below---the trimmed variants are useless here! :*)(*: Case (6) Segment is completely beyond the window and is not a window
probe :*)else(* hannes 2023-08-29 since the last case is "true", skip the conditional.
no need to evaluate any conditions with a "|| true" at the end *)(* if
(Sequence.less seg.seq cb.rcv_nxt &&
Sequence.less_equal (Sequence.addi seg.seq (Cstruct.length seg.payload + if fin_trimmed then 1 else 0)) cb.rcv_nxt) || (* (4) *)
(Sequence.equal seq_trimmed cb.rcv_nxt && cb.rcv_wnd = 0 &&
Cstruct.length seg.payload + (if fin then 1 else 0) > 0) || (* (5) *)
true (* uhm, really? (6) *)
then *)(*: Update socket's control block to assert that an [[ACK]] segment should be sent now. :*)(*: Source: TCPIPv2p959 says "segment is discarded and an ack is sent as a reply" :*)(*: Hack: assertion used to share values with later conditions :*)letfin_reass=falsein(* Definitely false---segment is outside window *)letcontrol_block={cbwithtf_shouldacknow=true}in({connwithcontrol_block},fin_reass,[]),truein(*: Finished processing the segment's data :*)(*: Thread the reassembled [[FIN]] flag through to [[di3_ststuff]] :*)ifcontthenthe_ststuffnowconn'fin_reassourfinisacked,outelseconn',outletdi3_datastuffnowthe_ststuffconnsegourfinisackedfinack=letcb=conn.control_blockinletwin=seg.Segment.windowlslcb.snd_scalein(*: Various things do not happen if BSD processes the segment using its header
prediction (fast-path) code. Header prediction occurs only in the
[[ESTABLISHED]] state, with segments that have only [[ACK]] and/or [[PSH]]
flags set, are in-order, do not contain a window update, when data is not
being retransmitted (no congestion is occuring) and either:
(a) the segment is a valid pure ACK segment of new data, less than
three duplicate [[ACK]]s have been received and the congestion window is at
least as large as the send window, or
(b) the segment contains new data, does not acknowlegdge any new data,
the segment reassembly queue is empty and there is space for the segment's
data in the socket's receive buffer. :*)letbsd_fast_path=(matchconn.tcp_statewithEstablished->true|_->false)&¬fin&&Sequence.equalseg.seqcb.rcv_nxt&&cb.snd_wnd=win&&Sequence.equalcb.snd_maxcb.snd_nxt&&((Sequence.greaterackcb.snd_una&&Sequence.less_equalackcb.snd_max&&cb.snd_cwnd>=cb.snd_wnd&&cb.t_dupacks<3)||(Sequence.equalackcb.snd_una&&Reassembly_queue.is_emptycb.t_segq&&seg.payload_len<conn.rcvbufsize-Rope.lengthconn.rcvq))in(*: Update the send window using the received segment if the segment will not be processed by
BSD's fast path, has the [[ACK]] flag set, is not to the right of the window, and either:
(a) the last window update was from a segment with sequence number less than [[seq]],
\ie, an older segment than the current segment, or
(b) the last window update was from a segment with sequence number equal to [[seq]] but
with an acknowledgement number less than [[ack]], \ie, this segment acknowledges
newer data than the segment the last window update was taken from, or
(c) the last window update was from a segment with sequence number equal to
[[seq]] and acknowledgement number equal to [[ack]], \ie, a segment similar to that
the previous update came from, but this segment contains a larger window advertisment
than was previously advertised, or
(d) this segment is the third segment during connection establishement (state is
[[SYN_RECEIVED]]) and does not have the [[FIN]] flag set. :*)letupdate_send_window=notbsd_fast_path&&Sequence.less_equalseg.seq(Sequence.addicb.rcv_nxtcb.rcv_wnd)&&(Sequence.lesscb.snd_wl1seg.seq||(Sequence.equalcb.snd_wl1seg.seq&&(Sequence.lesscb.snd_wl2ack||Sequence.equalcb.snd_wl2ack&&win>cb.snd_wnd)))inletseq_trimmed=Sequence.maxseg.seq(Sequence.mincb.rcv_nxt(Sequence.addiseg.seqseg.payload_len))in(*: Write back the window updates :*)letcontrol_block=ifupdate_send_windowthen{cbwithsnd_wnd=win;snd_wl1=seq_trimmed;snd_wl2=ack;}elsecb(*: persist timer will be set by [[deliver_out_1]] if this updates the
window to zero and there is data to send :*)inletconn'={connwithcontrol_block}in(*: If in [[TIME_WAIT]] or will transition to it from [[CLOSING]], ignore any
URG, data, or FIN. Note that in [[FIN_WAIT_1]] or [[FIN_WAIT_2]], we still
process data, even if [[ourfinisacked]]. :*)ifconn'.tcp_state=Time_wait||(conn'.tcp_state=Closing&&ourfinisacked)thenthe_ststuffnowconn'falseourfinisacked,[]elsedi3_datastuff_reallynowthe_ststuffconn'segbsd_fast_pathourfinisackedfinletdi3_ststuffidnowconnrcvd_finourfinisacked=letconn'=ifrcvd_finthen{connwithcantrcvmore=true}elseconninletenter_time_wait=letcontrol_block={conn'.control_blockwithtt_2msl=Some(Timers.timernow()(Int64.shift_leftParams.tcptv_msl1));tt_rexmt=None;tt_delack=None;tt_conn_est=None;tt_fin_wait_2=None;}in{conn'withtcp_state=Time_wait;control_block}andstatetcp_state={conn'withtcp_state}inmatchconn.tcp_state,rcvd_finwith|Established,false->conn'|Established,true->stateClose_wait|Close_wait,_->conn'|Fin_wait_1,falsewhenourfinisacked->letconn'=stateFin_wait_2inletcontrol_block=lettt_fin_wait_2=ifconn'.cantrcvmorethenSome(Timers.timernow()Params.tcptv_maxidle)elseNonein{conn'.control_blockwithtt_fin_wait_2}in{conn'withcontrol_block}|Fin_wait_1,false->conn'|Fin_wait_1,truewhenourfinisacked->enter_time_wait|Fin_wait_1,true->stateClosing|Fin_wait_2,false->conn'|Fin_wait_2,true->enter_time_wait|Closing,_whenourfinisacked->enter_time_wait|Closing,_->conn'|Last_ack,false->conn'|Last_ack,true->Log.warn(funm->m"Last_ack and we received a fin on %a"Connection.ppid);(* let's avoid assert false here *)conn'|Time_wait,_->enter_time_wait|x,f->Log.warn(funm->m"%a on %a, received fin? %B"pp_fsmxConnection.ppidf);(* avoid assert false *)conn'letdeliver_in_3mnowidconnsegflagack=m"deliver-in-3";(* we expect at most FIN PSH ACK - we drop with reset all other combinations *)let*()=guard(flag=None||flag=Some`Fin)(`Reset(fun()->"flags ACK | FIN & ACK"))inletfin=flag=Some`Finin(* PAWS, timers, rcv_wnd may have opened! updates fin_wait_2 timer *)letcb=conn.control_blockinletwesentafin=Sequence.greatercb.snd_max(Sequence.addicb.snd_una(Rope.lengthconn.sndq))inletourfinisacked=wesentafin&&Sequence.greater_equalackcb.snd_maxinletcontrol_block=di3_topstuffnowconnin(* ACK processing *)let(conn',outs),cont=di3_ackstuffnowid{connwithcontrol_block}segourfinisackedfinackin(* may have some fresh data to report which needs to be acked *)Option.fold~none:(Ok(None,[]))~some:(funconn'->letconn'',outs'=ifcontthendi3_datastuffnow(di3_ststuffid)conn'segourfinisackedfinackelse(conn',[])inletout=outs@outs'inOk(Someconn'',out))conn'letdeliver_in_7midconnseg=m"deliver-in-7";letcb=conn.control_blockinifSequence.equalcb.rcv_nxtseg.Segment.seqthen(* we rely that dropwithreset does not RST if a RST was received *)Error(`Reset(fun()->"received valid reset"))elseOk(Segment.make_ackcb~fin:falseid)letdeliver_in_8midconn_seg=m"deliver-in-8";Ok(Segment.make_ackconn.control_block~fin:falseid)lethandle_noconntnowidseg=letm=ruletinmatch(* TL;DR: if there's a listener, and it is a SYN, we do sth useful. otherwise RST *)IS.memseg.Segment.dst_portt.listeners,seg.Segment.flag=Some`Syn&&seg.Segment.ack=None(* deliver_in_1 - passive open *)with|true,true->(* there can't be anything in TIME_WAIT, otherwise we wouldn't end up here *)letconn,reply=deliver_in_1t.mk_notifymt.statsnowidsegin{twithconnections=CM.addidconnt.connections},[reply]|true,false->(* deliver_in_1b *)m"deliver-in-1b";letout=Option.map(fun_ack->dropwithresetidseg)seg.Segment.ackint,Option.to_list(Option.joinout)|false,syn->m"deliver-in-5-6";Log.debug(funm->m"%a dropping segment with reset (SYN %B) %a"Connection.ppidsynSegment.ppseg);(* deliver_in_5 / deliver_in_6 *)t,Option.to_list(dropwithresetidseg)lethandle_conntnowidconnseg=letm=ruletinLog.debug(funm->m"%a handle_conn %a@ seg %a"Connection.ppid(pp_conn_statenow)connSegment.ppseg);letaddconn'=Log.debug(funm->m"%a now %a"Connection.ppid(pp_conn_statenow)conn');{twithconnections=CM.addidconn't.connections}anddrop()=Log.debug(funm->m"%a dropped"Connection.ppid);{twithconnections=CM.removeidt.connections}inletr=matchconn.tcp_statewith|Syn_sent->beginmatchseg.Segment.ack,seg.Segment.flagwith|Someack,Some`Syn->let*c',o=deliver_in_2mt.statsnowidconnsegackinOk(addc',[o])|None,Some`Syn->(* simultaneous open: accept anything, send syn+ack *)(* let* c', o = deliver_in_2b now id conn seg in *)m"deliver_in_2b";Ok(drop(),[])|_,((None|Some`Rst|Some`Fin)asf)->let*()=deliver_in_2amconnsegfinOk(drop(),[])end|Syn_received->(* expected is:
- ACK with proper seg (3d) ~> ok established
- stupid ACK 3c -> drop
- RST (=rcv_nxt) 7a -> zap
- RST 7e -> drop
- RST in-window -> challenge-ack
may hit as well (ignore):
- FIN [grmbl - just not ack it, will then be handled in established]
- SYN (simultaneous open..)
model uses di_3 (there's no separate 3d)
according to 793, once simultaneous open ends us in syn_received, that
even may emit syn+ack (with seq = iss) to move forward [but then, as
well just an ack is possible with seq = iss + 1]
*)let*conn'=deliver_in_3c_3dmt.statsnowconnseginOk(addconn',[])|Time_waitwhenseg.Segment.flag=Some`Syn&&seg.Segment.ack=None&&IS.memseg.Segment.dst_portt.listeners&&Sequence.lessconn.control_block.rcv_nxtseg.Segment.seq->(* RFC1122 4.2.2.13:
When a connection is closed actively, it MUST linger in
TIME-WAIT state for a time 2xMSL (Maximum Segment Lifetime).
However, it MAY accept a new SYN from the remote TCP to
reopen the connection directly from TIME-WAIT state, if it:
(1) assigns its initial sequence number for the new
connection to be larger than the largest sequence
number it used on the previous connection incarnation,
and
(2) returns to TIME-WAIT state if the SYN turns out to be
an old duplicate.
*)(* model - hostLTSScript:14701 (deliver_in_1):
If another socket in the [[TIME_WAIT]] state matches the address quad of the SYN segment
then only proceed with the new incoming connection attempt if the sequence number of the
segment [[seq]] is strictly greater than the next expected sequence number on the
[[TIME_WAIT]] socket, [[rcv_nxt]]. This prevents old or duplicate SYN segments from previous
incarnations of the connection from inadvertently creating new connections.
Note: this models the behaviour in RFC1122 Section 4.2.2.13 which states that a new [[SYN]]
with a sequence number larger than the maximum seen in the last incarnation may reopen the
connection, \ie, reuse the socket for the new connection changing out of the [[TIME_WAIT]]
state. This is modelled by closing the existing [[TIME_WAIT]] socket and creating the new
socket from scratch.
*)letconn,reply=deliver_in_1t.mk_notifymt.statsnowidseginOk({twithconnections=CM.addidconnt.connections},[reply])|_->ifnot(in_windowconn.control_blockseg)thenifseg.Segment.flag=Some`RstthenError(`Drop(fun()->Fmt.str"RST out of window seq %a rcv_nxt %a"Sequence.ppseg.Segment.seqSequence.ppconn.control_block.rcv_nxt))elsebegin(* RFC9293 3.10.7.4 (Other states, [_]):
If an incoming segment is not acceptable, an acknowledgment should
be sent in reply (unless the RST bit is set, if so drop the segment
and return):
<SEQ=SND.NXT><ACK=RCV.NXT><CTL=ACK> *)Log.debug(funm->m"%a unacceptable segment seq %a seql %u rcv_nxt %a rcv_wnd %u, acking"Connection.ppidSequence.ppseg.Segment.seqseg.payload_lenSequence.ppconn.control_block.rcv_nxtconn.control_block.rcv_wnd);letcontrol_block={conn.control_blockwithtf_shouldacknow=true}inletconn'={connwithcontrol_block}inletconn',out=Segment.tcp_output_perhapsnowidconn'inOk(addconn',out)endelse(* RFC5961: challenge acks for SYN and (RST where seq != rcv_nxt), keep state *)matchseg.Segment.flag,seg.Segment.ackwith|Some`Rst,_->let*seg'=deliver_in_7midconnseginOk(t,[seg'])|Some`Syn,_->let*seg'=deliver_in_8midconnseginOk(t,[seg'])|_,None->Error(`Drop(fun()->"no ACK"))|f,Someack->let*conn',out=deliver_in_3mnowidconnsegfackinmatchconn'with|None->Ok(drop(),[])|Someconn'->letconn'',out'=matchoutwith|[]->Segment.tcp_output_perhapsnowidconn'|x->conn',xinOk(addconn'',out')inmatchrwith|Ok(t,a)->t,a|Error(`Dropmsg)->Log.debug(funm->m"%a dropping segment in %a failed condition %s"Connection.ppidpp_fsmconn.tcp_state(msg()));t,[]|Error(`Resetmsg)->Log.debug(funm->m"%a reset in %a %s"Connection.ppidpp_fsmconn.tcp_state(msg()));drop(),Option.to_list(dropwithresetidseg)lethandle_segmenttnowidseg=Log.debug(funm->m"%a TCP %a"Connection.ppidSegment.ppseg);lett',out=matchCM.find_optidt.connectionswith|None->handle_noconntnowidseg|Someconn->handle_conntnowidconnsegint',outlethandle_buftnow~src~dstdata=matchSegment.decode_and_validate~src~dstdatawith|Error(`Msgmsg)->Log.debug(funm->m"dropping invalid segment %s"msg);t,[],[]|Ok(seg,id)->Tracing.debug(funm->m"%a [%a] handle_buf %u %s"Connection.ppidMtime.ppnowseg.payload_len(Base64.encode_string(Cstruct.to_stringdata)));(* deliver_in_3a deliver_in_4 are done now! *)lett',outs=handle_segmenttnowidseginletev=letold_conn=CM.find_optidt.connectionsinletnew_conn=CM.find_optidt'.connectionsinmatchold_conn,new_connwith|None,None->[]|Someold,None->[`Drop(id,[old.rcv_notify;old.snd_notify])]|_,Someconn->letrcv_data=Rope.lengthconn.rcvq>0inletis_established=letwas_established=Option.value~default:false(Option.map(funs->s.tcp_state=Established)old_conn)innotwas_established&&conn.tcp_state=Establishedinletwas_syn_sent=Option.value~default:false(Option.map(funs->s.tcp_state=Syn_sent)old_conn)inletrcvd_fin=(* the peer shut down its write side (half-close): a pending reader
must be woken up (it will drain the remaining data and observe
Eof on the next recv), but the connection stays usable for
sending (CLOSE_WAIT). See [di3_ststuff] to see when we set
[cantrcvmore]. *)letwas_fin=Option.value~default:false(Option.map(funs->s.cantrcvmore)old_conn)innotwas_fin&&conn.cantrcvmoreinletsnd_space=letwas_snd=Option.value~default:false(Option.map(funs->Rope.lengths.sndq<s.sndbufsize)old_conn)innotwas_snd&&Rope.lengthconn.sndq<conn.sndbufsizein(ifis_establishedthen[`Established(id,ifwas_syn_sentthen`Activeconn.rcv_notifyelse`Passive)]else[])@(ifrcv_datathen[`Received(id,`Data,conn.rcv_notify)]else[])@(ifsnd_spacethen[`Send(id,conn.snd_notify)]else[])@(ifrcvd_fin&¬rcv_datathen[`Received(id,`Eof,conn.rcv_notify)]else[])inList.iter(fun(src',dst',_)->letsrc,_,dst,_=idinifIpaddr.comparesrc'src<>0thenLog.debug(funm->m"bad IP reply src' %a vs src %a"Ipaddr.ppsrc'Ipaddr.ppsrc);ifIpaddr.comparedst'dst<>0thenLog.debug(funm->m"bad IP reply dst' %a vs dst %a"Ipaddr.ppdst'Ipaddr.ppdst))outs;t',ev,outs