Repository navigation
Simulating USCarrier.nv may not converge #68
Description
Activity
Uncommenting lines 129-131 and then running
nv -v -s benchmarks/SinglePrefix/TopologyZoo/USCarrier.nvreveals that the BGPaslenappears to be continuously increasing. I'll take a look at how the policy is written for any obvious signs of bugs.Processing benchmarks/SinglePrefix/TopologyZoo/USCarrier.nv partial eval took: took: 0.012090 secs to complete L(102): (None,None,None,None,None) L(102): (Some (11u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (13u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (15u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (17u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (19u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (21u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (23u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (25u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (27u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (28u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (29u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (31u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (33u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (35u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (37u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (39u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (41u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (43u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (45u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (46u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (47u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (49u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (51u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (53u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (55u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (57u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (59u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (61u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (63u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (64u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (65u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (67u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (69u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (71u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (73u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (75u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (77u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (79u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (81u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (82u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (83u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (85u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (87u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (89u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (91u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (93u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (95u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (97u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (99u32,20u8,{ 6553613u32 |-> true; 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None) L(102): (Some (100u32,20u8,{ 6553615u32 |-> true; 6553606u32 |-> true ; _ |-> false},100u32,80u32),None,None,Some 3u2,None)I didn't work on this example -- is it possible it just doesn't converge? Even if stable solutions exist, I don't think the simulator is guaranteed to find one. BGP length increasing is suspicious as well.
I believe the NV file was generated using NetComplete configs per @nickgian. Unlike the fattree benchmarks, its
transferupdates local preference, so it's likely non-monotonic. It's certainly possible it just never converges, particularly if something happens to cause the local preference to continuously toggle between states. At any rate, it would be good to figure out if that's the case, and I can make a note in the file.- added a commit that references this issue
on May 25, 2021 I am sorry about that, weird that this problem went under the radar for so long. Perhaps we were trying a different prefix. You are right the problem appears to be the local-pref.
Here's a version of that network that keeps track of the set of nodes traversed through BGP and disallows cycles. I generated with that other version of the translation pipeline.
https://gist.github.com/nickgian/469ac32f8b89a3baf6985e09bbb1b78eThis converges normally. The question that may concern you the most is whether the SMT solver is finding the right solution. By verifying you mean you get unsat? In this case unsat might mean that there is no solution that converges. I'd be impressed if there is a stable state and the simulator just cannot find it because of the order it follows (do we know of any such examples?)
Yeah, my guess is that there is no solution so SMT just returns unsat anyway.
It looks like theexamples/uscarrier/USCarrier.nvexample works as expected, although I'm not quite clear on what's different there versus inbenchmarks/SinglePrefix/TopologyZoo/USCarrier.nv, beyond just a different ordering of declarations. I think this may just be a case of one badly-configured example. Should we get rid of it?Sure, get rid of it, and maybe drop in the replacement I posted here?
Reacted by Tim Alberdingk Thijm
I've been trying to get results from simulating
benchmarks/SinglePrefix/TopologyZoo/USCarrier.nv, but while I can verify it in SMT in about a minute, simulation appears to hang.Uncommenting the print statement at
Srp.ml#L141(which shows the currently-processed node in simulating state) leads to a very, very long sequence of nodes being output.I can't confirm that this sequence repeats yet, but it does look fishy in comparison to other benchmarks where this process typically finishes very quickly. Does anyone know what's going on with this benchmark?