There is a bug in the Chapar implementation that allows a client to issue requests that cause corrupted packets to be sent and to be accepted by servers. The problem is triggered when a client attempts to send a request larger than the UDP limit. When this happens, headers and partial request data are kept in internal buffers which can potentially be concatenated with subsequent requests.

This bug has several harmful consequences: 1) large requests are silently ignored; 2) small requests can be discarded because of preceding large requests and 3) servers can accept requests that no client issued.

The following steps, which are tuned for Algorithm 2, are able to reproduce the bug:

a. Construct three strings with size 60000, 65791, and 5711, denoted by str1, str2, and str3.
b. To more easily reproduce the bug it is convenient to modify the "value" type to string, although this is not strictly necessary to reproduce the bug.
c. Issue the following requests:

       Req 1: PUT  k0 “Hello World”
       Req 2: PUT  k1 str1    
       Req 3: PUT  k1 str2
       Req 4: PUT  k1 str3

d. Simulate reordering of the two network packets sent when invoking Req 2 and Req 4

After this sequence of steps the receiver will concatenate the two packets and interpret them as a single request (that does not match any of the PUTs issued). Furthermore, the server will wrongly consider the request to be valid and, consequently, the server will incorrectly update the key-value store.

The root of this problem lies on the use of the function Marshal.to_channel (from the OCaml library) to send messages to other servers (file runtime.ml). Internally, Marshal.to_channel works in the following way:

1. While marshaling the components of message, it makes several calls to the function caml_putblock [1], through the sequence of invocations: to_channel [3] -> caml_output_value [2] -> caml_output_val [2] -> caml_really_putblock [1] -> caml_putblock [1].
2. On each invocation caml_putblock appends the input data to an internal buffer.
3. This buffer is flushed when (1) flush is explicitly called on the channel or (2) inside caml_putblock when new contents cannot be appended to the buffer because it would reach its maximum capacity. Flushing the buffer consists in calling the write system call on the socket file descriptor. The size of the internal buffer is larger than the UDP packet limit
4. When caml_putblock tries to flush the internal buffer (in a case where it is filled beyond the UDP limit) the call to the write system call fails (as expected) and it fails with the error EMSGSIZE. Upon such error, an exception (UnixError) is thrown, which will be handled by an exception handler but crucially two things happen (1) the internal buffer is not cleared (i.e., it retains the prefix of the message) and (2) nobody tries to resend the suffix of the message that was discarded.

In practice, during runtime, the following happens behind the scenes for each of the reproduction steps:

     Req 1 is a dummy request that initializes internal data
     Req 2 sends a correct packet (which subsequently is appended to 
the packet sent by Req 4 by the receiver)
     Req 3 does not send any packet because the message is too long 
and garbage data (headers + key) is left behind in the OCaml library
     Req 4 sends an incorrect packet that concatenates (1) the garbage 
data left behind from Req 3 and (2) the data from Req 4

Note that the sizes of the string buffers are carefully chosen to ensure that the packet headers match. In addition, reordering of the packets is necessary only to ensure that the request delivered to the receiving server has the causal-consistent meta-data that is expected.

Given the above, it is hard to correctly use the to_channel function without explicitly checking before invoking to_channel that the message size fits within the content limit of UDP packets.

References:
[1] https://github.com/ocaml/ocaml/blob/trunk/byterun/io.c
[2] https://github.com/ocaml/ocaml/blob/trunk/byterun/extern.c
[3] https://github.com/ocaml/ocaml/blob/trunk/stdlib/marshal.ml

The algorithm 2 produces results that violate causal consistency when messages are duplicated and reordered by the network. This situation can occur in practice because the UDP protocol, which is used for the server-server communication, does not guarantee in-order delivery nor does it guarantee at-most once delivery.

The following steps are sufficient to reproduce the bug, with Client A, Client B and Client C running on different servers:

    Req 1: Client A: PUT key, “NA”
    Req 2: Client A: PUT key, “Request”

    Req 3: Client B: GET key -> “Request”
    Req 4: Client B: PUT key-effect, “Reply”

   <replay packets sent by Req 1>

    Req 5: Client C: GET key-effect -> “Reply” 
    Req 6: Client C: GET key -> “NA”

The steps above show that client C can see the effect event (“Reply”), produced by Client B, without seeing the cause event (“Request”), produced by Client A.

The client prog_photo_upload [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

OCaml code doesn't compile with at least OCaml 4.07. The code should be ported to use a modern version of Batteries, and the bundled version of Batteries removed.

Hi,

I cloned the project from git and ran make, make install and make stores, which all seemed well.
But I ran the demo experiment with ./batchrundetach and it returned the following error:

Run: 1
Launching ...
Tue Jul 13 10:13:09 MDT 2021
Fatal error: exception Unix.Unix_error(Unix.EINVAL, "out_channel_of_descr", "")
Receiving and saving results ...
scp: /root/Runner/Worker0/Result.txt: No such file or directory
scp: /root/Runner/Worker1/Result.txt: No such file or directory
scp: /root/Runner/Worker2/Result.txt: No such file or directory
scp: /root/Runner/Worker3/Result.txt: No such file or directory
cat: 'Result*': No such file or directory
Results ...
rm: cannot remove 'Result*': No such file or directory
Sleeping for 10 seconds before the next run ...

The following configurations FYI:

Settings.txt
KeyRange=
50
RepeatCount=
2
LauncherNode=
[email protected]
MasterNode=
[email protected]
WorkerNodes=
[email protected]
[email protected]
[email protected]
[email protected]

Packages under opam:

Packages matching: installed
Name Installed Synopsis
base-bigarray base
base-threads base
base-unix base
batteries 3.3.0 A community-maintained standard library extension
conf-findutils 1 Virtual package relying on findutils
conf-gmp 3 Virtual package relying on a GMP lib system installation
coq 8.13.2 Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.12.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.12.0 Official release 4.12.0
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml projects.
ocamlfind 1.9.1 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers

Could anyone give any suggestions on this?

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