at main
1 folder
21 files
dhcp: a client that has asked enough reverts to INIT
A spent retransmission budget ended the exchange: timer answered Failed
and left the client in SELECTING or REQUESTING, holding a half-finished
exchange nothing could take further. RFC 2131 s.3.1 step 5 is explicit
about the DHCPREQUEST -- "If the client receives neither a DHCPACK or a
DHCPNAK message after employing the retransmission algorithm, the client
reverts to INIT state and restarts the initialization process" -- and
s.3.2 step 3 says the same of a client verifying a remembered address.
For the DHCPDISCOVER the specification gives no bound at all: s.4.1
bounds the delay between retransmissions and not their number, and s.3.1
step 3 says only that the client times out and retransmits. Either way
a client that stops asking has recorded nothing, which is INIT.
So the pure machine no longer stops: it goes back to the start, drops
what it was holding, and hands the driver Restart, which already meant
begin again with a fresh transaction id. Figure 5 has no arrow that
ends a client's life, and now neither has this reducer, bar the two
lease-holding phases the next commit is about.
When to stop asking is a policy, and it moves to the driver that has a
clock and a user to answer to. Dhcp_eio.drive, lease and renew take a
~sends budget, eight by default -- a DORA's two phases at the four
attempts s.3.1 step 5 gives as its example -- and lease shares one
budget across every restart, so a client nobody answers stops rather
than beginning again for ever. A caller that wants the old timing
passes ~sends:4.
Two pins retired, two left.
dhcp: a renewal has no budget to spend, it has T2
A renewing client stopped after four DHCPREQUESTs and reported failure,
keeping a lease it had abandoned trying to extend. RFC 2131 s.4.4.5
gives RENEWING and REBINDING a schedule and no count: the client "SHOULD
wait one-half of the remaining time until T2 (in RENEWING state) and
one-half of the remaining lease time (in REBINDING state), down to a
minimum of 60 seconds, before retransmitting the DHCPREQUEST message".
What ends the retransmitting is T2 and the lease expiry, both of which
this machine already answers, and a client that stops before either
gives up an address it still holds and that a server may still be
willing to extend.
So the timer in those two phases always retransmits. The count is what
the other phases have and these two do not, which is why both timer
events answer alike here: the description says the split does not exist
in this phase rather than refusing one half of it, and the cell is
driven and clean instead of being a cell no run can present.
The schedule itself needs the time remaining to T2, so it stays the
driver's: this machine has no clock, next_timeout keeps s.4.1's backoff
to its 64-second cap, and Dhcp_eio's ~sends budget is what stops a
renewal nobody answers.
Client_control.divergences is now empty: every cell of the table is a
cell the reducer answers as RFC 2131 does, and the test fails on any
that stops being.
dhcp: a client that has asked enough reverts to INIT
A spent retransmission budget ended the exchange: timer answered Failed
and left the client in SELECTING or REQUESTING, holding a half-finished
exchange nothing could take further. RFC 2131 s.3.1 step 5 is explicit
about the DHCPREQUEST -- "If the client receives neither a DHCPACK or a
DHCPNAK message after employing the retransmission algorithm, the client
reverts to INIT state and restarts the initialization process" -- and
s.3.2 step 3 says the same of a client verifying a remembered address.
For the DHCPDISCOVER the specification gives no bound at all: s.4.1
bounds the delay between retransmissions and not their number, and s.3.1
step 3 says only that the client times out and retransmits. Either way
a client that stops asking has recorded nothing, which is INIT.
So the pure machine no longer stops: it goes back to the start, drops
what it was holding, and hands the driver Restart, which already meant
begin again with a fresh transaction id. Figure 5 has no arrow that
ends a client's life, and now neither has this reducer, bar the two
lease-holding phases the next commit is about.
When to stop asking is a policy, and it moves to the driver that has a
clock and a user to answer to. Dhcp_eio.drive, lease and renew take a
~sends budget, eight by default -- a DORA's two phases at the four
attempts s.3.1 step 5 gives as its example -- and lease shares one
budget across every restart, so a client nobody answers stops rather
than beginning again for ever. A caller that wants the old timing
passes ~sends:4.
Two pins retired, two left.
dhcp: a renewal has no budget to spend, it has T2
A renewing client stopped after four DHCPREQUESTs and reported failure,
keeping a lease it had abandoned trying to extend. RFC 2131 s.4.4.5
gives RENEWING and REBINDING a schedule and no count: the client "SHOULD
wait one-half of the remaining time until T2 (in RENEWING state) and
one-half of the remaining lease time (in REBINDING state), down to a
minimum of 60 seconds, before retransmitting the DHCPREQUEST message".
What ends the retransmitting is T2 and the lease expiry, both of which
this machine already answers, and a client that stops before either
gives up an address it still holds and that a server may still be
willing to extend.
So the timer in those two phases always retransmits. The count is what
the other phases have and these two do not, which is why both timer
events answer alike here: the description says the split does not exist
in this phase rather than refusing one half of it, and the cell is
driven and clean instead of being a cell no run can present.
The schedule itself needs the time remaining to T2, so it stays the
driver's: this machine has no clock, next_timeout keeps s.4.1's backoff
to its 64-second cap, and Dhcp_eio's ~sends budget is what stops a
renewal nobody answers.
Client_control.divergences is now empty: every cell of the table is a
cell the reducer answers as RFC 2131 does, and the test fails on any
that stops being.
dhcp: a renewal has no budget to spend, it has T2
A renewing client stopped after four DHCPREQUESTs and reported failure,
keeping a lease it had abandoned trying to extend. RFC 2131 s.4.4.5
gives RENEWING and REBINDING a schedule and no count: the client "SHOULD
wait one-half of the remaining time until T2 (in RENEWING state) and
one-half of the remaining lease time (in REBINDING state), down to a
minimum of 60 seconds, before retransmitting the DHCPREQUEST message".
What ends the retransmitting is T2 and the lease expiry, both of which
this machine already answers, and a client that stops before either
gives up an address it still holds and that a server may still be
willing to extend.
So the timer in those two phases always retransmits. The count is what
the other phases have and these two do not, which is why both timer
events answer alike here: the description says the split does not exist
in this phase rather than refusing one half of it, and the cell is
driven and clean instead of being a cell no run can present.
The schedule itself needs the time remaining to T2, so it stays the
driver's: this machine has no clock, next_timeout keeps s.4.1's backoff
to its 64-second cap, and Dhcp_eio's ~sends budget is what stops a
renewal nobody answers.
Client_control.divergences is now empty: every cell of the table is a
cell the reducer answers as RFC 2131 does, and the test fails on any
that stops being.
dhcp: classify an arriving reply before the phase decides
Client.incoming asked, phase by phase, whether the message in front of
it happened to be the reply that phase wanted, through is_reply: a
BOOTREPLY, our transaction id, and one message type. That reading
cannot say what arrived when it is not one, and it cannot see that one
message type carries several answers. RFC 2131 figure 5 draws two
arrows out of REQUESTING for a DHCPACK -- one to BOUND, one back to
INIT behind a DHCPDECLINE -- and s.3.1 step 5 says what tells them
apart: the client's own check on the address it has just been assigned,
which no field of the message carries. s.4.4.1 splits the DHCPOFFER
the same way, since the DHCPREQUEST answering it must carry the server
identifier the offer supplies and table 5 makes that a MUST.
Client_event declares the alphabet those branches induce -- six classes
over the three message types s.4.4 says a client can receive, the five
deadlines of s.4.1 and s.4.4.5, and the three operations the host above
asks for in s.4.4.1, s.4.4.2 and s.4.4.6 -- and derives the six through
Fsm.Classifier, so Theo proves the split total, satisfiable and
pairwise disjoint before the module loads. A hand-rolled split of one
message into several answers is exactly what fsm's core.mli names as
the trust boundary, and this is one of them.
The classifier reads five observations, three from the message and two
from the client: the opcode, the message-type option and the server
identifier, plus whether the transaction id is this client's and what
the address check answered. The last two are the client's rather than
the message's, so the input is the message paired with them.
The complement branch is a real class rather than a residue: a client
reads what a whole broadcast domain puts on the wire, and s.4.4.1 and
s.4.4.5 both have it discard every reply belonging to another exchange.
Nothing executes this yet and no behaviour moves; the description that
does is the next commit.
dhcp: classify an arriving reply before the phase decides
Client.incoming asked, phase by phase, whether the message in front of
it happened to be the reply that phase wanted, through is_reply: a
BOOTREPLY, our transaction id, and one message type. That reading
cannot say what arrived when it is not one, and it cannot see that one
message type carries several answers. RFC 2131 figure 5 draws two
arrows out of REQUESTING for a DHCPACK -- one to BOUND, one back to
INIT behind a DHCPDECLINE -- and s.3.1 step 5 says what tells them
apart: the client's own check on the address it has just been assigned,
which no field of the message carries. s.4.4.1 splits the DHCPOFFER
the same way, since the DHCPREQUEST answering it must carry the server
identifier the offer supplies and table 5 makes that a MUST.
Client_event declares the alphabet those branches induce -- six classes
over the three message types s.4.4 says a client can receive, the five
deadlines of s.4.1 and s.4.4.5, and the three operations the host above
asks for in s.4.4.1, s.4.4.2 and s.4.4.6 -- and derives the six through
Fsm.Classifier, so Theo proves the split total, satisfiable and
pairwise disjoint before the module loads. A hand-rolled split of one
message into several answers is exactly what fsm's core.mli names as
the trust boundary, and this is one of them.
The classifier reads five observations, three from the message and two
from the client: the opcode, the message-type option and the server
identifier, plus whether the transaction id is this client's and what
the address check answered. The last two are the client's rather than
the message's, so the input is the message paired with them.
The complement branch is a real class rather than a residue: a client
reads what a whole broadcast domain puts on the wire, and s.4.4.1 and
s.4.4.5 both have it discard every reply belonging to another exchange.
Nothing executes this yet and no behaviour moves; the description that
does is the next commit.
dhcp: classify an arriving reply before the phase decides
Client.incoming asked, phase by phase, whether the message in front of
it happened to be the reply that phase wanted, through is_reply: a
BOOTREPLY, our transaction id, and one message type. That reading
cannot say what arrived when it is not one, and it cannot see that one
message type carries several answers. RFC 2131 figure 5 draws two
arrows out of REQUESTING for a DHCPACK -- one to BOUND, one back to
INIT behind a DHCPDECLINE -- and s.3.1 step 5 says what tells them
apart: the client's own check on the address it has just been assigned,
which no field of the message carries. s.4.4.1 splits the DHCPOFFER
the same way, since the DHCPREQUEST answering it must carry the server
identifier the offer supplies and table 5 makes that a MUST.
Client_event declares the alphabet those branches induce -- six classes
over the three message types s.4.4 says a client can receive, the five
deadlines of s.4.1 and s.4.4.5, and the three operations the host above
asks for in s.4.4.1, s.4.4.2 and s.4.4.6 -- and derives the six through
Fsm.Classifier, so Theo proves the split total, satisfiable and
pairwise disjoint before the module loads. A hand-rolled split of one
message into several answers is exactly what fsm's core.mli names as
the trust boundary, and this is one of them.
The classifier reads five observations, three from the message and two
from the client: the opcode, the message-type option and the server
identifier, plus whether the transaction id is this client's and what
the address check answered. The last two are the client's rather than
the message's, so the input is the message paired with them.
The complement branch is a real class rather than a residue: a client
reads what a whole broadcast domain puts on the wire, and s.4.4.1 and
s.4.4.5 both have it discard every reply belonging to another exchange.
Nothing executes this yet and no behaviour moves; the description that
does is the next commit.
dhcp: fix O(n^2) pool fill and constant client-id hint in usable_addr
The lease-DB scale fuzzer found free-IP selection dies at scale. Two defects in Lease.usable_addr, neither fork-specific: (1) the client-identifier hint was the constant 1805, so every client that sends an RFC 2132 option-61 identifier -- most modern clients -- hashed to one address, collided, and fell to the linear scan; (2) that fallback rescanned the range from low on every call, so filling the pool was O(size^2), each of size allocations rewalking the dense allocated-from-low prefix.
Hash the identifier so distinct client-id clients spread across the range, as the hardware-address hint already does, and make the fallback probe forward from the per-client hint, wrapping across the range (open addressing). A partially-loaded pool is then served in a bounded number of probes per client. The address a client is offered when its hint is free is unchanged, so per-client affinity is preserved and the existing tests still pass.
fuzz_lease gains a regression test that fills a range to 80% load through usable_addr with distinct client identifiers and asserts the fill cost is sub-quadratic (doubling the range at most triples the cost). Verified to fail against the constant hint: ratio 3.98, ~104M words at size 8000, versus ratio 2.15 and ~1.4M words after the fix. Complete exhaustion of any probe-based allocator is inherently super-linear, so the load stops short of full.
dhcp: fix O(n^2) pool fill and constant client-id hint in usable_addr
The lease-DB scale fuzzer found free-IP selection dies at scale. Two defects in Lease.usable_addr, neither fork-specific: (1) the client-identifier hint was the constant 1805, so every client that sends an RFC 2132 option-61 identifier -- most modern clients -- hashed to one address, collided, and fell to the linear scan; (2) that fallback rescanned the range from low on every call, so filling the pool was O(size^2), each of size allocations rewalking the dense allocated-from-low prefix.
Hash the identifier so distinct client-id clients spread across the range, as the hardware-address hint already does, and make the fallback probe forward from the per-client hint, wrapping across the range (open addressing). A partially-loaded pool is then served in a bounded number of probes per client. The address a client is offered when its hint is free is unchanged, so per-client affinity is preserved and the existing tests still pass.
fuzz_lease gains a regression test that fills a range to 80% load through usable_addr with distinct client identifiers and asserts the fill cost is sub-quadratic (doubling the range at most triples the cost). Verified to fail against the constant hint: ratio 3.98, ~104M words at size 8000, versus ratio 2.15 and ~1.4M words after the fix. Complete exhaustion of any probe-based allocator is inherently super-linear, so the load stops short of full.