On The Distributed Resource Allocation Protocol

Distributed Resource Allocation Problem

 

Distributed Resource Allocation Protocol Description

The objective of the protocol is to enable safe distributed atomic reservation of a collection of resources. For instance any two distinct agents \mathsf{A_0} and \mathsf{A_1} may require any resource collections \mathsf{r_0} and \mathsf{r_1}, where \mathsf{r_0, r_1 \subseteq R}.

The protocol must guarantee that each agent gets all or nothing – partial request satisfaction is not permitted – and ensure that every agent request will be eventually satisfied as long as certain degenerated situations are avoided. A resource itself has an attributed memory, where requests can be stored together with a read pointer \mathsf{rp}(r_k), and a promise pointer \mathsf{pp}(r_k) – the largest {promised} index in the \mathsf{r_k} request pool.

\noindent \textbf{Stage 1} In this stage an agent attempts to negotiate a distributed lane. The negotation process continues until a lane is negotiated.

\noindent \textbf{Request} An agent \mathsf{A_i} which intends to lock a collection of resources \mathsf{res \subseteq R} generates a request to request pools associated with resources \mathsf{res}. Such requests are sent and received in no particular order and contain only agent name A_i. We define such message as \mathsf{request(A_i)} and write \mathsf{request(A_i) \rightarrow r_k} to state it is addressed to resource \mathsf{r_k \in \mathbf{res}}.

\noindent \textbf{Reply} Once a request pool \mathsf{r_k} receives request \mathsf{request(A_i)} it replies with a promised pointer index \mathsf{reply(\mathsf r_k, {pp}(r_k))} \rightarrow A_i and then increments \mathsf{pp}(r_k).

\noindent \textbf{Confirm} After sending all \mathsf{request(A_i)} messages an agent \mathsf{A_i} awaits for all replies to arrive which carry values \mathsf{pp}(r_k). Depending on the collection of reply values following actions should be taken:

\textbf{Write} If all reply values on reception are equal then \mathsf{A_i} should write at index \mathsf{n} to request pools \mathsf{write(A_i, n) \rightarrow r_k}.

\textbf{sRequest} If all values on reception are not equal then the agent must renegotiate a new index. This time an agent sends new (special) requests to resources. We define such message as \textbf{\mathsf{srequest(A_i, max+1) \rightarrow r_k}}.

\textbf{sReply} Once a request pool \mathsf{r_k} receives a special request it replies with the following message \mathsf{reply(\mathsf r_k, max) \rightarrow A_i} where \mathsf{max} the maximum value of the current \mathsf{pp(r_k)} value or received \mathsf{srequest(A_i)} index.

Rendered by QuickLaTeX.com

\noindent {\textbf{Stage 2}} This stage begins when an agent completes negotiating its distributed lane. The original version of this stage was trivial and only consisted of \mathsf{pReady}, \mathsf{Consumption} and \mathsf{Release} steps and basically was just a single message sent by resource to an agent to inform the resource can be consumed now. But, due to possible write message arrival delays another kind of deadlock could have been present in our system.

\noindent \textbf{pReady} A pre-ready message is sent by a resource to inform a next in line agent that it is available for consumption and we define such message \mathsf{pready(\mathsf r_k) \rightarrow A_i}.

\noindent \textbf{Lock} An agent waits for all pre-ready messages to arrive and once it receives them it sends a lock message to resources as follows \mathsf{lock(\mathsf A_i) \rightarrow r_k}.

\noindent \textbf{Respond} A request pool \mathsf{r_k} which receives a lock message will respond with a message \mathsf{respond(\mathsf r_k, response) \rightarrow A_i} where \mathsf{response \in {confirm, deny}}. The \mathsf{confirm} message is sent if resource has not been locked by other agent yet. If confirm message is sent, the request pool suspends sending pre-ready messages until an unlock or release message is received. If resource was locked beforehand – a \mathsf{deny} message is sent.

\noindent \textbf{Decide} An agent waits for all respond messages to arrive and depending on these messages following actions will be taken.

\textbf{Release} If one of the messages is a deny message, an agent \mathsf{A_i} will send an release messages to all resources which replied with confirm message. We define such message as follows
\mathsf{release(A_i) \rightarrow r_k}.

\textbf{Consumption} If all messages were confirm messages, an agent \mathsf{A_i} can proceed with resource consumption.

\noindent \textbf{Release} An agent \mathsf{A_i} will eventually release a resource by sending a message to all consumed resources, as follows \mathsf{release(A_i) \rightarrow r_k}. Once resource receives a release message, it will remove the request from its request pool and will update the read pointer to the the next minimum value.


Rendered by QuickLaTeX.com

Formal Protocol Model in Event-B

We apply the Event-B formalism to develop a high-fidelity functional model and prove the protocol functional correctness requirements.

Event-B Model: Refinement Plan

Abstract Model: Context C_0

Abstract Model: Machine M_0

Abstract model events for consuming and releasing objectives

First Refinement: Machine M_1

The refinement step \mathsf{M_1} expands on the previous refinement by introducing resources into the model. Instead of simply consuming an objective an agent captures resources until an objective is fulfilled. Captured resources are stored in newly created variable \mathsf{capt} whereas objective an agent will try to complete in the function \mathsf{objt}.

In contrary to capturing a single objective an agent might need to consume multiple resources in order to fulfil its objective. For the iterative process we previously introduced a two event pattern which we instantiate in this refinement step for capturing and releasing events. The loop body event \mathsf{agent\_consume\_b} takes any agent with previously initialised objective and assign a new resource to the variable \mathsf{capt}. The agent must be at \mathsf{CONSUME} state and the resources must be within agent’s objective and not yet be captured by any agent.

The loop completion event \mathsf{agent\_consume\_c} would be triggered as soon as the objective has been fulfilled (guard \mathsf{g_1}) and program counter would be updated to new state – \mathsf{RELEASE}. Similarly in this refinement we transform \mathsf{agent\_release} event according to the pattern presented.

Message Modelling: Contexts C_{mes.} and Machine Variables

The second group of contexts are used to define various message types and a separate context is created for an individual message type. In fact message contexts can be generalised in the following pattern and instantiated to the specific message type in the Event-B model.

To begin with we create a generic message carrier set \mathsf{MSG} which is used as an extractor in constant functions. Three constant functions are defined for messages: message source, message destination and optionally a message value. Depending on the message type the source of the message can be both agents and resources thus in our general form example we simplify to a general source \mathsf{SRC} function range. Likewise for the message destination constant functions form we give a general destination \mathsf{DST} the message. All constant message functions are surjective functions meaning they are total in domain and range and therefore \mathsf{VAL} must be interval for messages which carry a natural number. Lastly in addition to constant function axioms we introduce another axiom which states that there always exists a suitable message between any agent and resource.

To introduce a new message type in the machine we extend that machine with a specific context and introduce a three letter message channel variable. As messages are added and removed from the channel typically local variable (\mathsf{inv_2}) must be introduced when an agent needs to track what messages have been sent. The channel variables are modified by message sending events and we identified two message sending event patterns.

Communication Modelling Example: \mathsf{LOCK} message (Ref. \mathsf{M_2})