Cozy
The Collection Synthesizer
--------------------------------------------------------------------------------
Cozy is a tool that synthesizes collection data structure implementations
from very high-level specifications.
GETTING STARTED
Dependencies:
Python 2.7 - https://www.python.org/
Z3 Python bindings - https://github.com/Z3Prover/z3
To check for the necessary dependencies, you can run:
$ ./check.sh
To get help:
$ python src/main.py --help
To run the tool:
$ python src/main.py [options] [input-file]
The synthesizer may run for a very long time in some cases. To stop it,
press Ctrl+C and the tool will stop and output the best implementation
found so far. Alternatively, you can pass a timeout value to the tool.
EXAMPLES
Sample input files live in the "examples" folder.
Some of the interesting examples are:
graph - a multigraph data structure
simple-sort - a data structure requiring sorting on its results
neq - efficient lookup of elements NOT equal to a value
INPUT FORMAT
If you want to craft your own inputs for Cozy, the input format is very
simple. Each input file consists of:
- some fields with names and types
- optional assumptions about those fields
- a set of query method specifications
- an optional autotuning program
Fields are declared using
fields name1:type1, name2:type2, ...
The types are treated as opaque strings and Cozy will blindly write
them into the generated source code.
Assumptions are declared using
assume expr
Top-level assumptions can only talk about record fields. They state
conditions about individual records---i.e. preconditions for the
generated `add()` method. The resulting data structure does not check
these preconditions at runtime, but the synthesizer may be able to exploit
them to generate faster code. (See examples/myria-profiling-api.)
Query methods are declared using
query query_name (arg1:type1, arg2:type2, ...)
assume expr1
assume expr2
condition-expr
sort field_name
Query assumptions are optional. They state preconditions for the generated
method. The resulting data structure does not check these preconditions at
runtime, but the synthesizer may be able to exploit them to generate faster
code. (See examples/myria-profiling-api.)
The condition-expr states what records should be returned by the query
method.
The sort declaration is optional and, if present, requires that the
resulting data set be sorted by some particular field. (See
examples/simple-sort.)
Autotuning programs are declared using
costmodel file.java
See the inputs in the examples folder for inspiration.
HACKING
Source code lives in src. It is well-organized, but poorly commented.
src/
main.py -- program entry point
synthesis.py -- synthesis algorithm
codegen.py -- code generation
structures/ -- data structure library
...
There are a few scripts useful for developers:
Run pylint: ./lint.sh
Run tests: ./test.sh
Run fuzzer: ./fuzz.sh