Distributed key-value stores can offer different consistency guarantees, such as strong consistency, causal consistency, and eventual consistency, which leads to differences in performance and fault tolerance. Chapar is a causally consistent key-value store implementation verified in the Coq proof assistant and maintained as an open-source project on GitHub. The code is extracted from Coq to the OCaml programming language and has been experimentally executed and performance tested as part of the work described in a 2016 conference paper. However, there are several serious practical problems in the verified code, such as the formal specification assuming the removal of duplicates. At the same time, the implementation uses the UDP protocol which gives no guarantees regarding duplicates. This thesis confirmed the existence and reproducibility of the reported UDP issues. To address these underlying problems, a reliable protocol was integrated into the Chapar framework. This involved restructuring the codebase and extending the framework with the TCP protocol. Additionally, a testing framework was developed to replicate the conditions under which the errors occurred. The findings demonstrated the successful recreation of all reported issues. Furthermore, the results indicated that replacing the unreliable UDP protocol with the reliable TCP protocol resolved the issues while maintaining comparable performance levels.

Nyckel-värde-databaser har konsistensegenskaper vilker ger olika garantier och prestanda på databasen. ”Causal consistency” är ett exempel på en sådan egenskap som garanteerar kausalitet mellan olika händelser. Chapar är en ”causal consistent” nyckel-värde-databas som har verifierats med hjälp av bevisassistenten Coq i tidigare arbete från 2016 och underhålls som ett öppen källkodsprojekt på GitHub. Koden extraheras från Coq till OCaml programmeringsspråket och har experimentellt körts och prestandatestats som en del av den ursprungliga avhandlingen. Även om den nuvarande implementationen av den exekverbara koden kan extraheras till OCaml och kompileras med bibliotekskod, kan nyckel-värde-databasen inte köras på grund av problem i senare versioner av OCaml-biblioteket. Dessutom finns det flera allvarliga praktiska problem i den verifierade koden, såsom att den formella specifikationen förutsätter borttagning av dubbletter, medan OCaml- implementationen inte tar bort dubbletter eftersom den använder UDP- protokollet. Denna avhandling lyckas återskapa de problemen relaterade till UDP och återskapar de ursprungliga UDP-benchmarkstesterna med liknande resultat. Dessutom löses de öppna problemen genom att implementera ett pålitligt protokoll (TCP). TCP prestandatestas också och visas ha liknande prestanda, vilket gör det till ett lämpligt protokoll för framtida implementationer.