Modeling Streamlet (take two)

This post is a sequel to my last two posts on Streamlet. The first one explained the protocol. The second one presented a first draft modeling of the protocol.

In this post, I present two improvements to the first draft modeling.  In the first, I will make the epochs monotonic at the process level. In the second one, I give each node its own inbox, instead of using a shared whiteboard message set. Again, I will introduce the model dev-log style, using the notes I took while developing it.

Adding locally monotonic epochs

Why don't I just sequentially increase e in the process main loop. Instead of using while true, with e \in E, the process will go through the epochs in increasing order. This still doesn't constrain the processes to go in lock-step through the epochs. Each process can go through epochs in its own pace independent of the others. The only requirement is if a process participated at an epoch (either as a proposer or voter), it will not participate at a lower epoch number. This is locally enforcable at each process even in a completely asynchronous environment.

So here is the model, the change being only in process method at the end.

Making the epochs monotonic per process did wonders on the  model checking time. Now model checking is a blast. In the first model, checking chains longer than 4 took more than five minutes, in this model, checking chains of length 10 are almost instant. 

Adding per process mailboxes

Now that I have a very fast model, I can add per process message boxes to this model to check if there was any hidden concurrency problem missed in the shared whiteboard message set. 

In order to give each node its own inbox, I will make the Msgs set an array of sets. 

variable Msgs=[n \in Nodes |->

{[chain|-> <<0>>, epoch|->0, sender|->0],

[chain|-> <<0>>, epoch|->0, sender|->1],

[chain|-> <<0>>, epoch|->0, sender|->2]}];

Then I will drop the vote and propose message to the inbox of each process separately. This requires doing a while loop iteration. I can't do these in the macros, so I will just inline the macros in the process code. Here is the resulting model.

Consistency == \A i,j \in Nodes: ThreeCons(nChain[i]) /\ ThreeCons(nChain[j]) /\ Len(nChain[i])=< Len(nChain[j])                                  

=> \A k \in 1..Len(nChain[i]): 

            nChain[i][k]=nChain[j][Len(nChain[j])-Len(nChain[i])+k]

OK, Consistency still works. Recall that my consistency condition is actually stronger than what is in the theorem because I am taking the last block also into account. Even with that consistency still checks out. This time I have per process inboxes, rather than atomic/unequivocal shared message set communication. 

I think the reason this still checks is because of combination of two things. The first is the monotonic epoch condition I added. The second is that even though we have per process inboxes, the messages are delivered immediately to all the processes before the sender moves to the next epoch. I think this will involve making the inboxes a queue where messages are appended by the sender and separately the receiver will need to asynchronously remove the head of the queue. Still a message pool can be used for the received messages, so the rest of the model can be salvaged. It seems like more work and I will stop here.