[Termtools] About memory examples in C category

[Thomas Ströder]

Dear all,

Am 19.07.2015 um 16:33 schrieb Ton-Chanh Le:
> Dear Yamada,
> 
> Thank you very much for pointing out the rule.
> 
> We asked the question as the rule also mentioned
> that "we could also offer an additional category where 
> memory safety can be assumed" and we did not know
> whether that category is implemented in this competition
> or not.

Currently, there is no additional category where memory safety can be
assumed. If there is enough interest in it, we could build up such a
category for the next competition (we would need to gather suitable
examples and/or check existing ones).

> Regarding to the rule for C programs, we would like to
> clarify some points:
> 
> - The rule says that "neither YES nor NO is a correct result 
> for programs violating memory safety", does this mean
> the expected result in this case is MAYBE?

Yes. Such examples won't yield any points, but can lead to a penalty if
claimed to be proven to (non-)terminate. Together with some people from
SV-COMP, I had a little discussion about this rule. The question is
whether the property "non-termination" means that you can definitely
reach a non-terminating run or whether it is the negation of the
property "termination". Another related question is whether undefined
behavior means that everything counts as definitely reachable behavior.
Both answers to these questions have their pros and cons. Currently, the
interpretation at termCOMP is that "non-termination" means that a
non-terminating run can definitely be reached and undefined behavior
does not give you any guarantee of what can be reached. Hence, only
MAYBE is a correct answer for memory-unsafe examples (but since MAYBE
does not require any proof, this answer gives no points).

I would neither vote for nor against changing this rule, but if the
majority of participants would be in favor of changing the rule such
that violation of memory-safety implies non-termination, I think we
could do this (not sure whether this would already work for the current
competition, but it would definitely be possible for future editions).
However, violation of memory-safety would not include memory leaks as
these do not lead to undefined behavior and, thus, do not influence
termination behavior.

> - Although "allocation of memory always succeeds", how about the
> value of the allocated memory cell? Is it a non-deterministic value?

Yes.

> Thank you very much.
> 
> Best Regards,
> 
> Le Ton Chanh
> Email: chanhle at comp.nus.edu.sg <http://comp.nus.edu.sg>

Best regards,

  Thomas


> On Sun, Jul 19, 2015 at 8:19 PM, Akihisa Yamada
> <akihisa.yamada at uibk.ac.at <mailto:akihisa.yamada at uibk.ac.at>> wrote:
> 
>     Dear Le Ton Chanh,
> 
>     your question seems to be discussed in the competition rule:
>     http://termination-portal.org/wiki/C_Programs
> 
>     Best regards,
>     Akihisa
> 
> 
>     On 2015/07/16 4:36, Ton-Chanh Le wrote:
> 
>         Dear PC members,
> 
>         I would like to ask whether we have the assumption
>         that the pointer examples in the C category is
>         memory safe or we need to prove memory safety
>         prior to termination proofs.
> 
>         Thank you.
> 
>         Best Regards,
> 
>         Le Ton Chanh
>         Email: chanhle at comp.nus.edu.sg <http://comp.nus.edu.sg>
>         <http://comp.nus.edu.sg>
> 
> 
>         _______________________________________________
>         Termtools mailing list
>         Termtools at lists.lri.fr <mailto:Termtools at lists.lri.fr>
>         http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
> 
> 
> 
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
> 

-- 
Thomas Ströder        mailto:stroeder at informatik.rwth-aachen.de
LuFG Informatik 2     http://verify.rwth-aachen.de/stroeder
RWTH Aachen           phone: +49 241 80-21241

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150719/087e3b11/attachment.sig>