RulesPlease accept that the overall spirit of this competition is friendly, honest and well-spirited. The goal is to foster research and to motivate the implementation and optimization of new synthesis tools. However as it is still a competition, the following rules shall apply:
CategoriesThere will be 4 categories at SyntComp 2014:
- Synthesis - Sequential
- Synthesis - Parallel
- Realizability - Sequential
- Realizability - Parallel
- Not more than 3 submission per author in a category. Two tools are different as soon as their sources differ or as soon as the command line arguments used or the compilation options used to compile it are different.
- The source code of submitted tools must be made available (licensed for research purposes).
- Submitted tools must be accompanied by a 2 page description (IEEE format). This should include a list of all authors and their present institutional affiliations.
- Organizers can compete but have to make the MD5 of their code available before the opening of the submission system.
- All synthesis tools must conform to the Extended AIGER Format for Synthesis
- Tools must not include pre calculated results to any of the benchmarks and there must not be any intentional sabotage of the evaluation system.
- Tools write the resulting circuit to stdout. If the tool concludes that the specification is unrealizable, it should write UNREALIZABLE to stdout. For the realizability category, where the tool is not required to synthesize an implementation it should output REALIZABLE if it is realizable.
- There will be no qualification round, but only a testing phase to ensure that all tools are running properly on the evaluation system. The organizers reserve the right to disqualify poorly performing tools.
- A submission can be withdrawn from the competition only before the deadline for the submission of the final versions. After this deadline no further changes or withdrawals are possible.
RankingOur quality criterion (for categories with synthesis) is the size of the synthesized correct circuit as measured by the number of AND gates. As not all tools will solve the same subset of benchmarks, the following procedure is used to determine the ranking: An individual ranking is done for each benchmark, with (1000/b) * (n-m+1)/(n*(n+1)/2) points attributed to each tool, where b is the total number of benchmarks used for this category, n is the number of tools that provided a correct solution to the benchmark and m is the rank of the tool by circuit size. An incorrect solution is punished by disqualification. Tools not providing a solution (for example because they are stopped because they have reached the cpu time or wall time limit) will get 0 points. Example: b=50 benchmarks, 10 tools named "A" ... "J" are competing in the category, the first n=8 provide a correct circuit, I has no result (crashed, time limit reached etc) and J provides a result with syntax errors in this benchmark - therefore the points collected from this benchmark are:
A 4.44 B 3.89 C 3.33 D 2.78 E 2.22 F 1.67 G 1.11 H 0.56 I 0.00 J -20.00
Points from all benchmarks are summed up per tool to get the quality ranking of the SyntComp.
The same procedure is used to determine the speed ranking of SyntComp, with tools ranked for each benchmark by how fast they were.
If a benchmark can only be solved by a single synthesis tool, it will also be awarded a special price.
A subset of all available benchmarks will be selected for the competition. Randomization and the consultation of impartial judges will ensure that organizers have no undue advantage in the competition. The exact benchmark selection scheme is to be determined.
Extended AIGER Format for Synthesis
We think that, in order to have a successful competition at CAV/SYNT
2014, the three most important things are:
i) keeping the format simple,
ii) having sufficiently many competing tools,
iii) supplying the community with a format, benchmark set and framework for testing their tools as early as possible.
These three points led us to choosing the AIGER format — restricted to safety specifications, like in the main category of the HWMCC — both as input and ouput format for the synthesis competition. For the input format, we need to add a partition of inputs into controllable and uncontrollable, but otherwise we can build on a well-known language with a clear semantics and existing tool support. For the output format, choosing AIGER allows us to almost directly check the synthesized artifacts with any model checker that supports the format (in particular, any that competes in the HWMCC). A description of how we plan to use the AIGER format in reactive synthesis can be found here: Format Proposal (v0.1).
What happens to Tool and Benchmark descriptions (after the competition)?
Tool and benchmark descriptions will be published, exact details are tbd.
On what kind of system will my submission be tested?
All synthesis tools will be tested on the HPC Cluster provided by TU Graz, more specifically on the d-cluster, consisting of 120 computing nodes. A node consists of 2 Octo-Core Intel XEON processors (2.0 GHz) and 64 GB RAM. The queueing system in use is Torque - http://www.adaptivecomputing.com/products/open-source/torque/. As usual on a GNU/Linux system, the GNU Compiler Collection (GCC) is installed. The version of GCC available currently is 4.7. Each node has a local 400gb hard drive that should be used for storing any temp files your tools need to create.
During the competition, a complete node will be reserved for each job i.e. one synthesis tool (configuration) running one benchmark. Olivier Roussel's runsolver (http://www.cril.univ-artois.fr/~roussel/runsolver/) is used to run each job, set limits on cpu time, wall time, memory or stack and measure cpu and wall time. As all nodes are identical and no other tasks are run in parallel no other limits than a timeout per benchmark (cpu time for sequential tools, wall time for the parallel tracks) will be set. Each synthesis tool can therefore expect to use about 60GB of RAM.
Please contact us if you have any concerns about the fairness of this setup or if anything about it is for whatever reason unacceptable for you and/or your synthesis tool.
The list of available software will be updated continuously as requests/questions come in. The competition will be organized with the EDACC platform developed for the SAT Challenges.
What if my tool does not compile on the competition servers?
The SyntComp team will work together with tool developers to ensure that all tools run as intended on our servers. If you have reason to doubt that your tool will compile on our servers, consider submitting a first version as soon as possible, such that there is enough time to work on any compilation issues before the competition.
How are synthesized circuits checked for correctness?
AIGER files produced by synthesis tools are checked automatically with a model checker. We use a timeout for model checking (and results that cannot be verified are considered incorrect), but checking should be much easier than synthesizing and we do not expect many cases where a correct solution cannot be verified.
Can I withdraw my tool description if I “lose” the competition?
Tools can only be withdrawn before the actual competition. We will however allow every participating team to react to the competition results by inspecting the behavior of their tools on the benchmarks used in the competition. If bad performance in the competition is due to bugs that can be found and possibly fixed before presentation of the results or publication of the descriptions, the organizers will work together with the developers to shed light on these issues.
What will be the timeout for each synthesis task?
5000 seconds (wall-clock time) per task.