[Termtools] timing

[Claude Marche]

About timing:

Of course only the CPU time is a right measure, but I also use
"timeout" to kill too long-running process. There is 20% extra time to
handle possible gaps, that is for the 60 second round, process are
killed after 72 seconds. 

But to measure the running time afterwards, I'm requesting the cpu
time using the Unix times() function, and the tms_cutime field of the
result. It worked well with previous competitions, but this year I
think I hit the "bug" mentioned in the manual : 

     " Times for terminated children (and their descendants) is added in at  the  moment  wait(2)  or  waitpid(2)
       returns  their  process  ID.  In particular, times of grandchildren that the children did not wait for are
       never seen."

So if some tool is starting another process, but do not kill this second
process properly, my engine do not see the time spent in the second
process. I do not know how to fix this problem...

As far as I can see, this affects Jambox and Matchbox times (time
spent by the SAT solver not taken) and MuTerm (which calls the CiME
constraint solver)

There is a small chance that this affects the YES/NO score: if some
tool finds an answer in a time between 60 and 72 seconds, but my
engine reports less than 60 seconds of CPU time, the answer is
accepted whereas it should be marked as "timeout". If you see any
occurrence of this case, please tell me.

I'm sorry about all these problems happening this year, entirely due
to the lack of time I had. 

I don't think we should be too strict about the "rules" of the
competition. Being the "winner" is not that important. What is
important is to have a clear idea of respective power of existing
tools. It is also important to motivate and support research on
termination techniques, to emphasize interesting problems, open new
challenges. 

With respect to this, I think this year's competition is very
successful: it demonstrates the practical power of the matrix
interpretation technique ; I would say that the current Jambox version has
demonstrated to be a tool of choice for anyone interested in using
termination tools. Personally, I would say that in the TRS category,
for standard rewriting, AProVE and Jambox are winners ex-aequo.
That is, if anyone asks me "I need to use a tool for helping me
proving termination of some TRSs, what do ypu recommend ?" I would
answer try both AProVe and Jambox !

For the SRS category, I would say that Jambox is the clear
winner. Especially, I did not expect that any tool could beat
TORPA... 

For the future, the challenge of producing verifiable proofs is to me
the most important. I asked some days ago if we could identify a
"unsolved problem of the year" but nobody answered. I suggested
Waldmann/jw1 : b b b -> a a a , a a a -> b a b. Any other suggestion ?

- 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    |
_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools