Unexpected merge behaviour during simulation and SMT when "throwing away" values

[alberdingk-thijm]

The following example (uploaded at examples/funky-merge.nv) gives divergent results under SMT and simulation. Neither case gives the expected result, where L(0n) = 30 and L(3n) = 1.

type attribute = int

let nodes = 3

let edges = {
  0=1;
  1=2;
  2=3;
}

let trans edge x = x + 1

let merge node x y = match node with
  | 3n -> y (* change to sent value *)
  | 0n -> x (* keep current value *)
  | _ -> if x < y then x else y

let init node = match node with
  | 0n -> 30
  | 1n -> 0
  | 2n -> 10
  | 3n -> 20

let assert node x = match node with
  | 0n -> x = 30
  | 1n -> x = 0
  | 2n -> x = 1
  | 3n -> x = 1

Under SMT, we get:

Processing examples/funky-merge.nv
Inlining took: 0.000015 secs to complete
Map unrolling took: 0.000025 secs to complete
Inlining took: 0.000003 secs to complete
Unbox options took: 0.000026 secs to complete
Flattening Tuples took: 0.000040 secs to complete
Partially Evaluating Network took: 0.000014 secs to complete
Encoding network took: 0.000234 secs to complete
Compiling query took: 0.000042 secs to complete
Z3 stats:
  :memory              3.11
 :time                0.00)
Slice 0 took: 0.015009 secs to complete

Label(0):1u32
Label(1):0u32
Label(2):1u32
Label(3):20u32
Failed: assertion for node 0
Failed: assertion for node 3

Entire Program took: 0.015735 secs to complete

Under simulation, we get:

Processing examples/funky-merge.nv
Interpreted simulation took: 0.000063 secs to complete

Label(0):30u32
Label(1):0u32
Label(2):1u32
Label(3):2u32
Failed: assertion for node 3

Entire Program took: 0.000572 secs to complete

[alberdingk-thijm]

Changing the merge at node 0 to x + 1 gives Label(0):2u32 in SMT and Label(0):31u32 in simulation.

[nickgian]

That seems "normal" to me.
The SMT encoding considers x to be the received message and y to be the current message (so it's the other way around than your comments).
The simulator seems to consider the other order and the computed result is correct with that.

In general, if your merge function is not commutative and associative then something's wrong because the order of messages impact the result. Here you assumed a different order than the one picked by our tools and you got different results. Nothing that can be done to "fix" this on the tooling side. Closing but feel free to further discuss/reopen.

[alberdingk-thijm]

Perhaps SMT and the simulator should at the very least agree on one order? I don't really see why they should differ on that.
Once I flip the order and fix the typo in the assert (since 3n should actually have value 2), the SMT passes.

The idea is simply that for node 0, the value should always remain the initial value, which is commutative and associative so should work.
The case for node 3 is that the value should be exactly the one computed by its single neighbour. Maybe there's a better way to write those cases?

[DKLoehr]

I agree that we should be consistent in our ordering. However, remember that if your neighbor n has attribute y, then merge will receive trans y instead of y. So as currently written, node 3 should be exactly one greater than its neighbor. The only way to get around this is if your trans function is injective (which it is here).

[nickgian]

It's probably not very difficult for me to change the simulator or SMT to have the expected behavior here, but it's also kind of pointless IMO, this is very implementation-specific.
The two analyses can be made consistent in this case because you care about the order between incoming messages and init route. If the order of messages matters too then there is nothing that can be done.

The idea is simply that for node 0, the value should always remain the initial value, which is commutative and associative so should work.
The merge function needs to be commutative and associative, i.e. merge u x y = merge u y x and merge u x (merge u y z) = merge u (merge u x y) z
merge 0 is not here.

Your best bet is to change your nv program to capture these invariants explicitly instead of relying on orderings.
For instance, you can set the merge function for 0 to be 30 if that's what you want. Or you can use a boolean to explicitly describe the "keep the current value" invariant (your transfer function must respect this invariant then).

[alberdingk-thijm]

Gotcha, thanks for the input both of you.
The node 0 case seems easy enough to write an invariant for, which is certainly something I can rely on.

Is there a way to capture the invariant neatly for the node 3 case, where label(3n) = trans(2n~3n, label(2n))? This is something I'm having a bit more trouble with.

[nickgian]

any time.

I guess the idea is that you want your attributes to explicitly capture these ideas. So your attribute should capture the fact that "hey this is the route I want!". Again you could have a tuple, with a boolean that means "is this route coming from 2??" and then act upon that. Or more generally you could have a tuple that captures the node that sent you the route then do something like if (sender = 2n) then... else...

[DKLoehr]

Perhaps a little more simply, you could handle both cases by attaching a boolean to your attribute which indicates if that attribute is the local one or the one from trans. It would be always set to true by the transfer function, and always set to false at the end of the merge function. In the middle of the merge function, it would let you tell the attributes apart.

[alberdingk-thijm]

Hmm, right. I was hoping there could be a trick which wouldn't involve changing the attribute type, but that may indeed be unavoidable.

[DKLoehr]

Well, I patched the smt solver so that it uses the same order as the simulator, so for now you can just use that. Be wary of the version which always takes its neighbor’s attribute, though. If it has multiple neighbors with different attributes, then its final state depends on message ordering, which is undesirable. If it only ever has one neighbor, you should be fine.

By the way, remember that you can modify the transfer function to be the identity along specific edges. That lets you ensure the value at node 3 (in your example) is exactly the same as node 2).

[alberdingk-thijm]

Thanks, Devon. This is for input/output nodes so the topology should never lead to a case where a node which takes its neighbour's attribute has more than one in-edge (and it will always be a sink). I'll make a note that for future-proofing, this should be changed to something more robust.