Communications - December 2012

backward traversal, differing only in the sharing of objects between the two halves of the decomposition. The node sharing in decomposition 5 is advantageous for all benchmarks since it requires fewer memory allocations and allows more efficient implementations of insertion and removal; in particular because the lists are intrusive the compiler can find node w using either path and remove it from both paths without requiring any additional lookups.

6. 2. synthesis in existing systems

To demonstrate the practicality of our approach, we took three existing open-source systems—thttpd, Ipcap, and ZTopo—and replaced core data structures with relations synthesized by RelC.

The thttpd Web server is a small and efficient Web server implemented in C. We reimplemented the module of thttpd that caches the results of the mmap() system call. When thttpd receives a request for a file, it checks the cache to see whether the same file has previously been mapped into memory. If a cache entry exists, it reuses the existing mapping; otherwise it creates a new mapping. If the cache is full, then the code traverses through the mappings removing those older than a certain threshold.

The IpCap daemon is a TCP/IP network flow accounting system implemented in C. IpCap runs on a network gateway, and counts the number of bytes incoming and outgoing from hosts on the local network, producing a list of network flows for accounting purposes. For each network packet, the daemon looks up the flow in a table, and either creates a new entry or increments the byte counts for an existing entry. The daemon periodically iterates over the collection of flows and outputs the accumulated flow statistics to a log file; flows that have been written to disk are removed from memory. We replaced the core packet statistics data structures with relations implemented using RelC.

ZTopo is a topographic map viewer implemented in C++. A map consists of millions of small image tiles, retrieved using HTTP over the internet and reassembled into a seamless image. To minimize network traffic, the viewer maintains memory and disk caches of recently viewed map tiles. When retrieving a tile, ZTopo first attempts to locate it in memory, then on disk, and as a last resort over the network. The tile cache was originally implemented as a hash table, together with a series of linked lists of tiles for each state to enable cache eviction. We replaced the tile cache data structure with a relation implemented using RelC.

Table 1 shows non-comment lines of code for each test
case. In each case the synthesized code is comparable to
orshorterthantheoriginalcodeinsize.Bo th the thttpd
and ipcap benchmarks originally used open-coded C data
structures, accounting for a large fraction of the decrease
in line count. ZTopo originally used C++ STL and Boost data
structures, so the synthesized abstraction does not greatly
alter the line count. The ZTopo benchmark originally con-
tained a series of fairly subtle dynamic assertions that veri-
fied that the two different representations of a tile’s state
were in agreement; in the synthesized version the compiler
automatically guarantees these invariants, so the assertions
were removed.

table 1. non-comment lines of code for existing system experiments. for each system, we report the size of entire original system and just the source module we altered, together with the size of the altered source module and the mapping file when using synthesis.

system thttpd ipcap Ztopo

original total module

7050 402 2138 899 5113 1083

synthesis
Decomposition module
42 239
55 794
39 1048

figure 6. elapsed time for ipcap to log 3 × 105 random packets for 26 decompositions up to size 4 generated by the auto-tuner, ranked by elapsed time. the 58 decompositions not shown did not complete within 30 s.