Termination Competition 2014 technical details - Revision history

J.waldmann at 17:43, 3 June 2014

2014-06-03T17:43:46Z

J.waldmann at 15:49, 26 May 2014

2014-05-26T15:49:23Z

Albert: Created page with "We intend to run the competition on [http://www.starexec.org/ StarExec] - a cross-community solver execution and benchmark library service under joint development (since 2012..."

2014-05-26T09:41:17Z

Created page with "We intend to run the competition on [http://www.starexec.org/ StarExec] - a cross-community solver execution and benchmark library service under joint development (since 2012..."

New page

We intend to run the competition on [http://www.starexec.org/ 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 at HTWK Leipzig.

Here is some information for participants:

* submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]
* how to register on starexec [http://lists.lri.fr/pipermail/termtools/2014-February/000943.html] NOTE: there may be service interruptions (e.g., sudden changes in benchmark arrangement).
* 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.
* 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]
* java is available on starexec nodes (jdk 1.6.0_41) - see [http://starexec.forumotion.com/t27-install-more-recent-jre-on-nodes] - see also remark on ulimits and -Xmx [http://starexec.forumotion.com/t34-ulimits-settings-may-hurt-java-programs#69]
* it is helpful to follow other solver communities, e.g., [http://smtcomp.sourceforge.net/2014/ SMT COMP 2014]

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]]

@@ Line 3: / Line 3: @@
 For displaying the results of the termination competition, we are building a separate web service at HTWK Leipzig.
-Here is some information for participants:
+Here is some information for participants: (reverse chronological - newest first)
 * submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]
 * how to register on starexec [http://lists.lri.fr/pipermail/termtools/2014-February/000943.html] NOTE: there may be service interruptions (e.g., sudden changes in benchmark arrangement).
@@ Line 12: / Line 16: @@
 * 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] - see also remark on ulimits and -Xmx [http://starexec.forumotion.com/t34-ulimits-settings-may-hurt-java-programs#69]
 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]]