# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 5 Case Study
### Protocol Implementation  
Figure 9 presents the annotated implementation of the election protocol. (It should be noted here that the presentation is slightly different from the version that is verified with VerCors, to better connect to the theory discussed in the earlier sections to the case study. This is because VerCors uses Implicit Dynamic Frames [47] as its underlying logical framework, which is equivalent to separation logic [48] but handles ownership slightly differently. The details of this are deferred to [8; 49].) The elect method contains the code that is executed by every worker. The contract of elect(_rank_, \(v_{0}\), \(v\)) states that the method body adheres to the behavioural specification Elect(_rank_, \(v_{0}\), \(v\), \(N\)_) of the election protocol. Each worker performing elect enters a for-loop that iterates \(N\) times, whose loop invariant states that, at iteration \(i\), the remaining program behaves as prescribed by the process Elect(_rank_, \(v_{0}\), \(v\), \(i-1\)_). The invocations to mp_send and mp_recv on lines 32 and 36 are annotated with with clauses that resolve the assignments required by the given clauses in the contracts of mp_send and mp_recv. The given\(\overline{\eta}\) annotation expresses that the parameter list \(\overline{\eta}\) are extra ghost arguments for the sake of specification. Stated differently, \(\overline{\eta}\) is a sequence of logical variables which are universally quantified at the (outer) level of the method contract (the types of these are left implicit for ease of presentation). After \(N\) rounds all workers with \(v=v_{0}\) announce themselves as leader. However, since the initial values are chosen to be unique there can only be one such worker. Finally, we can verify that at the post-state of elect the abstract model has been fully executed and thus reduced to \(\varepsilon\) in the logic. The mp_send(_rank_, \(msg\)_) method implements the operation of enqueuing \(msg\) onto the message queue of worker _rank_. Its implementation has been omitted for brevity. The contract of mp_send expresses that the enqueuing operation is abstracted as a send(_rank_, \(msg\)_) action that is prescribed by an abstract model identified by \(X\). The mp_recv(\(X,\textit{rank}\)) method implements the operation of dequeuing and returns the first message of the message queue of worker _rank_. The receive is prescribed as an abstract recv action, where the received message is ranged over by the summation on line 17. Figure 10 presents bootstrapping code for the implementation of message passing. The main procedure initialises the communication channels whereas parelect spawns all workers. main(\(vs\)) additionally initialises and finalises the abstraction ParElect(\(vs\)) on the specification level (on lines 76 and 83, resp.) whose analysis allows establishing main's postconditions. The procedure parelect(\(vs\)) implements the abstract model ParElect(\(vs\)) by spawning \(N\) workers that all execute the elect program. The contract associated to the parallel block (lines 55-59) is called an _iteration contract_ and assigns pre- and postconditions to every parallel instance. For more details on iteration contracts we refer to [50]. Most importantly, the iteration contract of each parallel worker states (on line 58) that it behaves as specified by Elect. Thus, we deductively verify in a _thread-modular way_ that the program implements its behavioural specification. Observe that all the required ownership for the global fields and the Proc\({}_{1}\) predicate is split and distributed among the individual workers via the iteration contract and the with clause on lines 62-64. Finally, the main correctness property is conveyed from the process level to the program level by the query \(X\) annotation on line 82, which \"queries\" for ParElect's postconditions.