A refinement mapping using "callbacks"

[Nira Amit]

Hi group,

I'm re-posing a question of mine that hasn't been answered (probably because it was too complex and long, so I'm trying again):

I have a modular spec describing a distributed repository built around the Plumtree* protocol (a flavor of a gossip protocol, see below). My problem is this: the Plumtree spec doesn't care about the message body, obviously, because the protocol is only concerned with having all the messages delivered to all peers. Yet the DistRepo spec needs to somehow "plug-in" message creation and processing into the protocol's behavior. So in order to achieve this, I defined a couple of constant operators in the Plumtree spec, that are assumed to create a message and to process it once received. Sort of "callbacks" to pass from the implementing spec. E.g:

------------------------------ MODULE Plumtree ------------------------------

...

\* An abstraction of gossip generation, which creates some gossip message with origin <peer> and 

\* assignes it to message[peer].

\* For spec testing this is set to the TestCreateGossip(peer) operator 

CONSTANT CreateGossipMsg(_)

...

\* Generate gossip and start spreading it

\* For simplicity, the gossip message is created and assigned to message[peer], and then sent over the network to localhost 

GenerateGossip(peer) == 

    /\ msgCounter <= MAX_MSG

    /\ CreateGossipMsg(peer)  \* sets message[peer] to the new gossip message

    /\ Send( message'[peer], peer, peer )  \* gossip is sent to localhost

    /\ msgCounter' = msgCounter + 1

    /\ UNCHANGED <<pc, receivedUpdates, eagerPushPeers, lazyPushPeers, missingUpdateSrcs, timers, recipient>>

...

-------------------------- MODULE DistributedRepo --------------------------

...

\* The CreateGossipMsg implementation

CreateUpdate(peer) == \E eid \in ENTITY_ID, v \in ENTITY_VAL:

                        message' = [message EXCEPT ![peer] = 

                            [mtype |-> Gossip, 

                             mid   |-> msgCounter, 

                             mbody |-> CreateEntity(peer, eid, v),

                             msrc  |-> peer]]

...

So this works fine - TLC verifies the implementation and that the system indeed reaches consistency - but doesn't look very "elegant" to me. As a software developer it bothers me that this doesn't follow object-oriented principles where one module should not have to be aware of another one's inner state (here DistRepo has to know about the Plumtree's 'message' inner variable). On the other hand, I understand that specs are about discovering design flaws and verifying behaviors, not code modularity. So there's only so much abstraction one can expect (or want). I just wonder if there is a "cleaner" way to achieve this sort of spec interaction, that I'm not aware of. Would any of you have taken a different approach? 

The full specs are attached, as well as a screenshot of the model configuration I used for testing.

 

* The Plumtree protocol is a self-healing broadcast tree embedded in a gossip-based overlay. 

From the paper (http://homepages.gsd.inesc-id.pt/~jleitao/pdf/srds07-leitao.pdf): "The broadcast tree in created and maintained using a low cost algorithm, described in the paper. Broadcast is achieved mainly by using push gossip on the tree branches. However, the remaining links of the gossip-based overlay are also used to propagate the message using a lazy-push approach. The lazy-push steps ensure high reliability (by guaranteeing that, in face of failures, the protocol falls back to a pure gossip approach) and, additionally, also provide a way to quickly heal the broadcast tree".

[Ron Pressler]

Why does your CreateGossipMessage directly touch the message variable? Indeed, this may be problematic, as it makes the CreateGossipMsg constant a level-1 expression, and I don't think you'd even be able to pass it to an INSTANCE of Plumtree with a WITH clause, only externally through the TLC configuration (as, indeed you seem to be doing). A better approach -- so it would seem to me -- would be to change the line:

    /\ CreateGossipMsg(peer)

in the Plumtree module to:

    /\ message' = CreateGossipMsg(peer)

and have CreateUpdate "return" the message. However, then you'd lose the nondeterminstic creation of the message. This can be easily resolved with:

    /\ message' \in CreateGossipMsg(peer)

and having CreateGossipMsg return a set of possible messages.

Unrelated, I've noticed that in your configuration you use strings as some constant values (Prune, Graft, Peer). A model value may be a better fit for what you want. The problem with strings is that they cannot be tested for equality (or membership) with other, non-string sets (numbers, all forms of functions, explicit sets), while model values can be compared with anything.

Ron

[Nira Amit]

Hi Ron,

1. I didn't know that about Strings, thanks for pointing it out.

2. Regarding your suggestion: I was thinking about returning a message as you described, but couldn't find a way to make it work. If CreateGossipMsg(peer) is the set of all possible gossip messages then it quickly becomes too big for TLC to calculate. This is, of course, a technical problem and not a theoretical limitation of the language. I just saw another thread by FL suggesting a change to the CHOOSE mechanism that avoids calculating the entire set just to select a suitable member in it, this sounds like pretty much the same issue:

https://tlaplus.codeplex.com/workitem/24

I intend to dive into the TLC code and see if I can contribute, this might be a good place for me to start.

Nira.

[Ron Pressler]

On Tuesday, February 2, 2016 at 3:57:03 PM UTC+2, Nira Amit wrote:

Hi Ron,

1. I didn't know that about Strings, thanks for pointing it out.

2. Regarding your suggestion: I was thinking about returning a message as you described, but couldn't find a way to make it work. If CreateGossipMsg(peer) is the set of all possible gossip messages then it quickly becomes too big for TLC to calculate. 

I don't think you need to return the set of *all* possible gossip messages. If your original spec was:

    CreateUpdate(peer) == \E eid \in ENTITY_ID, v \in ENTITY_VAL:

                        message' = [message EXCEPT ![peer] = 

                            [mtype |-> Gossip, 

                             mid   |-> msgCounter, 

                             mbody |-> CreateEntity(peer, eid, v),

                             msrc  |-> peer]] 

your revised one can be:

    CreateUpdate(peer) = { [message EXCEPT ![peer] = 

                                                 [mtype |-> Gossip, 

                                                    mid   |-> msgCounter, 

                                                 mbody |-> CreateEntity(peer, eid, v),

                                                   msrc  |-> peer]] 

                                           : eid \in ENTITY_ID, v \in ENTITY_VAL }

The number of states you'll create is the same as in your original spec, but you're right that TLC can only handle sets much smaller than the number of states it can handle. Note, however, that you can set the size of the maximal set in the "Cardinality of largest enumerable set" option in the model's Advanced Options tab.

Ron

[Nira Amit]

Ron, 

This works and I like it better than the way I had written this, but it still involves DistRepo setting an internal variable of spec Plumtree (message). Maybe I'm just confused about the syntax but here's what I'd like to do and don't see how:

In spec Plumtree:

GenerateGossip(peer) == 

    /\ msgCounter <= MAX_MSG

    /\ message' = [message EXCEPT ![peer] = 

                                 [mtype |-> Gossip, 

                                  mid   |-> msgCounter, 

                                  mbody |-> <GET ME A RANDOM MESSAGE BODY>,

                                  msrc  |-> peer]]

    /\ Send( message'[peer], peer, peer )  \* gossip is sent to localhost

    /\ msgCounter' = msgCounter + 1

    /\ UNCHANGED <<pc, receivedUpdates, eagerPushPeers, lazyPushPeers, missingUpdateSrcs, timers, recipient>>

Do you see a way to do this? Actually even CHOOSE won't help me here because it is deterministic, and I want a (possibly) different message in different behaviors.

Thanks again,

Nira.

[Nira Amit]

^^ 

[Ron Pressler]

In Plumtree:

    /\ message' \in { [message EXCEPT ![peer] = msg] : msg \in GenerateGossip }

In the other module:

     CreateUpdate(peer) == { [mtype |-> Gossip, 

                                                    mid   |-> msgCounter, 

                                                 mbody |-> CreateEntity(peer, eid, v),

                                                   msrc  |-> peer]

                                           : eid \in ENTITY_ID, v \in ENTITY_VAL }

Now there's no access to message (sorry I confused you before). The same "randomness" (really nondeterminism) you had before is preserved now. 

[Ron Pressler]

On Tuesday, February 2, 2016 at 5:17:03 PM UTC+2, Ron Pressler wrote:

In Plumtree:

    /\ message' \in { [message EXCEPT ![peer] = msg] : msg \in GenerateGossip }

That should be:

    msg \in CreateUpdate(peer)

 

[Nira Amit]

Hi Ron,

It works! Thanks!!

So to sum it up: my problem was that I couldn't find a way to blindly select a gossip message-body from within the Plumtree module when it is implemented by another spec. Declaring the body to be \in the constant set of all possible message bodies would result in calculating this set, which can be very big. But it was actually possible to narrow down the set of relevant message bodies substantially.

This is probably not a silver-bullet solution for all such cases, but for now I have my spec nicely broken down into fairly independent modules, so I'm happy :-)

For reference, I'm adding here a summery of the changes and attaching the modified specs:

In module Plumtree:

...

\* The set of possible message bodies for gossip-messages with origin <peer>

\* For spec testing this is set to the MBody constant for all peers 

CONSTANT GossipMsgBody(_)

ASSUME \A p \in Peer: GossipMsgBody(p) \in SUBSET(MBody) 

...

\* The set of possible gossip messages with origin <peer>

GossipMsg(peer) == { [mtype |-> Gossip, 

                      mid   |-> msgCounter, 

                      mbody |-> body,

                      msrc  |-> peer]

                    : body \in GossipMsgBody(peer) }

...

\* Generate gossip and start spreading it

\* For simplicity, the gossip message is created and assigned to message[peer], and then sent over the network to localhost 

GenerateGossip(peer) == 

    /\ msgCounter <= MAX_MSG

    /\ message' \in { [message EXCEPT ![peer] = msg] : msg \in GossipMsg(peer) }

    /\ Send( message'[peer], peer, peer )  \* gossip is sent to localhost

    /\ msgCounter' = msgCounter + 1

    /\ UNCHANGED <<pc, receivedUpdates, eagerPushPeers, lazyPushPeers, missingUpdateSrcs, timers, recipient>>

...

And in module DistributedRepo:

...

\* The GossipMsgBody implementation

CreateUpdate(peer) == { CreateEntity(peer, eid, v)  

                         : eid \in ENTITY_ID, v \in ENTITY_VAL }