microsoft / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
223 stars 80 forks source link

Broadcast scenario in Ivy #58

Closed prasitaGit closed 4 years ago

prasitaGit commented 4 years ago

Suppose I have n nodes and I would want to send the id of a particular node to all other n - 1 nodes, on the reception of which the nodes would have to perform a certain task. I want to embed the sending of id in the form of action (say : call sendnodes(n.id, nodes) ). Here sendnodes is my action, n.id is the id of node n and nodes are the set of all other nodes.

Ex : In leader election protocol, we just have to send id to the next node only, which is fetched by get_next function. Say I would like to send id to all nodes and not just the next node and would like to do it in the form of action and not relation. However, I am not able to figure out how to do this. I can create a relation send, and set it to true for all nodes N. But that does not work in my case as I need to perform some action in each of the nodes on reception and hence I would like to have action like sendnodes. Any insights would be highly helpful to me.

kenmcmil commented 4 years ago

If you are making an abstract model, then there are various ways to do broadcast, depending on what transport properties you want to assume. For example, if you are assuming the possibility of duplication, you can just create one relation sent that tells you what messages have been broadcast (regardless of the receiver). The abstract protocol action that corresponds to receiving this message will have a parameter corresponding to the id of the receiver (in other words, the reception each each node is a distinct event). If you need to assume non-duplication (let's say you are intending to use TCP as your transport) then you would have sent(D,M) where D is the destination and M is the message. You can send to all destinations like this:

sent(D,m) := true;  # send message m to all destinations

Here, D is a placeholder that stands for all destinatons. Then in your receive action you have:

action process_message(receiver:node, m:message) = {
    require send(receiver,m);
    sent(receiver,m) := false;
    # handle message here
}

This models removal of the message from the network (and works so long as you don't allow multiple copies of a message in the network at the same time).

Now if you want to implement broadcast messaging on the actual network, you need to make a network "shim" that sends to all nodes in a loop. I can provide an example of that if you need it.

prasitaGit commented 4 years ago

I actually want to implement broadcast messaging on the actual network. it'd be great if you could provide an example.

kenmcmil commented 4 years ago

bcast.zip