[Termtools] testing starexec for termination

[Carsten Fuhs]

Dear Johannes,

thank you very much for running the tests on starexec! There is one
aspect that is troubling me. On

https://wiki.uiowa.edu/display/stardev/User+Guide#UserGuide-Solvers

the section on "Special Variables" says:

| $STAREXEC_MAX_MEM
|	
| The maximum amount of memory your job pair can consume before being
| terminated. This is not user configurable and has a current limit of
| 768,000KB (750MB).

Only 750 MB RAM is a certain setback after half a decade of running
TermComp on a machine with 65,536 MB. This would also discourage the
recent trend towards tool configurations that keep the 16 cores of the
competition machine occupied (and thus also tend to use more RAM).

Is there a way to convince the starexec administrators to raise the
memory limit to a higher level (several GB)?

Best regards,

  Carsten

On 21.02.2014 15:47, Johannes Waldmann wrote:
> Dear all,
> 
> I could use one or two (TRS/SRS) termination/complexity
> provers/certifiers for testing on starexec.
> 
> The subject of the tests is not the termination prover,
> but the platform: how to run a competition there, how
> to collect and present results data. I will have a student
> working on this. For that, I want to generate some test data.
> 
> For now I am using some version of Matchbox
> (written in Haskell, compiled, dynamically linked executable)
> and it'd be good to have some that use other technology (Java, ocaml).
> Of course it can be some old version,
> with a very "stupid" configuration etc.
> 
> For specification of the platform, see
> https://wiki.uiowa.edu/display/stardev/User+Guide#UserGuide-Solvers
> Here is the matchbox package:
> http://www.imn.htwk-leipzig.de/~waldmann/termination/
> I noticed that starexec machines have rather old libc
> (so, Centos and not Fedora)
> 
> I am not sure how Aaron is handling accounts on starexec,
> I guess you'd have to ask him if you prefer to do your own testing.
> But, as I said, for now I want to test the platform
> (and our programmatic access to it), not the solvers.
> 
> Thanks - Johannes.
> 
> 
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
> 

-- 
Carsten Fuhs                       mailto:c.fuhs at cs.ucl.ac.uk
Department of Computer Science     http://www.cs.ucl.ac.uk/staff/C.Fuhs/
University College London          phone: +44 20 7679 0386
Programming Principles, Logic and Verification