# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 5 Case Study  
Finally, we demonstrate our verification approach on a well-known version of the leader election protocol [46] that is based on shared memory. Most importantly, this case study shows how our approach bridges the typical abstraction gap between process algebraic models and program implementations. In particular, it shows how a high-level process algebraic model of a leader election protocol, together with a contract for this model (checked with mCRL2 for various inputs), is formally connected to an actual program implementation of the protocol, using VerCors.  
The protocol is performed by \(N\) concurrent workers that are organised in a ring, so that worker \(i\) only sends to worker \(i+1\) and only receives from worker \(i-1\), modulo \(N\). The goal is to determine a leader among these workers. To find a leader, the election procedure assumes that each worker \(i\) receives a unique integer value to start with, and then operates in \(N\) rounds. In every round, (1) each worker sends the highest value it encountered so far to its right neighbour, (2) receives a value from its left neighbour, and (3) remembers the highest of the two. The result after \(N\) rounds is that all workers know the highest unique value in the network, allowing its original owner to announce itself as leader.  
The case study has been verified with VerCors using the presented approach. All workers communicate via two standard non-blocking operations for message passing: mp_send(_r,msg_) for sending a message _msg_ to the worker with rank \(r\), and \(msg:=\texttt{mp\_recv}(r)\) for receiving a message from worker \(r\). (The identifiers of workers are typically called _ranks_ in message passing terminology. Ranks are simply natural numbers.) The election protocol is implemented on top of this message passing system.  
The main challenge of this case study is to define a message passing system on the process algebra level that matches this implementation. To design such a system we follow the ideas of [46]; by defining two actions, \(\mathsf{send}(r,msg)\) and \(\mathsf{recv}(r,msg)\), that abstractly describe the behaviour of the concrete implementations in mp_send and mp_recv, respectively. Process algebraic summation \(\Sigma_{x}\,\widetilde{P}\) is used to quantify over the possible messages that mp_recv might receive.  
The following two rules illustrate how the abstract send and recv actions are connected to the mp_send and mp_recv procedures in the program, respectively. The latter rule uses a summation (shorthand) of the form \(\Sigma_{x\in Msg}\,\widetilde{P}\) that can be considered equivalent to the process \(\Sigma_{x}\,(x\in Msg:\widetilde{P})\).  
\[\{\mathsf{send}(r,msg)\cdot\widetilde{P}\}\,\texttt{mp\_send}(r,msg )\,\{\widetilde{P}\}\] \[\{\Sigma_{x\in Msg}\mathsf{recv}(r,x)\cdot\widetilde{P}\}\,msg: =\texttt{mp\_recv}(r)\,\{\widetilde{P}[x/msg]\}\]  
Finally, we construct a process-algebraic model of the election protocol using send and recv, and verify that the implementation adheres to this model. This model has been analysed with mCRL2 for various inputs (since mCRL2 is essentially finite-state) to establish the global property of announcing the correct leader. The deductive proof of the program can then rely on this property.