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

Incorrect assertion in client prog_photo_upload #1

Closed pfons closed 8 years ago

pfons commented 8 years ago

The client _prog_photoupload [1] in Chapar has a bug in its assertion.

The current check simply asserts the condition of the conditional branch (if-condition). Therefore, the assertion always evaluates to true, which defeats its purpose (i.e., detecting causal consistency violations). In addition, there is no other assertion that correctly does the causal consistency check for this client application.

This bug can be fixed by asserting that the variable photo, instead of post, is non-empty:

--- Clients.v   2016-04-21 20:29:35.743409593 -0700
+++ Clients-fixed.v     2016-04-21 20:30:07.423566686 -0700
@@ -56,7 +56,7 @@
           post <- get (Post);;
           if (string_dec post "Uploaded") then
              photo <- get (Photo);;
-             if string_dec post "" then
+             if string_dec photo "" then
                fault
              else
                skip

[1] https://github.com/mit-plv/chapar/blob/master/coq/Examples/Clients.v