Difference between revisions of "Termination Competition 2014"
J.waldmann (talk | contribs) |
J.waldmann (talk | contribs) |
||
| Line 25: | Line 25: | ||
* STAREXEC_MAX_MEM only 750 MB? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html] (UPDATE: this was out of date, the limit is actually 64 GB) | * STAREXEC_MAX_MEM only 750 MB? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html] (UPDATE: this was out of date, the limit is actually 64 GB) | ||
* Beware if your solver writes to stderr. The "postprocessor" (that expects YES|NO in the first line, for termination) gets to see stdout and stderr merged. If you have trace/log output, you can only show it after the actual answer. | * Beware if your solver writes to stderr. The "postprocessor" (that expects YES|NO in the first line, for termination) gets to see stdout and stderr merged. If you have trace/log output, you can only show it after the actual answer. | ||
| − | * hardware on starexec: see [https://www.starexec.org/starexec/public/machine-specs.txt] | + | * hardware on starexec: see [https://www.starexec.org/starexec/public/machine-specs.txt] Solvers are run on nodes with 4 cores each. |
* software on starexec: RHEL 6.3 (so [http://mirror.nsc.liu.se/centos-store/6.3/isos/x86_64/ Centos 6.3] should be a close match). Package selection, see [http://starexec.forumotion.com/t23-problem-with-dynamic-linking#47] | * software on starexec: RHEL 6.3 (so [http://mirror.nsc.liu.se/centos-store/6.3/isos/x86_64/ Centos 6.3] should be a close match). Package selection, see [http://starexec.forumotion.com/t23-problem-with-dynamic-linking#47] | ||
* java is available on starexec nodes (jdk 1.6.0_41) - see [http://starexec.forumotion.com/t27-install-more-recent-jre-on-nodes] | * java is available on starexec nodes (jdk 1.6.0_41) - see [http://starexec.forumotion.com/t27-install-more-recent-jre-on-nodes] | ||
Revision as of 19:48, 13 May 2014
In 2014, the Termination Competition will be part of the FLoC Olympic Games.
Competition Categories
(to be announced)
Dates (tentative)
- call for solvers, certifiers, benchmarks: May 15
- registration of solvers: June 15
- updates of registered solvers, submission new benchmarks: July 1
- competition starts: July 15
- results announced: during FLoC Olympic Games Award Ceremony, Vienna.
Technical Detail
We intend to run the competition on StarExec - a cross-community solver execution and benchmark library service under joint development (since 2012) at the University of Iowa and the University of Miami. Its goal is to facilitate the experimental evaluation of logic solvers and other automated reasoning tools by providing a shared storage and computing infrastructure to store, manage and make available benchmark libraries; execute comparative evaluations; and run solver competitions.
For displaying the results of the termination competition, we are building a separate web service.
Here is some information for participants:
- submit solvers for testing the platform [1]
- how to register on starexec [2] NOTE: this registration is for testing, and not for actual competition. There may be service interruptions (e.g., sudden changes in benchmark arrangement).
- STAREXEC_MAX_MEM only 750 MB? [3] (UPDATE: this was out of date, the limit is actually 64 GB)
- Beware if your solver writes to stderr. The "postprocessor" (that expects YES|NO in the first line, for termination) gets to see stdout and stderr merged. If you have trace/log output, you can only show it after the actual answer.
- hardware on starexec: see [4] Solvers are run on nodes with 4 cores each.
- software on starexec: RHEL 6.3 (so Centos 6.3 should be a close match). Package selection, see [5]
- java is available on starexec nodes (jdk 1.6.0_41) - see [6]
information on the web GUI (under construction) for presenting results Star_Exec_Presenter
Separate page with impressions from using the demo version of Star Exec, in 2012: Star_Exec_Test
