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
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
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.
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.
Elapsed time (s)
5 10 15 20
Decompositions, ranked by time