search

coq-community / chapar

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
MIT License
32 stars 7 forks source link

Packet drop prevents clients from reading updates #4

Open pfons opened 8 years ago

pfons commented 8 years ago

The implementation of Chapar is unable to handle packet drops because it currently assumes that the network layer is reliable. Unfortunately the UDP transport is not reliable and packet loss can occur.

This problem is particularly serious because a single packet dropped can prevent clients from reading all the subsequent updates made by clients on the source server.

For example, if the following execution occurs: 

    Req 1: Client A: PUT key, “1”
<Req 1 is dropped>
    Req 2: Client A: PUT key2, “Request”

Because the message corresponding to request 1 was dropped and did not arrive at the other servers, client B will never be able to see the updated values of key2:

    Req 3: Client B: GET key2 -> “Request”   // This result is never returned
MohsenLesani commented 8 years ago

Causal consistency has to prevent other nodes from viewing the new messages if a previous message is not seen or lost. However, we can always add additional mechanisms that periodically check with other nodes whether they have received certain messages or not.