Cloud9 can test distributed systems by simulating them using a program that forks multiple processes, which communicate through network sockets. In this case study, we test the memcached distributed in-memory object cache by modifying its testing harness to send symbolic packets. We'll use the most recent version of the code available at the moment of writing this tutorial. A similar setup was used to discover a security vulnerability in memcached (which was fixed in the mean time).
memcached requires libevent, so we first have to generate a static LLVM binary that we'll link into the final memcached executable.
You should now have the
Building memcached using the LLVM toolchain is similar to building libevent. However, the original memcached code produces only the server executable. In order to test memcached with symbolic packets, we need to change the program entry point to fork both a server and a client. The modified memcached code (called memcached-llvm) can be found here, together with a change list.
You should now have the
You should see each test case being executed and passed. Note that the execution is linear - each test case is executed one after the other as a single path.
We can now ask Cloud9 to inject symbolic packets into memcached, by running
Now memcached runs along multiple paths, since the execution forks inside the server code for each branch depending on the packet contents. Notice that most of the paths are erroneous -- the packet structure is invalid, so memcached terminates the connection.
We mentioned earlier that the original memcached code produces only the server executable. So what happens if we ran the server directly? Let's assume that we download the original code, and build it using the procedure above. When we run the server using a command like:
we see that the memcached execution ends with an error message like
So why is this happening? It's very unlikely that memcached would hang or deadlock at initialization when we run it for real. However, in the context of symbolic execution, memcached runs in a "closed universe". The symbolic state contains only its process, and as soon as memcached initializes and starts listening for connections, no other thread or process exists to be scheduled. Cloud9 detects this as a "hang", since the system can no longer progress at that point.
Testing Programs >