Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Simulating USCarrier.nv may not converge #68

Open
alberdingk-thijm opened this issue May 25, 2021 · 6 comments
Open

Simulating USCarrier.nv may not converge #68

alberdingk-thijm opened this issue May 25, 2021 · 6 comments
Labels
help wanted Extra attention is needed question Further information is requested

Comments

@alberdingk-thijm
Copy link
Collaborator

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?
@alberdingk-thijm alberdingk-thijm added the bug Something isn't working label May 25, 2021
@alberdingk-thijm
Copy link
Collaborator Author

Uncommenting lines 129-131 and then running nv -v -s benchmarks/SinglePrefix/TopologyZoo/USCarrier.nv reveals that the BGP aslen appears 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)

@DKLoehr
Copy link
Collaborator

DKLoehr commented May 25, 2021

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.

@alberdingk-thijm
Copy link
Collaborator Author

alberdingk-thijm commented May 25, 2021 •
edited
Loading

I believe the NV file was generated using NetComplete configs per @nickgian. Unlike the fattree benchmarks, its transfer updates 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.

@alberdingk-thijm alberdingk-thijm added help wanted Extra attention is needed question Further information is requested and removed bug Something isn't working labels May 25, 2021
alberdingk-thijm added a commit that referenced this issue May 25, 2021
@alberdingk-thijm
Add maintenance benchmarks
8844946 
Add benchmarks for maintenance in fatXPol networks, and allow them to be
benchmarked by kiribench.py.
Add code to generate hMETIS-cut networks with gen_part_nv, although our
current examples for USCarrier.nv don't appear to be useful since its
simulation diverges (see issue #68).
Do some minor reformatting in Simulator.ml and Srp.ml
@nickgian
Copy link
Collaborator

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/469ac32f8b89a3baf6985e09bbb1b78e

This 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?)

@alberdingk-thijm
Copy link
Collaborator Author

Yeah, my guess is that there is no solution so SMT just returns unsat anyway.
It looks like the examples/uscarrier/USCarrier.nv example works as expected, although I'm not quite clear on what's different there versus in benchmarks/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?

@nickgian
Copy link
Collaborator

Sure, get rid of it, and maybe drop in the replacement I posted here?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
help wanted Extra attention is needed question Further information is requested
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@nickgian @DKLoehr @alberdingk-thijm