[Termination tools] Re: WST competition: executable

[Claude Marche]

>>>>> "Peter" == Peter Schneider-Kamp <psk at informatik.rwth-aachen.de> writes:

    Peter> Hi Claude,
    Peter> we are starting to prepare for the WST competition. The rules
    Peter> state that for the executable "The preferred form is directly
    Peter> a stand-alone executable for i386/Linux".

    Peter> As you might know, our system is written in Java. Previous
    Peter> attempts (and one more this afternoon) compiling our sources
    Peter> to native code have all failed :-( There is always an issue
    Peter> with the libraries as the compiler folk seem not to be up to
    Peter> date with the Java SDKs.

    Peter> Now, I guess it would be okay to deliever a script called
    Peter> runme which executes java (which is hopefully installed in
    Peter> version 1.4.2 or something similar). The problem is that

Yes, runme may just execute some java -jar ...

    Peter> startup of the Java virtual machine as well as just-in-time
    Peter> compilation of the required classes consume a non-trivial
    Peter> part of the (limited) total runtime.

    Peter> On one hand, we understand that it is important to measure
    Peter> the time the program takes instead of relying on information
    Peter> given by the program. On the other hand, it is pretty unfair
    Peter> to measure the times including startup of the runtime
    Peter> environment and compilation of the termination prover for
    Peter> each example.

But how much time ? If less than a second, it would be neglectable. I
plan to give at least 10 seconds.

If just tested launching the Aprove version I have, it takes a few
seconds but it needs to launch the GUI, may be a text version would
start faster.

    Peter> There seem to be 3 possible ways out - all of which
    Peter> have their own advantages and disadvantages:

    Peter> 1) Measure and subtract startup overhead (also for other
    Peter>     tools like Termptation).
    Peter>     Advantage: Fair.
    Peter>     Disadvantage: Not very precise.

    Peter> 2) Let a "server"-version of AProVE run in the background
    Peter>     which gets filename and maximal runtime from a
    Peter>     small runme-stub. This would require that the process
    Peter>     of runme is not killed with a SIGKILL but with a
    Peter>     SIGTERM in order to be able to notify the server of
    Peter>     the timeout.
    Peter>     Advantage: More fair and precise.
    Peter>     Disadvantage: Requires considerable effort in
    Peter>                   implementation. Server has to be
    Peter>                   started and stopped.

    Peter> 3) Give a whole directory or list of files instead of
    Peter>     one file at a time.
    Peter>     Advantage: Easy to implement.
    Peter>     Disadvantage: Only total runtime can be checked
    Peter>                   precisely.

    Peter> What is your opinion on the above suggestions?

For the moment when just reading this: this seems much much
overcomplicated to me ! 

Please remember something: the only thing that counts is the answer,
the time to give it is not important, unless the time limit is reach.

Moreover, I plan to make the competition viewable in direct live on
the web, so if you see some example where you suspect that Aprove
timeouts but you think it would have succeeded with a few seconds
more, please ask: I would agree to increase the time limit for this
particular example.

In fact, I plan to have a default time limit, and the possibility to
increase it for "interesting problems", where tools appear to need
much time.

Do you understand my point of view ?

So don't spend time in implement feature like "server" version. Just
write a text-based non-interactive version that I can run with java
-jar ... 

    Peter> Of course, if you have any other suggestions, I will be glad
    Peter> to discuss them with you, too.

    Peter> Greetings from sunny Aachen,

Greetings from not so sunny Paris !

- Claude

-- 
| Claude Marché           | mailto:Claude.Marche at lri.fr |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  |
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |