DSL For Common Patterns In Distributed Protocols

DSL For Common Patterns In Distributed Protocols

Two common patterns at the moment recur across the body of examples we have demonstrating the applicability of the DiSeL framework.

• A 2-way communication channel in which one end asks a question and waits for the answer, and the other end does some work upon receiving the question and computing the answer. In some sense this corresponds to a remote procedure call: we are interested in some property of another node, so invoke some code on it to obtain this information.
• A 1-way communication channel in which one end notifies the other of some event occurring. In some sense this corresponds to an event-listener pattern.
• A 1-to-many broadcast in which an initiator polls a designated quorum of receivers and waits for all of them to reply.

Setting up an RPC in DiSeL requires a total of 4 separate transitions to be defined, along with transformations on states, pre- and post-conditions and messages, etc.

Conceivably we can invent a notation for describing such a system of communication channels, or perhaps just parts of it - and mechanically compute the definitions of the required transitions, lifting the examples size for DiSeL examples a notch.

Example

As part of the Lease based locking protocol, a resource guarded by a lock must verify the sequence number offered by a client to be the active sequence number. So we can specify this 'transaction' as an RPC, invoked by the resource 'on' the lock.

The resource sends the sequence number provided by the client to the lock, which in turn responds with a boolean indicating whether the two agree.

Alternatively, the resource pings the lock for the current sequence number, and performs the comparison locally. We explore both in what follows:

IS_ACTIVE : Nat -> Bool {
  client_transition : CState -> Maybe (Nat, Bool -> CState)
  server_transition : Nat -> SState -> Maybe (Bool, SState)
}

We specify the state transition of the client by a partial function CState -> Maybe (Nat, Bool -> CState), partiality used to model whether the transition is allowed from that particular state, the first component of the tuple is the Nat to send over the channel, and the continuation computes the state upon reception of the answer from the server. The idea is for the client to block upon initiating the RPC, so we can specify the entire transaction from the client perspective in this single specification.

The server side is similar: upon receiving the sequence number, we model whether a given state can handle the message using partiality and compute the response in addition to the updated server state. We give them implementations here:

ResourceState = Idle
              | PendingWrite Nat NodeID
              | Rejected NodeID

CState = Resource {
  value : Nat,
  outstanding_requests : [ResourceRequests],
  state : ResourceState
}

SState = Lock {
  next_token : Nat,
  held_token : Maybe Nat,
  outstanding_requests : [LockRequests]
} 

IS_ACTIVE : Nat -> Bool {
  client_transition : CState -> Maybe (Nat, Bool -> CState)
  client_transition cs = 
    match outstanding_requests cs, state cs with
      | (Update, [t, v], from) \+ oreqs, Idle -> 
          Just (t, \isValid ->
            if isValid
            then cs { outstanding_requests <- oreqs, pending_write <- PendingWrite v NodeID }
            else cs { outstanding_requests <- oreqs, pending_write <- Rejected NodeID }
      | _ -> Nothing

  server_transition : Nat -> SState -> Maybe (Bool, SState)
  server_transition n ss =
    match outstanding_requests ss, held_token ss with
      | (IsActiveRequest, [t], from) \+ oreqs, Just t' ->
          Just (t == t', ss { outstanding_requests <- ore's }
      | _ -> Nothing
} 

This RPC pattern involves a total of 4 transitions and two messages.

• client_send_is_active_request
• server_receive_is_active_request
• server_send_is_active_response
• client_receive_is_active_response

Messages are defined as follows:

 IsActiveRequest(Nat)
 IsActiveResponse(Bool)

We can then give the following pre- and post-conditions on the 4 transitions based on the above implementation in the DSL:

client_send_is_active_request - sender n, message m, receiver to
requires: n = Resource, 
          to = Lock,
          n >-> ls,
          client_transition ls = Just (t, k),
          m = (IsActiveRequest, [t])
ensures: n >-> BlockingOnIsActive(k)

server_receive_is_active_request - receiver n, message m, sender from
requires: n = Lock,
          m = (IsActiveRequest, [t]),
          n >-> ls, 
          server_transition t ls = Just (ans, ls')
ensures: n >-> ReturnToIsActive(ans, ls', from)

server_send_is_active_response - sender n, message m, receiver to
requires: n = Lock,
          to = Resource,
          n >-> ReturnToIsActive(ans, ls', to),
          m = (IsActiveResponse, [ans]),
ensures: n >-> ls'

client_receive_is_active_response - receiver n, message m, sender from
requires: n = Resource,
          from = Lock,
          n >-> BlockingOnIsActive(k)
          m = (IsActiveResponse, [ans])
ensures: n >-> k ans

So, this went and became a higher order spec, but perhaps there are ways around this. Manual defunctionalization?

Scratch Area - Ignore

In general, the shape is as follows:

type ClientState
type ServerState

RPC : ReqType -> AnsType {
   client_transition : ClientState -> Maybe (ReqType, ClientContext)
   client_receive : AnsType -> ClientContext -> ClientState
   server_transition : ReqType -> ServerState -> Maybe (AnsType, ServerState)
}

with transitions

client_send_RPC_request - sender n, message m, receiver to
requires: n >-> ls,
          client_transition ls = Just (req, ctx)
          m = (RPCRequest, [req])
ensures: n >-> BlockingOnRPC(ctx)

server_receive_RPC_request - receiver n, message m, sender from
requires: m = (RPCRequest, [req]),
          n >-> ls, 
          server_transition req ls = Just (ans, ls')
ensures: n >-> ReturnToRPC(ans, ls', from)

server_send_is_active_response - sender n, message m, receiver to
requires: n >-> ReturnToRPC(ans, ls', to),
          m = (RPCResponse, [ans]),
ensures: n >-> ls'

client_receive_is_active_response - receiver n, message m, sender from
requires: n >-> BlockingOnRPC(ctx)
          m = (RPCResponse, [ans])
ensures: n >->  client_receive ctx ans