Skip to content

Commit 5e76e34

Browse files
committed
tests: fix and harden MLD host module tests after the IPv6 DAD-disable RNG shift
The DAD-disable fix (initiateDad now short-circuits to makeTentativeAddressPermanent when dupAddrDetectTransmits=0, RFC 4862 Section 5.4) removed a uniform() draw, shifting the seeded RNG stream in simulations that disable DAD. MLD_host_basic and MLD_host_groupstates exercise the MLDv1 report-suppression race: when two hosts share a group, the one with the shorter random uniform(0, maxRespDelay) delay answers a Query and holds flag=true while the other suppresses, and only the flag=true host sends a Done on leave. Which host wins is an RNG coin flip, so after the shift host2 wins at seed 0 and host1 sends no Done -- failing the HOST-04 assertion. opp_test cannot express the relational property "the host that Reported is the one that sends the Done, and the other sends none", so the tests pin the seed to fix the roles: - re-seed both tests to 1, where host1 is the reporter again (a pure role choice -- host1 wins for seeds 1, 3, 4, 6 and loses for 0, 2, 5, 7; the behavior is identical either way); - have host2 also leave at t=5s and assert via %not-contains that it sends no Done, so the "exactly one Done, from the reporter" correlation is actually checked rather than being a tautology of host2 never leaving; - document the seed dependence and that an RNG-stream shift swaps the roles (re-pick a seed where host1 wins). (Not attempted: asserting "the other host sends no Report" -- MLDv1 hosts also send unsolicited Report retransmits and the querier sends multiple Queries, so that is not a stable fact even at a fixed seed. The Done is the one unambiguous per-host signal of who the reporter was.)
1 parent 4cf53b9 commit 5e76e34

2 files changed

Lines changed: 64 additions & 19 deletions

File tree

tests/module/MLD_host_basic.test

Lines changed: 31 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -28,17 +28,20 @@ HOST-02 (delayed Report on General Query):
2828
and then a subsequent "sending Multicast Listener Report".
2929

3030
HOST-04 (Done on leave):
31-
host1's UdpSink has stopTime=5s, which closes the socket and fires
32-
ipv6MulticastGroupLeftSignal -> Mldv1::multicastGroupLeft -> Done sent to
33-
ff02::2 (ALL_ROUTERS_2). After the Query-driven Report (t~2..3s),
34-
host1's flag=true, so Done is sent.
31+
BOTH hosts' UdpSinks have stopTime=5s. On close, ipv6MulticastGroupLeftSignal ->
32+
Mldv1::multicastGroupLeft sends a Done ONLY if the host holds flag=true. Exactly one
33+
host is the reporter (holds flag=true after the Query race) -- host1 at the pinned
34+
seed -- so host1 sends the Done and host2 leaves silently. The test asserts host1's
35+
Done and, as a %not-contains, that host2 sends none. This is the seed-pinned form of
36+
the relational property "the host that Reported is the one that sends the Done".
3537

3638
Network: host1, host2, and router all connect to a shared EthernetHub, putting
3739
them on the same Ethernet segment. Ipv6FlatNetworkConfigurator assigns addresses.
3840
All three nodes have hasMld=true. The router is a real querier (router.multicastForwarding
3941
enabled -- set at node level so NetworkLayerNodeBase propagates it to the routing table)
4042
with short startup timer so the General Query arrives within the 10s limit.
41-
RNG seed is fixed for reproducibility.
43+
The RNG seed is pinned (see the seed-set note below): an RNG shift swaps which host wins
44+
the race, so the seed may need re-picking so host1 stays the reporter.
4245

4346
%#--------------------------------------------------------------------------------------------------------------
4447
%file: test.ned
@@ -80,8 +83,17 @@ sim-time-limit = 10s
8083
cmdenv-express-mode = false
8184
cmdenv-log-prefix = "%C: "
8285

83-
# Fix RNG seed for deterministic behavior of uniform(0, maxRespTime) in startHostTimer
84-
seed-set = 0
86+
# MLDv1 answers a General Query after a random uniform(0, maxRespDelay) delay; when two hosts share
87+
# a group, the shorter delay reports first and the other suppresses (Mldv1.cc:311 and :410). So
88+
# which host ends up as the reporter -- and therefore holds flag=true and sends the Done on leave --
89+
# is an RNG coin flip. opp_test cannot express the relational property "the reporter is the host that
90+
# sends the Done, and the other sends none", so we PIN the seed to fix the roles: at seed 1 host1 is
91+
# the reporter, so host1 sends the Done and host2 (which also leaves) sends none -- exactly one Done,
92+
# from host1, as asserted below.
93+
# NOTE: a change elsewhere that shifts how many random numbers are drawn before this point can swap
94+
# the roles. If that happens, re-pick a seed where host1 wins (seeds 1, 3, 4, 6 do; 0, 2, 5, 7 do
95+
# not) -- the behavior is unchanged, only which host plays which role.
96+
seed-set = 1
8597

8698
# Enable MLD on all nodes
8799
**.ipv6.hasMld = true
@@ -100,14 +112,16 @@ seed-set = 0
100112
**.host1.app[0].typename = "UdpSink"
101113
**.host1.app[0].localPort = 1000
102114
**.host1.app[0].multicastGroup = "ff0e::1:2:3"
103-
# HOST-04: host1 leaves at t=5s (socket close fires ipv6MulticastGroupLeftSignal -> Done).
104-
# After the Query-driven Report (flag=true), Done is sent to ff02::2.
115+
# HOST-04: BOTH hosts leave at t=5s (socket close -> ipv6MulticastGroupLeftSignal). Only the host
116+
# holding flag=true (the reporter, host1 at this seed) sends a Done; the suppressed host leaves
117+
# silently. host2 also leaving is what makes "host2 sends no Done" a real check, not a tautology.
105118
**.host1.app[0].stopTime = 5s
106119

107120
**.host2.numApps = 1
108121
**.host2.app[0].typename = "UdpSink"
109122
**.host2.app[0].localPort = 1000
110123
**.host2.app[0].multicastGroup = "ff0e::1:2:3"
124+
**.host2.app[0].stopTime = 5s
111125

112126
# HOST-02: enable real querier on the router (multicastForwarding at node level so
113127
# NetworkLayerNodeBase propagates *.multicastForwarding = this.multicastForwarding
@@ -145,6 +159,14 @@ MldHostBasicNetwork.host1.ipv6.mld: Mldv1: sending Multicast Listener Report for
145159
%contains: stdout
146160
MldHostBasicNetwork.host1.ipv6.mld: Mldv1: sending Multicast Listener Done for group=ff0e::1:2:3
147161

162+
%#--------------------------------------------------------------------------------------------------------------
163+
%# CORRELATION (the other host): host2 also leaves at t=5s, but as the suppressed loser at this seed
164+
%# it holds flag=false and sends NO Done -- only the reporter (host1) does. This is the seed-pinned
165+
%# "the reporter sends the Done, the other does not" check. (See the seed-set note above: an RNG
166+
%# shift swaps the roles, and the seed would need to be re-picked so host1 is the reporter again.)
167+
%not-contains: stdout
168+
MldHostBasicNetwork.host2.ipv6.mld: Mldv1: sending Multicast Listener Done
169+
148170
%#--------------------------------------------------------------------------------------------------------------
149171
%postrun-command: grep "undisposed object:" test.out > test_undisposed.out || true
150172
%not-contains: test_undisposed.out

tests/module/MLD_host_groupstates.test

Lines changed: 33 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -39,13 +39,16 @@ TRAJ-3 ff0e::1 Query-driven (host1 receives General Query after becoming Idle
3939
HOST-02: The "received General Listener Query" line proves Idle --> DELAYING_LISTENER.
4040
The subsequent "sending Multicast Listener Report" line proves the delayed Report was sent.
4141

42-
TRAJ-4 ff0e::1 Done on leave (host1 leaves at t=5s via UdpSink stopTime)
43-
host1's UdpSink has stopTime=5s. Socket close fires ipv6MulticastGroupLeftSignal ->
44-
Mldv1::multicastGroupLeft -> Done sent to ff02::2. After the Query-driven Report
45-
(flag=true), Done is sent to ff02::2 (ALL_ROUTERS_2).
42+
TRAJ-4 ff0e::1 Done on leave (BOTH hosts leave at t=5s via UdpSink stopTime)
43+
Both hosts' UdpSinks have stopTime=5s. Socket close fires ipv6MulticastGroupLeftSignal ->
44+
Mldv1::multicastGroupLeft, which sends a Done to ff02::2 ONLY if the host holds flag=true.
45+
Exactly one host is the reporter (won the Query race) -- host1 at the pinned seed -- so host1
46+
sends the Done and host2 leaves silently.
4647

47-
HOST-04: The "sending Multicast Listener Done" line proves
48-
IDLE_LISTENER --> NON_LISTENER (leave with Done, flag=true).
48+
HOST-04: The "sending Multicast Listener Done" line from host1 proves
49+
IDLE_LISTENER --> NON_LISTENER (leave with Done, flag=true); a %not-contains proves host2,
50+
the suppressed loser, sends none. This is the seed-pinned form of "the host that Reported is
51+
the one that sends the Done".
4952

5053
Note on intermediate IDLE_LISTENER observability: timer expiry is only EV_DEBUG in Mldv1
5154
(not EV_INFO), so the IDLE_LISTENER state after unsolicited-Report-timer expiry is inferred
@@ -57,7 +60,8 @@ Network: host1, host2, and router all connect to a shared EthernetHub.
5760
Ipv6FlatNetworkConfigurator assigns /64 link-local and global addresses.
5861
hasMld=true on all nodes; dupAddrDetectTransmits=0 eliminates DAD delay.
5962
Router is a real querier (multicastForwarding=true at node level) with short timers.
60-
seed-set=0 pins uniform(0, maxRespDelay) for deterministic timer behavior.
63+
The RNG seed is pinned (see the seed-set note below): it fixes which host wins the query-response
64+
race, and thus which one holds flag=true and sends the Done. An RNG shift swaps the roles.
6165

6266
%#--------------------------------------------------------------------------------------------------------------
6367
%file: test.ned
@@ -99,8 +103,16 @@ sim-time-limit = 30s
99103
cmdenv-express-mode = false
100104
cmdenv-log-prefix = "%C: "
101105

102-
# Fix RNG seed for deterministic behavior of uniform(0, maxRespTime) in startHostTimer
103-
seed-set = 0
106+
# MLDv1 answers a General Query after a random uniform(0, maxRespDelay) delay; when two hosts share
107+
# a group, the shorter delay reports first and the other suppresses (Mldv1.cc:311 and :410), so which
108+
# host ends up as the reporter -- and therefore holds flag=true and sends the Done on leave -- is an
109+
# RNG coin flip. opp_test cannot express the relational "the reporter is the host that Dones, and the
110+
# other does not", so we PIN the seed: at seed 1 host1 is the reporter, so host1 sends the Done and
111+
# host2 (which also leaves) sends none -- exactly one Done, from host1, as asserted below.
112+
# NOTE: a change elsewhere that shifts how many random numbers are drawn before this point can swap
113+
# the roles. If that happens, re-pick a seed where host1 wins (seeds 1, 3, 4, 6 do; 0, 2, 5, 7 do
114+
# not) -- the behavior is unchanged, only which host plays which role.
115+
seed-set = 1
104116

105117
# Enable MLD on all nodes
106118
**.ipv6.hasMld = true
@@ -120,13 +132,16 @@ seed-set = 0
120132
**.host1.app[0].typename = "UdpSink"
121133
**.host1.app[0].localPort = 1000
122134
**.host1.app[0].multicastGroup = "ff0e::1"
123-
# TRAJ-4: host1 leaves at t=5s via socket close (fires ipv6MulticastGroupLeftSignal -> Done).
135+
# TRAJ-4: BOTH hosts leave at t=5s via socket close (fires ipv6MulticastGroupLeftSignal). Only the
136+
# host holding flag=true (the reporter, host1 at this seed) sends a Done; the suppressed host leaves
137+
# silently. host2 also leaving is what makes "host2 sends no Done" a real check, not a tautology.
124138
**.host1.app[0].stopTime = 5s
125139

126140
**.host2.numApps = 1
127141
**.host2.app[0].typename = "UdpSink"
128142
**.host2.app[0].localPort = 1000
129143
**.host2.app[0].multicastGroup = "ff0e::1"
144+
**.host2.app[0].stopTime = 5s
130145

131146
# TRAJ-3: real querier on the router drives the Idle -> Delaying -> Report path.
132147
# multicastForwarding MUST be set at node level: NetworkLayerNodeBase propagates
@@ -181,6 +196,14 @@ MldHostGroupstatesNetwork.host1.ipv6.mld: Mldv1: received General Listener Query
181196
%contains: stdout
182197
MldHostGroupstatesNetwork.host1.ipv6.mld: Mldv1: sending Multicast Listener Done for group=ff0e::1 on iface=eth0
183198

199+
%#--------------------------------------------------------------------------------------------------------------
200+
%# CORRELATION (the other host): host2 also leaves at t=5s, but as the suppressed loser at this seed
201+
%# it holds flag=false and sends NO Done -- only the reporter (host1) does. This is the seed-pinned
202+
%# "the reporter sends the Done, the other does not" check (see the seed-set note: an RNG shift swaps
203+
%# the roles, and the seed would need re-picking so host1 stays the reporter).
204+
%not-contains: stdout
205+
MldHostGroupstatesNetwork.host2.ipv6.mld: Mldv1: sending Multicast Listener Done
206+
184207
%#--------------------------------------------------------------------------------------------------------------
185208
%postrun-command: grep "undisposed object:" test.out > test_undisposed.out || true
186209
%not-contains: test_undisposed.out

0 commit comments

Comments
 (0)