[Proposal] Sending network messages across processes

Abstract

This draft starts the discussion on how we can support the direct sending and receiving of messages across PlusCal processes (then compiled to processes that may live in different nodes in a distributed system). The main advantage of supporting direct communication is that the resulting systems won't have to rely on global state (which needs to be exclusively acquired before use) nor on abstractions from the model checking world that have a high maintenance cost in a realistic implementation.

A network in PlusCal

PlusCal (or TLA+) has no notion of a "network". You are free to model a network however you like (and to any level of abstraction: a network may drop packets, become unavailable, duplicate messages, corrupt messages, etc).

In the two-phase commit currently being developed, network is modeled as records that associate a <from,to> tuple with a sequence of messages (that's a high-level description of the model). The relevant definitions are included below for convenience:

  define {
    send(from, to, msg) == [network EXCEPT ![from][to] = Append(@, msg)]
    broadcast(from, msg) == [network EXCEPT ![from] = [to \in 1..NumProcs |-> IF from = to THEN network[from][to] ELSE Append(network[from][to], msg)]]
  }

  macro rcv(dst, buf) {
    with (src \in { s \in 1..NumProcs : Len(network[s][dst]) > 0 }) {
      buf := Head(network[src][dst]);
      network[src][dst] := Tail(@)
    }
  }

As can be seen, the definitions above model a network with no losses or failures as a global data structure that holds all messages. Processes can send, receive, and broadcast messages. Messages can be of any form (or "type"), since there is no restrictions on the TLA+ side of things.

While PGo could naively compile the network modeled above as an actual global data structure, that would severely hurt the performance of the resulting systems:

processes would need perform polling when checking if there's any messages available;
access to the "network" would be mediated by locks, and "sending a message" would require exclusive access to the network object;
depending on the rate of message sends, the "network" object could grow considerably large, further aggravating the issue of ownership (single copy of the object is moved around across the real network during system execution).

In order to avoid these problems, PGo could be smart enough to translate message-based communication directly.

Proposal: Network operators

In the specification above, send, rcv, and broadcast are "network operators": they do nothing but maintain state of the global network data structure. PGo could support a restricted definition of such operators in order to generate code that share the same semantics.

Example: telling PGo our network operators in the compilation configuration file:

"networking": {
    "operators": {
        "variable": "network",
        "send": "send",
        "receive": "rcv",
        "broadcast": "broadcast"
    }
}

The meaning of the options above should be straightfoward.

The configuration above would cause PGo to compile the two-phase commit spec differently in the following aspects:

No declarion of the network variable. The following line would be skipped and produce no counterpart in the resulting Go AST:

  variable network = [from \in 1..NumProcs |-> [to \in 1..NumProcs |-> <<>>]];

The compiler would also skip the definitions of the network operators themselves (send, broadcast, and the rcv macro).

Sending of messages on send. The following translation could be performed (a similar translation would happen on broadcast).

    network := send(rm, TM, [type |-> state, rm |-> rm]);

runtime.SendMsg(rm, TM, map[string]string{
    "type": state,
    "rm": rm,
})

Receiving of messages on receive. The following translation could be performed:

rcv(TM, tmsg);

// buf declared as map[string]string
// blocks until a message is received
runtime.RcvMsg(TM, buf)

Other Specifications

Raft models network as a "bag" (although one not coming from TLA+'s Bags module). Messages can be duplicated or dropped (not supported in this proposal). However, the model could be easily changed to the format proposed in this draft. Instead of using mdest and msource in the message "fields", the messages could be modeled as in the two-phase commit protocol of this repository to achieve the same result.
WPaxos models networks as a set (therefore no message duplication), and does not model message drops. Sender and receiver also seem to be sent as part of the message "fields".

Both specs model messages as TLA+ records, and therefore fit the model proposed here. Such specs could reasonably be changed to accommodate the restrictions proposed.

Limitations

Messages sent on the network need to be TLA+ records. While this does seems to be the norm in protocol specifications, it is reasonable to expect that changing a spec that uses another data type to use records should require superficial changes only.
API could be more flexible (i.e., rcv operation receives a message from any process; perhaps a spec would find useful to wait for a message coming from a particular process).
As currently proposed, process identifiers need to be both numerical, sequential and the sets of process identifiers for each process need to be disjoint. This restriction is for convenience of implementation and could be relaxed on a second iteration of the design.
As with the other types of network communication in PGo, this proposal does not take failures into account.

DistCompiler / pgo