Proving Protocol’s Probabilistic Termination with PRISM

The progress of the protocol relies on agents ability to negotiate a distribute lane. As negotiating a distributed lane is a probabilistic process in our protocol we need to demonstrate that a desired state will be eventually reached. Because of reasons explained before instead of Event-B we use a well-known symbolic probabilistic model checker – PRISM for ensuring liveness requirement. However, the drawback of using PRISM model checker, if a bounded problem abstraction cannot be found, the verification is limited to bounded models.

PRISM Generic Protocol Model


To model the distributed lane negotiation protocol we use the Discrete Time Markov Chains framework from the PRISM model checker. The generic model can be partitioned into three main parts: global variable declaration, resource modules and agent modules.

\noindent\textbf{Global Variables.} There are two types of global variables \mathsf{a_{nm}} and \mathsf{aon_{nm}} and both types are associated with agents. The first variable \mathsf{a_{nm}} is used to model \mathsf{stage_{1}} messages exchanges between an agent \mathsf{n} and resource \mathsf{m}. So, if one wants to model a scenario where an agent \mathsf{a_{0}} wants to lock resources \mathsf{r_{0}, r_{1}} two global variables \mathsf{a_{01}} and \mathsf{a_{10}} (initially set to 0). The second variable \mathsf{aon_{nm}} is a status variable and similarly to the previous one, a separate variable is created for every agent-resource relation in the scenario. The status variable can take two possible values ([0..1] init 1) and are used to update probabilities as well as control models flow. The following paragraphs explain how these variables are modified.

\noindent\textbf{Resource Modules.} For each resource an individual resource module is created which contain a local promised pointer variables and single command. Two parameters which can be varied for the \mathsf{ppt_m}: initial value (or the promised pointer offset) and the upper bound of the promised pointer. The module also only requires a single command which is expressed below. The additional guards are mainly added to protect from variable overflows and terminate model once distributed all distributed lanes negotiated.

\mathbf{module} \mathsf{r_m}

\mathsf{ppt_m \: : \: [0\:..\:T] \: init \: T_n;}

\mathsf{[] \quad additional\_guards \quad \& \quad (aon_{am} \: + \: aon_{bm} \: + \: aon_{cm} \: +  \cdots > 0) \rightarrow}

\mathsf{(ppt_m'={max}(a_{am}, ppt_m) + 1) \quad \& \quad (aon_{am}'=0) + \cdots ;}
\mathbf{endmodule}

\mathsf{(ppt_m'={max}(a_{am}, ppt_m) + 1) \quad \& \quad (aon_{am}'=0) + \cdots ;}

\mathbf{endmodule}

The main guard uses agent status variables \mathsf{aon_{nm}} to activate module only if there is at least one agent which is interested in reserving that resource but has not received a promised pointer value. Then for each interested agent, there is an associated probabilistic state transition. A probability of specific state transition is inversely proportional to the number of remaining agents which have not yet received a promised pointer value from that resource. The specific state transition will update variables \mathsf{a_{am}}, \mathsf{ptt_{m}} and will deactivate status variable \mathsf{aon_{am}} by setting it to zero. All interested agents have structurally identical expression in the command with modified variable identifiers (after +).

Generating PRISM Protocol Instances

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})