Star Exec - Revision history

J.waldmann: /* Starexec for Termcomp in 2014 */

2014-05-13T19:34:09Z

Starexec for Termcomp in 2014

@@ Line 10: / Line 10: @@
 == Starexec for Termcomp in 2014 ==
-information for participants (submitting and running solvers)
+information for participants (submitting and running solvers) - moved to [[Termination_Competition_2014]]
 == Running the Competition (Entries are from 2012, don't edit) ==

J.waldmann: /* Starexec for Termcomp in 2014 */

2014-05-13T19:23:32Z

Starexec for Termcomp in 2014

← Older revision		Revision as of 19:23, 13 May 2014
Line 16:		Line 16:
	* 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.
	* java is available on starexec nodes (jdk 1.6.0_41)		* hardware on starexec: see [https://www.starexec.org/starexec/public/machine-specs.txt]
			* 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]

	information on the web GUI (under construction) for presenting results [[Star_Exec_Presenter]]		information on the web GUI (under construction) for presenting results [[Star_Exec_Presenter]]

J.waldmann: /* Starexec for Termcomp in 2014 */

2014-02-25T19:31:51Z

Starexec for Termcomp in 2014

← Older revision		Revision as of 19:31, 25 February 2014
Line 9:		Line 9:

	== Starexec for Termcomp in 2014 ==		== Starexec for Termcomp in 2014 ==

			information for participants (submitting and running solvers)

	* submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]		* submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]
Line 15:		Line 17:
	* 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.
	* java is available on starexec nodes (jdk 1.6.0_41)		* java is available on starexec nodes (jdk 1.6.0_41)

			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]])		Separate page with impressions from using the demo version of Star Exec, in 2012: [[Star_Exec_Test]]

	== Running the Competition (Entries are from 2012, don't edit) ==		== Running the Competition (Entries are from 2012, don't edit) ==

J.waldmann: /* Starexec for Termcomp in 2014 */

2014-02-25T17:36:43Z

Starexec for Termcomp in 2014

← Older revision		Revision as of 17:36, 25 February 2014
Line 14:		Line 14:
	* 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.
			* java is available on starexec nodes (jdk 1.6.0_41)

J.waldmann: /* Starexec for Termcomp in 2014 */

2014-02-21T19:02:16Z

Starexec for Termcomp in 2014

← Older revision		Revision as of 19:02, 21 February 2014
Line 12:		Line 12:
	* submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]		* 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: this registration is for testing, and not for actual competition. There may be service interruptions (e.g., sudden changes in benchmark arrangement).		* how to register on starexec [http://lists.lri.fr/pipermail/termtools/2014-February/000943.html] 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? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html]		* 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.

J.waldmann: /* Starexec for Termcomp in 2014 */

2014-02-21T18:34:40Z

Starexec for Termcomp in 2014

← Older revision		Revision as of 18:34, 21 February 2014
Line 13:		Line 13:
	* how to register on starexec [http://lists.lri.fr/pipermail/termtools/2014-February/000943.html] NOTE: this registration is for testing, and not for actual competition. There may be service interruptions (e.g., sudden changes in benchmark arrangement).		* how to register on starexec [http://lists.lri.fr/pipermail/termtools/2014-February/000943.html] 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? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html]		* STAREXEC_MAX_MEM only 750 MB? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html]
			* 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.

J.waldmann at 18:27, 21 February 2014

2014-02-21T18:27:16Z

← Older revision		Revision as of 18:27, 21 February 2014
Line 1:		Line 1:
	[http://www.starexec.org/ StarExec] is a cross-community solver execution and benchmark library service under joint development 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~~. StarExec should be available for public use in the fall of 2012~~.		[http://www.starexec.org/ StarExec] is 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.

	The termination community intends to use this platform for running the competition in 2014		The termination community intends to use this platform for running the competition in 2014

J.waldmann: /* Starexec for Termcomp in 2014 */

2014-02-21T18:24:21Z

Starexec for Termcomp in 2014

← Older revision		Revision as of 18:24, 21 February 2014
Line 11:		Line 11:

	* submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]		* submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]
	* how to register~~: go to~~ [~~https~~://~~www~~.~~starexec~~.~~org~~/~~starexec~~/~~public~~/~~registration~~.~~jsp~~] ~~This gets forwarded to the "community leader" (currently, J. Waldmann) for approval. I (J.W.) will aprove all previous termcomp participants, and forward new entries to the Termcomp SC.~~ NOTE: this registration is for testing, and not for actual competition. There may be service interruptions (e.g., sudden changes in benchmark arrangement).		* how to register on starexec [http://lists.lri.fr/pipermail/termtools/2014-February/000943.html] 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? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html]		* STAREXEC_MAX_MEM only 750 MB? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html]

J.waldmann: /* Starexec for Termcomp in 2014 */

2014-02-21T18:09:49Z

Starexec for Termcomp in 2014

← Older revision		Revision as of 18:09, 21 February 2014
Line 11:		Line 11:

	* submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]		* submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]
	* how to register: go to [https://www.starexec.org/starexec/public/registration.jsp] This gets forwarded to the "community leader" (currently, J. Waldmann) for approval. I (J.W.) will aprove all previous termcomp participants, and forward new entries to the Termcomp SC.		* how to register: go to [https://www.starexec.org/starexec/public/registration.jsp] This gets forwarded to the "community leader" (currently, J. Waldmann) for approval. I (J.W.) will aprove all previous termcomp participants, and forward new entries to the Termcomp SC. 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? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html]		* STAREXEC_MAX_MEM only 750 MB? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html]

J.waldmann: /* Starexec for Termcomp in 2014 */

2014-02-21T18:06:26Z

Starexec for Termcomp in 2014

← Older revision		Revision as of 18:06, 21 February 2014
Line 10:		Line 10:
	== Starexec for Termcomp in 2014 ==		== Starexec for Termcomp in 2014 ==

	* submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]		* submit solvers for testing the platform [http://lists.lri.fr/pipermail/termtools/2014-February/000940.html]
			* how to register: go to [https://www.starexec.org/starexec/public/registration.jsp] This gets forwarded to the "community leader" (currently, J. Waldmann) for approval. I (J.W.) will aprove all previous termcomp participants, and forward new entries to the Termcomp SC.
	* STAREXEC_MAX_MEM only 750 MB? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html]		* STAREXEC_MAX_MEM only 750 MB? [http://lists.lri.fr/pipermail/termtools/2014-February/000941.html]

Line 16:		Line 17:

	(Separate page with impressions from using the demo version of Star Exec, in 2012: [[Star_Exec_Test]])		(Separate page with impressions from using the demo version of Star Exec, in 2012: [[Star_Exec_Test]])


	== Running the Competition (Entries are from 2012, don't edit) ==		== Running the Competition (Entries are from 2012, don't edit) ==