open HolKernel Parse boolLib infix THEN open bossLib local open TNet_oksTheory TNet_LIBinterfaceTheory TNet_auxfnsTheory TNet_host0Theory in end; open TNet_typesTheory; (* needed for ^duration_ty ... why? *) val Term = Parse.Term; val _ = new_theory "TNet_hostLTS"; (* TODO: * eyeball them to check for dsched vs d, etc. *) val _ = add_rule { block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)), paren_style = OnlyIfNecessary, fixity = Infix(NONASSOC, 420), pp_elements = [HardSpace 1, TOK "/*", HardSpace 1, TM (* cat *), HardSpace 1, TOK "*/", BreakSpace(1,0), TM, (* host0 *) BreakSpace(1,2), TOK "--", HardSpace 1, TM, (* label *) HardSpace 1, TOK "-->", BreakSpace(1,0)], term_name = "host_redn" }; val _ = add_rule { block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)), paren_style = OnlyIfNecessary, fixity = Infixl 199, pp_elements = [BreakSpace(1,~2), TOK "<==", HardSpace 1], term_name = "revimp" }; val revimp_def = xDefine "revimp" `q <== p = p ==> q`; (* -------------------------------------------------- *) (* Time passage function *) (* -------------------------------------------------- *) (* Time passage is a *function*, i.e., deterministic. Any nondeterminism must occur as a result of a tau (or other) transition. In the present semantics, time passage merely: 1. decrements all timers uniformly 2. prevents time passage if a timer reaches zero 3. prevents time passage if an urgent action is enabled. We model point 3 with the predicate Urgent, and use it in the function Time_Pass which also models points 1 and 2. Thus the function Time_Pass tells us if time may pass, and if so, to what state. We define Time_Pass as a function returning an option type; if the result is NONE then time may not pass for the given duration. Notice that a host state never becomes urgent due merely to time passage, apart from when a timer reaches zero. We depend on this in giving the signature of Urgent (no duration argument). *) val Time_Pass_d_def = Define `(Time_Pass_d : ^duration_aty -> ^time_aty -> ^time_aty option) dur d = let d' = d - dur in if d' >= time_zero then SOME d' else NONE`; val Time_Pass_xd_def = Define `(Time_Pass_xd : ^duration_aty -> 'a timed -> 'a timed option) dur (Timed(x,d)) = case Time_Pass_d dur d of SOME d' -> SOME (Timed(x,d')) || NONE -> NONE`; val Time_Pass_ts_def = Define `(Time_Pass_ts : ^duration_aty -> ('a |-> 'b timed) -> ('a |-> 'b timed) option) dur ts = let ts0' = (Time_Pass_xd dur) o_f ts in if FEVERY ((\t. ?t'. SOME t' = Time_Pass_xd dur t) o SND) ts then SOME ($o_f (\t. @t'. SOME t' = Time_Pass_xd dur t) ts) else NONE`; val Time_Pass_h0_def = Define `(Time_Pass_h0 : ^duration_aty -> host -> host option) dur h = let ts0' = Time_Pass_ts dur h.ts and (* threads allow time to pass *) oq0' = Time_Pass_xd dur h.oq (* oq allows time to pass *) in case (ts0',oq0') of (SOME ts', SOME oq') -> SOME (h with <| ts := ts'; oq := oq' |>) || otherwise -> NONE`; val Urgent_def = (* test if the host is now urgent *) Define `(Urgent : host -> bool) h = (* recvfrom_6 *) (?FC ifds tid d s p1 m ps3 ps4 data ifid mq. F_context FC /\ (h = FC(ifds, tid, Timed(Recvfrom2 s.fd,d), s with <| ps1 := SOME p1; es := NONE; mq := (m with body := UDP(ps3,ps4,data), ifid) :: mq |>))) \/ (* recvfrom_7 *) (?FC tid d ifds s p1 e. F_context FC /\ (h = FC(ifds, tid, Timed(Recvfrom2 s.fd,d), s with <| ps1 := SOME p1; es := SOME e |>))) \/ (* select_3 *) (?ts tid d readseq readseq' writeseq writeseq'. (h.ts = FUPDATE ts (tid, Timed(Select2(readseq,writeseq),d))) /\ (readseq' = FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ ((s.mq <> []) \/ (s.es <> NONE))) readseq) /\ (writeseq' = FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ (h.oqf = F)) writeseq) /\ ((readseq' <> []) \/ (writeseq' <> []))) \/ (* sendto_8 *) (?SC ts tid d s ips is1 ps1 is2 ps2 data oq' oqf'. (h.ts = FUPDATE ts (tid, Timed(Sendto2(s.fd,ips,is1,ps1,is2,ps2,data),d))) /\ (h.s = SC (s with es := NONE)) /\ socklist_context SC /\ ((oq',oqf',T) IN dosend(h.ifds, (ips, data), (s.is1,s.ps1,s.is2,s.ps2), h.oq, h.oqf) /\ ((ips <> NONE) \/ (s.is2 <> NONE)) \/ (oq',oqf',T) IN dosend(h.ifds, (ips, data), (is1,ps1,is2,ps2), h.oq, h.oqf)) /\ string_size data <= UDPpayloadMax) \/ (* sendto_9 *) (?FC tid d ifds s junk e. (h = FC(ifds, tid, Timed(Sendto2(s.fd,junk),d), s with es := SOME e)) /\ F_context FC) \/ (* sendto_10 *) (?ts tid d fd ips data is1 ps1 is2 ps2 SC s. (h.ts = FUPDATE ts (tid,Timed(Sendto2(fd,ips,is1,ps1,is2,ps2,data),d))) /\ (h.s = SC (s with es := NONE)) /\ socklist_context SC /\ (?oq' oqf'. (oq',oqf',T) IN dosend(h.ifds, (ips, data), (is1,ps1,is2,ps2), h.oq, h.oqf)) /\ (string_size data > UDPpayloadMax \/ ((ips = NONE) /\ (s.is2 = NONE)))) `; val Time_Pass_def = Define `(Time_Pass : ^duration_aty -> host -> host option) dur h = let h0' = Time_Pass_h0 dur h and (* timers allow time to pass *) urg = Urgent h (* host not urgent *) in case (h0',urg) of (SOME h', F) -> SOME h' || otherwise -> NONE`; (* Notice that a host state never becomes urgent due merely to time passage, apart from when a timer reaches zero. This means we need only test for urgency at the beginning of the time interval, not throughout it. This is a proof obligation. *) (* -------------------------------------------------- *) (* Host transition rules *) (* -------------------------------------------------- *) (* The standard format for a rule is: (! universally-quantified variables. rule_name /* rule_category (* optional rule description *) */ rule_lhs -- rule_label --> rule_rhs <== rule_side_condition (*: optional rule commentary :*) ) Note that blank lines are to be respected, and preferably indents also. LaTeX is permitted in comments, and Hol source can be enclosed in double square brackets like this: [[Flags(T,F)]]. *) open Net_Hol_reln val (host_redn_rules, host_redn_ind, host_redn_cases) = Net_Hol_reln` (!h ts tid d fd. socket_1 /* succeed */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,(socket ())) --> h with <| ts := FUPDATE ts (tid, Timed(Ret (OK fd),dsched)); s := (Sock(fd,NONE,NONE,NONE,NONE,NONE,Flags(F,F),[]) :: h.s) |> <== fd NOTIN sockfds h.s (* In BSD, this would be [[Flags(T,F)]]. *) ) /\ (!h ts tid d e. socket_2 /* badfail (*: as no file descriptors or file table space :*) */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,socket ()) --> h with ts := FUPDATE ts (tid, Timed(Ret (FAIL e),dsched)) <== e IN {EMFILE; ENFILE} (* The errors are \sEMFILE{} and \sENFILE. *) ) /\ (!FC tid d p1' ifds fd es f mq. bind_1 /* succeed (*: autobinding :*) */ FC(ifds, tid, Timed(Run,d), Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)) -- Lh_call (tid,bind(fd, NONE, NONE)) --> FC(ifds, tid, Timed(Ret (OK ()),dsched), Sock(fd,NONE,SOME p1',NONE,NONE,es,f,mq)) <== F_context FC /\ p1' IN unused FC INTER ephemeral ) /\ (!FC tid d p1' ifds fd i es f mq. bind_2 /* succeed (*: autobinding :*) */ FC(ifds, tid, Timed(Run,d), Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)) -- Lh_call (tid,bind(fd, SOME i, NONE)) --> FC(ifds, tid, Timed(Ret (OK ()),dsched), Sock(fd,SOME i,SOME p1',NONE,NONE,es,f,mq)) <== F_context FC /\ i IN ifds /\ p1' IN unused FC INTER ephemeral ) /\ (!FC tid d ifds fd es f mq p. bind_3 /* succeed (*: autobinding :*) */ FC(ifds, tid, Timed(Run,d), Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)) -- Lh_call (tid,bind(fd,NONE,SOME p)) --> FC(ifds, tid, Timed(Ret (OK ()),dsched), Sock(fd,NONE,SOME p,NONE,NONE,es,f,mq)) <== F_context FC /\ p NOTIN privileged /\ !s. s IN FC /\ (s.ps1 = SOME p) ==> f.reuseaddr /\ s.f.reuseaddr (* Note that the [[ i1 ]] doesn't get chosen until a datagram is sent, as in \cite[p.92]{stevens1998a}. *) ) /\ (!FC tid d ifds fd es f mq i p. bind_4 /* succeed */ FC(ifds, tid, Timed(Run,d), Sock(fd, NONE,NONE,NONE,NONE,es,f,mq)) -- Lh_call (tid,bind(fd,SOME i,SOME p)) --> FC(ifds, tid, Timed(Ret (OK ()),dsched), Sock(fd,SOME i,SOME p,NONE,NONE,es,f,mq)) <== F_context FC /\ i IN ifds /\ p NOTIN privileged /\ !s. s IN FC ==> (s.ps1 = SOME p) /\ ((s.is1 = NONE) \/ (s.is1 = SOME i)) ==> f.reuseaddr /\ s.f.reuseaddr ) /\ (!FC tid d ifds s fd is p. bind_5 /* fail (*: as we don't have access for port p :*) */ FC(ifds, tid, Timed(Run,d), s with fd := fd) -- Lh_call (tid,bind(fd,is,SOME p)) --> FC(ifds, tid, Timed(Ret (FAIL EACCES),dsched), s with fd := fd) <== F_context FC /\ p IN privileged (* On Linux, [[is]] is written into the [[Sock(...)]]; we choose \emph{not} to do so because it would violate our tidy [[socket]] invariant. Since the socket is not placed on the delivery list, we can hide this by letting our wrapper for [[getsockname]] test the local port, and, if it is [[*]], return [[*]] for local [[is]]. *) ) /\ (!FC tid d ifds s fd is p. bind_6 /* fail (*: as port p is already in use :*) */ FC(ifds, tid, Timed(Run,d), s with fd := fd) -- Lh_call (tid,bind(fd,is,SOME p)) --> FC(ifds, tid, Timed(Ret (FAIL EADDRINUSE),dsched), s with fd := fd) <== F_context FC /\ ~(!s'. s' IN FC ==> (s'.ps1 = SOME p) /\ ((s'.is1 = NONE) \/ (is = NONE) \/ (is = s'.is1)) ==> s.f.reuseaddr /\ s'.f.reuseaddr) ) /\ (!FC tid d ifds s fd i ps. bind_7 /* fail (*: as [[i]] is not one of our ip addresses :*) */ FC(ifds, tid, Timed(Run,d), s with fd := fd) -- Lh_call (tid,bind(fd, SOME i, ps)) --> FC(ifds, tid, Timed(Ret (FAIL EADDRNOTAVAIL),dsched), s with fd := fd) <== F_context FC /\ i NOTIN ifds ) /\ (!FC tid d ifds s fd p1 is ps. bind_8 /* fail (*: as the socket has a non-* port already :*) */ FC(ifds, tid, Timed(Run,d), s with <| fd := fd; ps1 := SOME p1 |>) -- Lh_call (tid,bind(fd, is, ps)) --> FC(ifds, tid, Timed(Ret (FAIL EINVAL),dsched), s with <| fd := fd; ps1 := SOME p1|>) <== F_context FC ) /\ (!FC tid d ifds fd es f mq is e. bind_9 /* fail (*: as there are no ephemeral ports left :*) */ FC(ifds, tid, Timed(Run,d), Sock(fd, NONE, NONE, NONE, NONE, es, f, mq)) -- Lh_call (tid,bind(fd,is,NONE)) --> FC(ifds, tid, Timed(Ret (FAIL e),dsched), Sock(fd, NONE, NONE, NONE, NONE, es, f, mq)) <== F_context FC /\ (unused FC INTER ephemeral = EMPTY) /\ (e IN ephemeralErrors) (* This error is awkward to test, as the test machines run out of files ([[ENFILE]] from [[socket]]) at about 3500, before the ephemeral ports are exhausted. The error set [[ephemeralErrors = \{EAGAIN,EADDRINUSE\}]] is therefore speculative. \mignore{Looking at the kernel, the tcp port rover has an explicit check for running out, but I (can't see the udp port rover in udpv4getport in net/ipv4/udp.c doing anything sensible. The error set is therefore a guess. We may be able to test by using sysctl to cut down the number of ephemeral ports. (a test machine crashes when we try to do that).} *) ) /\ (!FC tid d ifds fd ps1 i1 p1' es f mq i ps. connect_1 /* succeed (*: autobinding if necessary :*) */ FC(ifds, tid, Timed(Run,d), Sock(fd,NONE,ps1,NONE,NONE,es,f,mq)) -- Lh_call (tid,connect(fd,i,ps)) --> FC(ifds, tid, Timed(Ret (OK ()),dsched), Sock(fd,SOME i1,SOME p1',SOME i,ps,es,f,mq)) <== F_context FC /\ i1 IN outroute(ifds,i) /\ p1' IN autobind(ps1, FC) ) /\ (!FC tid d ifds fd i1 p1 is2 ps2 es f mq i ps. connect_2 /* succeed */ FC(ifds, tid, Timed(Run,d), Sock(fd,SOME i1,SOME p1,is2,ps2,es,f,mq)) -- Lh_call (tid,connect(fd,i,ps)) --> FC(ifds, tid, Timed(Ret (OK ()),dsched), Sock(fd,SOME i1,SOME p1,SOME i,ps,es,f,mq)) <== F_context FC ) /\ (!FC tid d ifds fd es f mq i ps s e. connect_3 /* fail (*: as there are no ephemeral ports left :*) */ FC(ifds, tid, Timed(Run,d), Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)) -- Lh_call (tid,connect(fd,i,ps)) --> FC(ifds, tid, Timed(Ret (FAIL e),dsched), s with fd := fd) <== F_context FC /\ (unused FC INTER ephemeral = EMPTY) /\ e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd) (* See remark for [[bind.9]]. The rule leaves the socket in a indeterminate state, as we do not want to specify exactly when the \texttt{getport} is called. *) ) /\ (!FC tid d ifds fd is1 p1 is2 ps2 es f mq. disconnect_1 /* succeed */ FC(ifds, tid, Timed(Run,d), Sock(fd,is1,SOME p1,is2,ps2,es,f,mq)) -- Lh_call (tid,disconnect fd) --> FC(ifds, tid, Timed(Ret (OK ()),dsched), Sock(fd,NONE,SOME p1,NONE,NONE,es,f,mq)) <== F_context FC (* Note that this leaves the local port in place, perhaps surprisingly. *) ) /\ (!FC tid d ifds fd es f mq p1. disconnect_2 /* succeed (*: but also autobind :*) */ FC(ifds, tid, Timed(Run,d), Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)) -- Lh_call (tid,disconnect fd) --> FC(ifds, tid, Timed(Ret (OK ()),dsched), Sock(fd,NONE,SOME p1,NONE,NONE,es,f,mq)) <== F_context FC /\ p1 IN unused FC INTER ephemeral (* This autobind may be surprising, but the resulting state \emph{can} receive msgs on [[*,p1]]. *) ) /\ (!FC tid d ifds fd es f mq e s. disconnect_3 /* fail (*: as there are no ephemeral ports left :*) */ FC(ifds, tid, Timed(Run,d), Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)) -- Lh_call (tid,disconnect fd) --> FC(ifds, tid, Timed(Ret (FAIL e),dsched), s with fd := fd) <== F_context FC /\ (unused FC INTER ephemeral = EMPTY) /\ e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd) (* See remark for [[connect_3]]. *) ) /\ (!FC tid d ifds s fd. getsockname_1 /* succeed */ FC(ifds, tid, Timed(Run,d), s with fd := fd) -- Lh_call (tid,getsockname fd) --> FC(ifds, tid, Timed(Ret (OK(s.is1, s.ps1)),dsched), s with fd := fd) <== F_context FC (* See comment at [[bind.5]] ([[EACCES]]). This involves a thin wrapper over the C system call; if we get [[( SOME is,* )]] from the C system call then return [[( *,* )]]. This [[ps1=*]] case of the rule covers for the weird Linux behaviour of a failing bind due to [[EACCES]] or [[EADDRINUSE]]. *) ) /\ (!FC tid d ifds s fd. getpeername_1 /* succeed */ FC(ifds, tid, Timed(Run,d), s with fd := fd) -- Lh_call (tid,getpeername fd) --> FC(ifds, tid, Timed(Ret (OK(s.is2,s.ps2)),dsched), s with fd := fd) <== F_context FC (* This involves a thin wrapper over the C system call: if we get [[ENOTCONN]] then return [[( *,* )]]. *) ) /\ (!FC tid d ifds s fd. geterr_1 /* succeed */ FC(ifds, tid, Timed(Run,d), s with fd := fd) -- Lh_call (tid,geterr fd) --> FC(ifds, tid, Timed(Ret (OK s.es),dsched), s with <| fd := fd; es := NONE|>) <== F_context FC (*: [[geterr fd]] is our name for the C call \texttt{getsockopt(fd,SOL\_SOCKET,SO\_ERROR,...)}. :*) ) /\ (!FC tid d ifds s fd opt b. getsockopt_1 /* succeed */ FC(ifds, tid, Timed(Run,d), s with fd := fd) -- Lh_call (tid,getsockopt(fd, opt)) --> FC(ifds, tid, Timed(Ret (OK b),dsched), s with fd := fd) <== F_context FC /\ ((opt = SO_BSDCOMPAT) ==> (b = s.f.bsdcompat)) /\ ((opt = SO_REUSEADDR) ==> (b = s.f.reuseaddr)) ) /\ (!FC tid d ifds s fd opt b f'. setsockopt_1 /* succeed */ FC(ifds, tid, Timed(Run,d), s with fd := fd) -- Lh_call (tid,setsockopt(fd,opt,b)) --> FC(ifds, tid, Timed(Ret (OK ()),dsched), s with <| fd := fd; f := f' |>) <== F_context FC /\ ((opt = SO_BSDCOMPAT) ==> (f' = s.f with bsdcompat := b)) /\ ((opt = SO_REUSEADDR) ==> (f' = s.f with reuseaddr := b)) ) /\ (!SC h ts tid d s ips data nb oq' oqf' p1'. sendto_1 /* succeed (*: autobinding :*) */ h with <| ts := FUPDATE ts (tid, Timed(Run,d)); s := SC (s with es := NONE) |> -- Lh_call (tid,sendto(s.fd,ips,data,nb)) --> h with <| ts := FUPDATE ts (tid, Timed(Ret (OK ()),dsched)); s := SC (s with <| es := NONE; ps1 := SOME p1' |>); oq := oq'; oqf := oqf' |> <== socklist_context SC /\ p1' IN autobind(s.ps1, SC) /\ (oq', oqf', T) IN dosend(h.ifds, (ips, data), (s.is1, SOME p1', s.is2, s.ps2), h.oq, h.oqf) /\ string_size data <= UDPpayloadMax /\ ((ips <> NONE) \/ (s.is2 <> NONE)) ) /\ (!SC h ts tid d s ips data p1' oq' oqf'. sendto_2 /* enter2 (*: entering Sendto2 state :*) */ h with <| ts := FUPDATE ts (tid, Timed(Run,d)); s := SC (s with es := NONE) |> -- Lh_call (tid,sendto(s.fd, ips, data, F)) --> h with <| ts := FUPDATE ts (tid, Timed(Sendto2(s.fd,ips,s.is1,SOME p1',s.is2,s.ps2, data), time_infty)); s := SC (s with <| es := NONE; ps1 := SOME p1' |>); oq := oq'; oqf := oqf' |> <== socklist_context SC /\ p1' IN autobind(s.ps1, SC) /\ (oq',oqf',F) IN dosend(h.ifds, (ips, data), (s.is1, SOME p1', s.is2, s.ps2), h.oq, h.oqf) /\ ((ips <> NONE) \/ (s.is2 <> NONE)) (*: Note how the blocking call to [[sendto]] records the values of the socket's four address fields so that messages may still be delivered, even if the socket is later disconnected. :*) ) /\ (!SC h ts tid d s ips data p1' oq' oqf'. sendto_3 /* fail (*: as would block :*) */ h with <| ts := FUPDATE ts (tid, Timed(Run,d)); s := SC (s with es := NONE) |> -- Lh_call (tid,sendto(s.fd,ips,data,T)) --> h with <| ts := FUPDATE ts (tid, Timed(Ret (FAIL EAGAIN),dsched)); s := SC (s with <| es := NONE; ps1 := SOME p1' |>); oq := oq'; oqf := oqf' |> <== socklist_context SC /\ p1' IN autobind(s.ps1, SC) /\ (oq',oqf',F) IN dosend(h.ifds, (ips, data), (s.is1, SOME p1', s.is2, s.ps2), h.oq, h.oqf) /\ ((ips <> NONE) \/ (s.is2 <> NONE)) (* Note that in Linux [[ \tscon{EWOULDBLOCK}]] and [[EAGAIN ]] are aliased. *) ) /\ (!FC tid d ifds fd is1 ps1 f mq data nb p1'. sendto_4 /* fail (*: as socket unconnected :*) */ FC(ifds, tid, Timed(Run,d), Sock(fd,is1,ps1,NONE,NONE,NONE,f,mq)) -- Lh_call (tid,sendto(fd,NONE,data,nb)) --> FC(ifds, tid, Timed(Ret (FAIL ENOTCONN),dsched), Sock(fd,is1,SOME p1',NONE,NONE,NONE,f,mq)) <== F_context FC /\ p1' IN autobind(ps1,FC) (* \cite{stevens1998a} states this should give [[\tscon{EDESTADDRREQ}]], not [[ENOTCONN]]. *) ) /\ (!FC tid d ifds s p1 e ips data nb. sendto_5 /* fail (*: as socket in an error state :*) */ FC(ifds, tid, Timed(Run,d), s with <| ps1 := SOME p1; es := SOME e |>) -- Lh_call (tid,sendto(s.fd,ips,data,nb)) --> FC(ifds, tid, Timed(Ret (FAIL e),dsched), s with <| ps1 := SOME p1; es := NONE |>) <== F_context FC (* Recall that by the [[socket-ok]] invariant if the error component is [[SOME e]] then the local port is not [[*]]. *) ) /\ (!FC tid d ifds s ips data nb ps1'. sendto_6 /* fail (*: as [[data]] size too big :*) */ FC(ifds, tid, Timed(Run,d), s) -- Lh_call (tid,sendto(s.fd, ips, data, nb)) --> FC(ifds, tid, Timed(Ret (FAIL EMSGSIZE),dsched), s with ps1 := ps1') <== F_context FC /\ string_size data > UDPpayloadMax /\ ps1' IN {s.ps1} UNION (IMAGE (SOME) (autobind(s.ps1, FC))) (* In Linux, [[sendto_5]] takes precedence over this, so [[EMSGSIZE]] cannot happen in an error state. In a normal state, it does not set the error flag. What happens on a [[Sendto2]] if an error flag is set is open. Note that we let [[ps1'=ps1]] nondeterministically, as the size check may be before or after the autobind. On Linux this is unnecessary as the autobind is performed before the [[EMSGSIZE]] check. Note that we nondeterministically allow the message size check to fail either on entry to [[Sendto2]] or on exit. *) ) /\ (!FC tid d ifds fd ips data nb f mq e s. sendto_7 /* fail (*: as there are no ephemeral ports left :*) */ FC(ifds, tid, Timed(Run,d), Sock(fd,NONE,NONE,NONE,NONE,NONE,f,mq)) -- Lh_call (tid,sendto(fd, ips, data, nb)) --> FC(ifds, tid, Timed(Ret (FAIL e),dsched), s with fd := fd) <== F_context FC /\ (autobind(NONE, FC) = EMPTY) /\ e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd) ) /\ (!SC h ts tid d s ips is1 ps1 is2 ps2 data oq' oqf'. sendto_8 /* slowsucceed (*: [urgent] :*) */ h with <| ts := FUPDATE ts (tid, Timed(Sendto2(s.fd,ips,is1,ps1,is2,ps2,data),d)); s := SC (s with es := NONE) |> -- Lh_tau --> h with <| ts := FUPDATE ts (tid, Timed(Ret (OK ()),dsched)); s := SC (s with es := NONE); oq := oq'; oqf := oqf' |> <== socklist_context SC /\ ((oq',oqf',T) IN dosend(h.ifds, (ips, data), (s.is1,s.ps1,s.is2,s.ps2), h.oq, h.oqf) /\ ((ips <> NONE) \/ (s.is2 <> NONE)) \/ (oq',oqf',T) IN dosend(h.ifds, (ips, data), (is1,ps1,is2,ps2), h.oq, h.oqf) /\ ((ips <> NONE) \/ (is2 <> NONE))) /\ string_size data <= UDPpayloadMax (* Note that the [[Sendto2]] state can only be entered by the [[sendto_2]] rule. Unfortunately, this does not guarantee that the socket's [[is2]] and [[ps2]] will be present, because a call to [[disconnect]] may have removed them. We allow for a successful send to occur based on the values in the socket when the call was made however. *) ) /\ (!FC tid d ifds s ips data e. sendto_9 /* slowfail (*: [urgent] as socket has entered an error state :*) */ FC(ifds, tid, Timed(Sendto2(s.fd,ips,data),d), s with es := SOME e) -- Lh_tau --> FC(ifds, tid, Timed(Ret (FAIL e),dsched), s with es := NONE) <== F_context FC ) /\ (!h ts tid d fd ips is1 ps1 is2 ps2 e data SC s. sendto_10 /* slowfail (*: [urgent] as [[data]] size too big or socket now disconnnected :*) */ h with <| ts := FUPDATE ts (tid,Timed(Sendto2(fd,ips,is1,ps1,is2,ps2,data),d)); s := SC (s with es := NONE) |> -- Lh_tau --> h with <| ts := FUPDATE ts (tid,Timed(Ret (FAIL e),dsched)); s := SC (s with es := NONE) |> <== socklist_context SC /\ (?oq' oqf'. (oq',oqf',T) IN dosend(h.ifds, (ips, data), (is1,ps1,is2,ps2), h.oq, h.oqf)) /\ ((string_size data > UDPpayloadMax /\ (e = EMSGSIZE) \/ (s.is2 = NONE) /\ (ips = NONE) /\ (e = ENOTCONN))) (*: The condition ensures it fires only when we try to put the message onto the outqueue, modelling the discovery at that point that the message is too large, or that the socket has become disconnected. (This rule nondeterministically competes with [[sendto_6]], which would catch an outsize message earlier, and with [[sendto_8]], which would allow the delivery of a message on a now-disconnected socket based on the values of [[s.is2]] and [[s.ps2]] when the call was made. This rule leaves the socket state unchanged. One might wish to allow it to have been disturbed, nondeterministically. :*) ) /\ (!FC tid d ifds s i3 i4 ifid mq nb p1 ps3 ps4 data. recvfrom_1 /* succeed */ FC(ifds, tid, Timed(Run,d), s with <| ps1 := SOME p1; es := NONE; mq := (IP(i3,i4,UDP(ps3,ps4,data)), ifid) :: mq |>) -- Lh_call (tid,recvfrom(s.fd,nb)) --> FC(ifds, tid, Timed(Ret (OK(i3,ps3,data)),dsched), s with <| ps1 := SOME p1; es := NONE; mq := mq |>) <== F_context FC ) /\ (!FC tid d ifds s p1'. recvfrom_2 /* enter2 (*: entering Recvfrom2 state :*) */ FC(ifds, tid, Timed(Run,d), s with <| es := NONE; mq := [] |>) -- Lh_call (tid,recvfrom(s.fd,F)) --> FC(ifds, tid, Timed(Recvfrom2 s.fd,time_infty), s with <| es := NONE; mq := []; ps1 := SOME p1'|>) <== F_context FC /\ p1' IN autobind(s.ps1, FC) (* The autobinding can be observed by guessing the next ephemeral port. *) ) /\ (!FC tid d ifds s p1'. recvfrom_3 /* fail (*: as would block :*) */ FC(ifds, tid, Timed(Run,d), s with <| es := NONE; mq := [] |>) -- Lh_call (tid,recvfrom(s.fd,T)) --> FC(ifds, tid, Timed(Ret (FAIL EAGAIN),dsched), s with <| es := NONE; mq := []; ps1 := SOME p1'|>) <== F_context FC /\ p1' IN autobind(s.ps1, FC) (* Note that in Linux [[ \tscon{EWOULDBLOCK}]] and [[EAGAIN ]] are aliased. *) ) /\ (!FC tid d ifds s p1 e nb. recvfrom_4 /* fail (*: as socket in an error state :*) */ FC(ifds, tid, Timed(Run,d), s with <| ps1 := SOME p1; es := SOME e |>) -- Lh_call (tid,recvfrom(s.fd, nb)) --> FC(ifds, tid, Timed(Ret (FAIL e),dsched), s with <| ps1 := SOME p1; es := NONE |>) <== F_context FC ) /\ (!FC tid d ifds fd nb f e s. recvfrom_5 /* fail (*: as there are no ephemeral ports left :*) */ FC(ifds, tid, Timed(Run,d), Sock(fd,NONE,NONE,NONE,NONE,NONE,f,[])) -- Lh_call (tid,recvfrom(fd,nb)) --> FC(ifds, tid, Timed(Ret (FAIL e),dsched), s with fd := fd) <== F_context FC /\ (autobind(NONE, FC) = EMPTY) /\ e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd) (* See remark for [[connect_3]]. *) ) /\ (!FC tid d ifds s p1 mq i3 i4 ps3 ps4 data ifid. recvfrom_6 /* slowsucceed (*: [urgent] :*) */ FC(ifds, tid, Timed(Recvfrom2 s.fd,d), s with <| ps1 := SOME p1; es := NONE; mq := (IP(i3,i4,UDP(ps3,ps4,data)), ifid) :: mq |>) -- Lh_tau --> FC(ifds, tid, Timed(Ret (OK(i3,ps3,data)),dsched), s with <| ps1 := SOME p1; es := NONE; mq := mq |>) <== F_context FC (* Note that the [[Recvfrom2]] state can only be entered by the [[recvfrom_2]] rule, so we have [[ps1= SOME p1]] in the [[host-ok]] invariant. *) ) /\ (!FC tid d ifds s p1 e. recvfrom_7 /* slowfail (*: [urgent] as socket has entered an error state :*) */ FC(ifds, tid, Timed(Recvfrom2 s.fd,d), s with <| ps1 := SOME p1; es := SOME e |>) -- Lh_tau --> FC(ifds, tid, Timed(Ret (FAIL e),dsched), s with <| ps1 := SOME p1; es := NONE |>) <== F_context FC ) /\ (!h ts tid d s1 s2 s. close_1 /* succeed */ h with <| ts := FUPDATE ts (tid, Timed(Run,d)); s := APPEND s1 (s :: s2) |> -- Lh_call (tid,close s.fd) --> h with <| ts := zombify s.fd o_f FUPDATE ts (tid, Timed(Ret(OK()),dsched)); s := APPEND s1 s2 |> <== T (*: The [[zombify]] function takes Sendto2 and Recvfrom2 threadstates involving [[s.fd]] to the Zombie threadstate. Select2 threadstates involving [[s.fd]] have that descriptor removed from the lists of file-descriptors maintained by that state. Note that we are unsure about this behaviour. Initial experiments using MiniCaml threads suggest that blocked [[Recvfrom2]] threads remain blocked in this situation (and don't raise an error, as one might expect). Further experiments, particularly on blocked [[Sendto2]] states are required. :*) ) /\ (!h ts tid d d' readseq writeseq tms. select_1 /* enter2 (*: entering Select2 state :*) */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,select(readseq,writeseq,tms)) --> h with ts := FUPDATE ts (tid, Timed(Select2(readseq,writeseq),d')) <== LIST_TO_SET (APPEND readseq writeseq) SUBSET sockfds h.s /\ (!i. (tms = SOME i) ==> 0 <= i) /\ (d' = case tms of NONE -> time_infty || SOME i -> time (real_of_int i / 1000000)) ) /\ (!h ts tid d readseq writeseq tm. select_2 /* fail (*: as timeout negative :*) */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,select(readseq,writeseq,SOME tm)) --> h with ts := FUPDATE ts (tid, Timed(Ret (FAIL EINVAL),dsched)) <== tm < 0 ) /\ (!h ts tid d readseq readseq' writeseq writeseq'. select_3 /* slowsucceed (*: [urgent] with at least one [[fd]] ready :*) */ h with ts := FUPDATE ts (tid, Timed(Select2(readseq,writeseq),d)) -- Lh_tau --> h with ts := FUPDATE ts (tid, Timed(Ret (OK(readseq', writeseq')),dsched)) <== (readseq' = FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ ((s.mq <> []) \/ (s.es <> NONE))) readseq) /\ (writeseq' = FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ (h.oqf = F)) writeseq) /\ ((readseq' <> []) \/ (writeseq' <> [])) ) /\ (!h ts tid readseq readseq' writeseq writeseq'. select_4 /* slowsucceed (*: timeout reached :*) */ h with ts := FUPDATE ts (tid, Timed(Select2(readseq,writeseq),time_zero)) -- Lh_tau --> h with ts := FUPDATE ts (tid, Timed(Ret (OK(readseq',writeseq')),dsched)) <== (readseq' = FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ ((s.mq <> []) \/ (s.es <> NONE))) readseq) /\ (writeseq' = FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ (h.oqf = F)) writeseq) /\ (readseq' = []) /\ (writeseq' = []) ) /\ (!h ts tid d tm d'. delay_1 /* enter2 (*: entering Delay2 state :*) */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,delay tm) --> h with ts := FUPDATE ts (tid, Timed(Delay2,d')) <== (tm >= 0) /\ (d' = time (real_of_int tm / 1000000)) ) /\ (!h ts tid d tm. delay_2 /* fail (*: as timeout negative :*) */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,delay tm) --> h with ts := FUPDATE ts (tid, Timed(Ret (FAIL EINVAL),dsched)) <== tm < 0 ) /\ (!h ts tid. delay_3 /* slowsucceed (*: when timer reaches zero :*) */ h with ts := FUPDATE ts (tid, Timed(Delay2,time_zero)) -- Lh_tau --> h with ts := FUPDATE ts (tid, Timed(Ret (OK ()),dsched)) <== T ) /\ (!h ts tid d iflist ifset (*[VARS hifd ipslist ]*). getifaddrs_1 /* succeed */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,getifaddrs ()) --> h with ts := FUPDATE ts (tid, Timed(Ret (OK iflist),dsched)) <== iflist IN orderings ifset /\ (ifset = { (hifd.ifid, hifd.primary, ipslist, hifd.netmask) | hifd IN h.ifds /\ ipslist IN orderings hifd.ipset }) (* Note this returns the interfaces in any arbitrary order each time; likewise the aliases within each interface. If one wanted otherwise, [[ifds]] and [[iset]] should be lists. *) ) /\ (!h ts tid d v. console_print_1 /* enter2 (*: enter the Print2 state :*) */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,print_endline_flush v) --> h with ts := FUPDATE ts (tid, Timed(Print2 v,dsched)) <== T ) /\ (!h ts tid d v. console_print_2 /* misc (*: print the string on console :*) */ h with ts := FUPDATE ts (tid, Timed(Print2 v,d)) -- Lh_console v --> h with ts := FUPDATE ts (tid, Timed(Ret (OK ()),dsched)) <== T ) /\ (!h ts tid d v. convert_port_1 /* succeed */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,port_of_int v) --> h with ts := FUPDATE ts (tid, Timed(Ret (OK (Port (Num v))),dsched)) <== 1 <= v /\ v <= 65535 ) /\ (!h ts tid d v. convert_port_2 /* fail */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,port_of_int v) --> h with ts := FUPDATE ts (tid, Timed(Ret (FAIL EINVAL),dsched)) <== v < 1 \/ v > 65535 ) /\ (!h ts tid d v i. convert_ip_1 /* succeed */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,ip_of_string v) --> h with ts := FUPDATE ts (tid, Timed(Ret (OK i),dsched)) <== valid_ip_string v /\ (i = ipstr_to_ip v) ) /\ (!h ts tid d v. convert_ip_2 /* fail */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,ip_of_string v) --> h with ts := FUPDATE ts (tid, Timed(Ret (FAIL EINVAL),dsched)) <== ~valid_ip_string v ) /\ (!h ts tid d readseq writeseq tms. notsockfd_1 /* fail (*: [[select]] as some [[fd]] not a socket file descriptor :*) */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,select(readseq,writeseq,tms)) --> h with ts := FUPDATE ts (tid, Timed(Ret (FAIL EBADF),dsched)) <== ?fd. MEM fd (APPEND readseq writeseq) /\ fd NOTIN sockfds h.s (*: Error is \lq Bad file number'. :*) ) /\ (!h ts tid d fd opn e. notsockfd_2 /* fail (*: [[OP]] as [[fd]] not a socket file descriptor :*) */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,opn) --> h with ts := FUPDATE ts (tid, Timed(Ret (FAIL e),dsched)) <== opn IN OP fd /\ fd NOTIN sockfds h.s /\ e IN {ENOTSOCK; EBADF} (* The errors are 'Socket operation on non-socket' and 'Bad file number'. *) ) /\ (!h ts tid d opn. intr_1 /* slowfail (*: as system call interrupted :*) */ h with ts := FUPDATE ts (tid, Timed(opn,d)) -- Lh_tau --> h with ts := FUPDATE ts (tid, Timed(Ret (FAIL EINTR),dsched)) <== (?v. opn = Sendto2 v) \/ (?v. opn = Recvfrom2 v) \/ (?v. opn = Select2 v) \/ (?v. opn = Print2 v) \/ ( opn = Delay2) \/ ( opn = Zombie) (* (need to add explanation here) *) ) /\ (!h ts tid d e. badmem_1 /* badfail (*: [[socket]] as no space :*) */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,socket()) --> h with ts := FUPDATE ts (tid, Timed(Ret (FAIL e),dsched)) <== e IN {ENOMEM; ENOBUFS} (* The errors are (no space to allocate) and (no space for buffers) respectively. *) ) /\ (!FC ifds tid d s opn e. badmem_2 /* badfail (*: [[OP]] as no space :*) */ FC(ifds, tid, Timed(Run,d), s) -- Lh_call (tid,opn) --> FC(ifds, tid, Timed(Ret (FAIL e),dsched), s) <== F_context FC /\ opn IN OP(s.fd) /\ e IN {ENOMEM; ENOBUFS} (* The errors are (no space to allocate) and (no space for buffers) respectively. *) ) /\ (!FC ifds tid t d s e. badmem_3 /* badfail (*: [[OP2]] as no space :*) */ FC(ifds, tid, Timed(t,d), s) -- Lh_tau --> FC(ifds, tid, Timed(Ret (FAIL e),dsched), s) <== F_context FC /\ t IN OP2(s.fd) /\ e IN {ENOMEM; ENOBUFS} (* The errors are (no space to allocate) and (no space for buffers) respectively. *) ) /\ (!h ts tid d v e. badmem_4 /* badfail (*: [[Select2]] as no space :*) */ h with ts := FUPDATE ts (tid, Timed(Select2 v,d)) -- Lh_tau --> h with ts := FUPDATE ts (tid, Timed(Ret (FAIL e),dsched)) <== e IN {ENOMEM; ENOBUFS} (* The errors are 'Out of memory' and 'No buffer space available'. *) ) /\ (!h ts tid d. exit_1 /* exit */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,exit()) --> h with ts := FUPDATE ts (tid, Timed(Exit,dsched)) <== T ) /\ (!h ts tid d. exit_2 /* exit */ h with ts := FUPDATE ts (tid, Timed(Exit,d)) -- Lh_exit --> h with <| ts := FEMPTY ; s := [] |> <== T ) (* See \S mref{b71}. This rule removes all the sockets (matching Unix behaviour, supposing that all sockets in the machine were created by the process). It leaves the [[oq]] and [[oqf]] unchanged, so messages may still be delivered outwards. \mignore{in fact, some of them might be lost?) When any thread calls exit, all the threads are zapped. It should also be the case that when the top thread terminates normally, all the other threads should be zapped. *) /\ (!h ts tid d v. ret_1 /* misc (*: return value [[v]] from fast system call to thread :*) */ h with ts := FUPDATE ts (tid, Timed(Ret v,d)) -- Lh_return (tid,v) --> h with ts := FUPDATE ts (tid, Timed(Run,time_infty)) <== T ) /\ (!h ts tid d tid'. create_1 /* succeed (*: create new thread :*) */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,create()) --> h with ts := FUPDATE (FUPDATE ts (tid, Timed(Ret (OK tid'),dsched))) (tid',Timed(Run,time_infty)) <== tid' NOTIN ({tid} UNION FDOM ts) ) /\ (!h ts tid d. create_2 /* badfail (*: no space for new thread :*) */ h with ts := FUPDATE ts (tid, Timed(Run,d)) -- Lh_call (tid,create()) --> h with ts := FUPDATE ts (tid, Timed(Ret (FAIL EAGAIN),dsched)) <== T (* The man page for pthread_create explains that EAGAIN is returned if there aren't enough system resources, or if there are more threads than PTHREAD_THREADS_MAX. *) ) /\ (!h i1 i2 oq' oqf'. delivery_out_1 /* misc (*: put UDP or ICMP to the network from [[oq]] :*) */ h -- Lh_sendmsg (IP(i1,i2,body)) --> h with <| oq := oq'; oqf := oqf' |> <== (IP(i1,i2,body),oq',oqf') IN dequeue(h.oq, h.oqf) /\ i2 NOTIN LOOPBACK UNION MARTIAN /\ i1 NOTIN MARTIAN (*: [[dequeue]] resets the [[oq']] timer to [[time_infty]] if the queue is empty, or to [[doq]] otherwise. Note that [[dequeue]] gives an empty set of possible outcomes if [[oq=[] ]]. :*) ) /\ (!h oq' oqf'. delivery_out_martian /* misc (*: discard martian IP from [[oq]] :*) */ h -- Lh_tau --> h with <| oq := oq'; oqf := oqf' |> <== ?i1 i2 body. (IP(i1,i2,body),oq',oqf') IN dequeue(h.oq, h.oqf) /\ i2 IN MARTIAN (* This rule is speculative. Note that it applies to UDP and to ICMP, and to loopback destinations. *) ) /\ (!h SC s i3 i4 ifd ps3 ps4 data. delivery_in_udp_1 /* misc (*: get UDP from network and deliver it to a matching socket :*) */ h with s := SC s -- Lh_recvmsg (IP(i3,i4,UDP(ps3,ps4,data))) --> h with s := SC (s with mq := APPEND s.mq [(IP(i3,i4,UDP(ps3,ps4,data)),ifd.ifid)]) <== socklist_context SC /\ s IN lookup (SC s) (i3, ps3, i4, ps4) /\ ifd IN h.ifds /\ i4 IN ifd.ipset /\ i4 NOTIN LOOPBACK /\ i3 NOTIN MARTIAN UNION LOOPBACK ) /\ (!h i3 i4 oq' oqf' ps3 ps4 data ok. delivery_in_udp_2 /* misc (*: get UDP from network but generate ICMP, as no matching socket :*) */ h -- Lh_recvmsg (IP(i3,i4,UDP(ps3,ps4,data))) --> h with <| oq := oq'; oqf := oqf' |> <== i4 IN h.ifds /\ (lookup h.s (i3,ps3,i4,ps4) = EMPTY) /\ (oq',oqf',ok) IN ({(h.oq,h.oqf,T)} UNION enqueue(IP(i4,i3,ICMP_PORT_UNREACH(i3,ps3,i4,ps4)), h.oq, h.oqf)) /\ i4 NOTIN LOOPBACK /\ i3 NOTIN MARTIAN UNION LOOPBACK (* Note that ICMP generation is unreliable; the Linux kernel has per-type-of-ICMP rate-limiting to control denial-of-service attacks. We take a nondeterministic approximation. Note also that the ICMP is dropped if the outqueue is full ([[ok=false]]). \mignore{In the real world, there is no socket to charge this to... so who says "no room to allocate skb"?} *) ) /\ (!h i3 i4 body. delivery_in_martian_3 /* misc (*: get martian IP from network and discard :*) */ h -- Lh_recvmsg (IP(i3,i4,body)) --> h <== i4 IN h.ifds /\ i4 NOTIN LOOPBACK /\ (loopback (IP(i3,i4,body)) \/ martian (IP(i3,i4,body))) (* This is a garbage collection rule to pull martian UDP or ICMP off of the network and discard them. *) ) /\ (!h s SC es' i3' i4' i3 ps3 i4 ps4 body. delivery_in_icmp_1 /* misc (*: get ICMP from the network, setting error in a matching socket :*) */ h with s := SC s -- Lh_recvmsg (IP(i4',i3',body)) --> h with s := SC (s with es := es') <== socklist_context SC /\ ((body = ICMP_HOST_UNREACH(i3,ps3,i4,ps4)) \/ (body = ICMP_PORT_UNREACH(i3,ps3,i4,ps4))) /\ s IN lookup (SC s) (i3,ps3,i4,ps4) /\ i3' IN h.ifds /\ ~(loopback(IP(i4',i3',body)) \/ martian(IP(i4',i3',body))) /\ (es' = if (s.is2 <> NONE) \/ ~s.f.bsdcompat then SOME ECONNREFUSED else s.es) (* As we are not sure which destination ([[i3]], [[i3']]) address the matching is done on, we add the [[LOOPBACK]] check to both to make the rule sensible. Should (re?)check the source. *) ) /\ (!h i3' i4' i3 ps3 i4 ps4 body. delivery_in_icmp_2 /* misc (*: get ICMP from the network and drop as no matching socket :*) */ h -- Lh_recvmsg (IP(i4',i3',body)) --> h <== i3' IN h.ifds /\ ((body = ICMP_HOST_UNREACH(i3,ps3,i4,ps4)) \/ (body = ICMP_PORT_UNREACH(i3,ps3,i4,ps4))) /\ (lookup h.s (i3,ps3,i4,ps4) = EMPTY) /\ ~(loopback(IP(i4',i3',body)) \/ martian(IP(i4',i3',body))) ) /\ (!h i3 i4 SC s ifid oq' oqf' ps3 ps4 data. delivery_loopback_udp_1 /* misc (*: get loopback UDP from [[oq]] and deliver it to a matching socket :*) */ h with s := SC s -- Lh_tau --> h with <| s := SC (s with mq := APPEND s.mq [(IP(i3,i4,UDP(ps3,ps4,data)),ifid)]); oq := oq'; oqf := oqf' |> <== socklist_context SC /\ (IP(i3,i4,UDP(ps3,ps4,data)), oq', oqf') IN dequeue(h.oq,h.oqf) /\ i4 IN LOOPBACK /\ s IN lookup (SC s) (i3,ps3,i4,ps4) /\ <| ifid := ifid; ipset := LOOPBACK; primary := localhost; netmask := NETMASK (255 * (2 EXP 24)) |> IN h.ifds (* [[dequeue]] resets the [[oq']] timer to [[time_infty]] if the queue is empty, or to [[doq]] otherwise. Note that [[\{i3,i4\}\cap MARTIAN = \emptyset ]] is guaranteed by invariants. *) ) /\ (!h i3 i4 oq' oq'' oqf' oqf'' ps3 ps4 data ok. delivery_loopback_udp_2 /* misc (*: get a loopback UDP from [[oq]] but generate loopback ICMP, as no matching socket :*) */ h -- Lh_tau --> h with <| oq := oq''; oqf := oqf'' |> <== (IP(i3,i4,UDP(ps3,ps4,data)), oq', oqf') IN dequeue(h.oq, h.oqf) /\ i4 IN LOOPBACK /\ (lookup h.s (i3,ps3,i4,ps4) = EMPTY) /\ (oq'',oqf'',ok) IN enqueue(IP(i4,i3,ICMP_PORT_UNREACH(i3,ps3,i4,ps4)), oq', oqf') (* ICMPs are dropped if the outqueue is full (the [[ok]] flag is ignored). Note that [[\{i3,i4\}\cap MARTIAN = \emptyset ]] is guaranteed by invariants. *) ) /\ (!h SC s es' oq' oqf' i3' i4' i3 ps3 i4 ps4. delivery_loopback_icmp_1 /* misc (*: get a loopback ICMP from [[oq]] and deliver (by setting [[es]]) to a matching socket :*) */ h with s := SC s -- Lh_tau --> h with <| s := SC (s with es := es'); oq := oq'; oqf := oqf'|> <== socklist_context SC /\ (IP(i4',i3',ICMP_PORT_UNREACH(i3,ps3,i4,ps4)),oq',oqf') IN dequeue(h.oq, h.oqf) /\ i3' IN LOOPBACK /\ s IN lookup (SC s) (i4,ps4,i3,ps3) /\ (es' = if (s.is2 <> NONE) \/ ~s.f.bsdcompat then SOME ECONNREFUSED else s.es) (* Note that [[\{i4',i3',i3,i4\}\cap MARTIAN = \emptyset ]] is guaranteed by invariants. *) ) /\ (!h i3' i4' oq' oqf' i3 ps3 i4 ps4. delivery_loopback_icmp_2 /* misc (*: get a loopback ICMP from [[oq]] and drop, as no socket matches :*) */ h -- Lh_tau --> h with <| oq := oq'; oqf := oqf' |> <== (IP(i4',i3',ICMP_PORT_UNREACH(i3,ps3,i4,ps4)), oq', oqf') IN dequeue(h.oq,h.oqf) /\ i3' IN LOOPBACK /\ (lookup h.s (i4,ps4,i3,ps3) = EMPTY) (* Note that [[\{i4',i3'\}\cap MARTIAN = \emptyset ]] is guaranteed by invariants. *) ) /\ (!h h' d. epsilon_1 /* misc (*: time passage :*) */ h -- Lh_epsilon d --> h' <== d > 0 /\ (Time_Pass d h = SOME h') ) ` handle e => Raise e; val _ = add_rule { block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)), paren_style = OnlyIfNecessary, fixity = Infix(NONASSOC, 420), pp_elements = [HardSpace 1, TOK "--", HardSpace 1, TM (* label *), HardSpace 1, TOK "--->", BreakSpace(1,0)], term_name = "transition3" }; val host_redn'_def = Define` host_redn' h0 l h = ?rid rcat. rid /* rcat */ h0 -- l --> h`; val _ = overload_on ("transition3", ``host_redn'``); val _ = export_theory();