# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 5 Case Study
### Behavioural Specification  
The main goal is proving that the implementation determines the correct leader upon termination. To prove this we first define a _behavioural specification_ of the election protocol that hides all irrelevant implementation details, and prove the correctness property on this specification. Process algebra provides a proper abstraction language that suits our needs well, as the behaviour of leader election can concisely be specified in terms of sequences of sends and receives. Figure 8 presents the process algebraic specification. In particular, ParElect specifies the _global_ behaviour of the program whereas Elect specifies its _thread-local_ behaviour. The ParElect process encodes the parallel composition of all eligible participants. ParElect takes a sequence _vs_ of initial values as argument, whose length equals the total number of workers by its precondition. ParElect's postcondition (i.e., trailing assertion) states that _lead_ must be a valid rank after termination and that _vs[lead]_ be the highest initial worker value. It follows that worker _lead_ is the correctly chosen leader. 1 seq(seq(Msg))cham;//communicationchannelsbetweenworkers
2 intlead;//therankoftheworkerthatisannouncedasleaderaftertermination
3
4/*Actionforresedingsings. */
5 guard0\(\leq\)rank\(<\)|chan|;
6 effect\(\textit{chan}[\textit{rank}]=\)\(\backslash\)old(\(\textit{chan}[\textit{rank}]\))+{msg};
7 effect\(\forall\prime^{\prime}\colon\texttt{int. }\left(0\leq r^{\prime}<|\textit{chan}|\wedge r^{\prime}\
eq\textit{rank}\right)\implies\textit{chan}[r^{\prime}]=\)\(\backslash\)old(\(\textit{chan}[r^{\prime}]\));
8 action\(\textsf{send}(\textit{int}\textit{rank}\),Msgmsg);
9
10/*Actionforreceingmessages. */
11 guard0\(\leq\)rank\(<\)|chan|;
12 effect\(\{msg\}+\textit{chan}[\textit{rank}]=\)\(\backslash\)old(\(\textit{chan}[\textit{rank}]\));
13 effect\(\forall r^{\prime}\colon\texttt{int. }\left(0\leq r^{\prime}<|\textit{chan}|\wedge r^{\prime}\
eq\textit{ rank}\right)\implies\textit{chan}[r^{\prime}]=\)\(\backslash\)old(\(\textit{chan}[r^{\prime}]\));
14 action\(\textsf{recv}(\textit{int}\textit{rank}\),Msgmsg);
15
16/*Actionforannouncingleader. */
17 guard0\(\leq\)rank\(<\)|chan|;
18 effect\(\textit{lead}=\)rank;
19 action\(\textsf{announce}(\)int\(\textit{rank})\);
20
21/*Thelocal behaviouralspecificationforeveryworker. */
22 requires0\(\leq\)n\(\leq\)|chan|\(\wedge\)0\(\leq\)rank\(<\)|chan|;
23 process\(\textsf{Elect}(\)int\(\textit{rank}\),Msg\(v_{0}\),Msg\(v\), int\(n)):=
24 if0\(<\)nthen\(\textsf{send}((\textit{rank}+1)\)\(\%\)|chan|,\(v)\). 25\(\Sigma_{\
u^{\prime}\in\textit{Msg}}\textsf{recv}(\textit{rank}\), \(v^{\prime})\cdot\textsf{Elect}(\textit{rank}\), \(v_{0}\),max(\(v\),\(v^{\prime}\)), \(n-1)\)
26 else(if\(v=v_{0}\)then\(\textsf{announce}(\textit{rank})\)else\(\varepsilon\));
27
28/*Globalbehaviourspecificationoftheelectelectprotocol. */
29 requires\(|\)vs\(|\)chan|;
30 requires\(\forall_{i}\colon\texttt{int. }\left(0\leq i<|\)vs\(|\)\(\wedge\)0\(\leq\)\(j<|\)vs\(|\)\(\wedge\)vs\(|\)\(i\)\(=\)vs\(|\)\(j\right)\implies i=j\);
31 ensures\(|\)vs\(|\)chan|\(\wedge\)0\(\leq\)lead\(|\)vs|;
32 ensures\(\forall i\colon\left(0\leq i<|\)vs\(|\right)\implies\)vs\(|\)\(i\)\(\leq\)vs\(|\)lead\(|\);
33 process\(\textsf{ParElect}(\)asg\(\rangle\)vs\():=
34 Elect(0, \(\textit{vs}[0]\), \(\textit{vs}[0]\), \(|\)vs\(|\))\(\cdots\)\(\parallel\)Elect\((|\)vs\(|\)\(-1\), \(\textit{vs}[|\)vs\(|\)\(-1]\), \(\textit{vs}[|\)\(\textit{vs}[|\)\(-1]\), \(|\)vs\(|\));  
**Figure 8. The behaviouralprocess-algebraicspecificationoftheleaderelectionprotocol. Processes of theformif\(\textit{lb}\)then\(\textit{P}\)else\(Q\)areabstandforward\(\textit{lb}:\textit{P}+\
eg b:Q\).Moreover,allensuresclausesofParElectaretranslatedintotrailingassertions,asdescribedearlieratthebeginningofSection3.4.2.