Closed alberdingk-thijm closed 4 years ago
Changing the merge at node 0 to x + 1
gives Label(0):2u32
in SMT and Label(0):31u32
in simulation.
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.
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?
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).
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).
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.
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...
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.
Hmm, right. I was hoping there could be a trick which wouldn't involve changing the attribute type, but that may indeed be unavoidable.
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).
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.
The following example (uploaded at
examples/funky-merge.nv
) gives divergent results under SMT and simulation. Neither case gives the expected result, whereL(0n) = 30
andL(3n) = 1
.Under SMT, we get:
Under simulation, we get: