Simulating USCarrier.nv may not converge

[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?

[alberdingk-thijm]

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]

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]

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.

[nickgian]

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]

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]

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