University of Twente Student Theses


Verification of distributed locks : a case study

Ledelay, Joël (2023) Verification of distributed locks : a case study.

[img] PDF
Abstract:In this thesis, VerCors will be used to verify functional correctness of a lock implementation provided by BetterBe. This implementation is a distributed, reentrant, read-write lock, in which the resource which the lock locks on is a database table row. This implementation has been used in practice and any problems which have previously turned up have been solved. BetterBe is fairly confident that the implementation works as intended, as the implementation has run for an extended amount of time without major defects. In an effort to ensure that no more major defects will appear down the line, BetterBe wishes to employ formal verification to close the gap between the perceived correctness of the system and its actual correctness. Scenarios which are highly dependent on timing, availability of database services or other specific conditions such as system load or connectivity issues may not have been encountered, but that does not give any guarantee that these scenarios never lead to faults in system behaviour. This thesis formally verifies the functional correctness of a simplified version of the implementation, and proves properties such as data race freedom. Annotations are added to the program to specify handling of ownership and functional correctness of the program with regards to its expected behaviour. The annotated code is then analysed by VerCors to verify these properties.
Item Type:Essay (Master)
BetterBe, Enschede, The Netherlands
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page