www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Is D's TimSort correct?

reply =?UTF-8?B?QWxpIMOHZWhyZWxp?= <acehreli yahoo.com> writes:
Some implementation out there are buggy:

 
http://www.reddit.com/r/programming/comments/2wze7z/proving_that_androids_javas_and_pythons_sorting/

Ali
Feb 24 2015
next sibling parent reply ketmar <ketmar ketmar.no-ip.org> writes:
On Tue, 24 Feb 2015 10:47:19 -0800, Ali =C3=87ehreli wrote:


 Some implementation out there are buggy:
=20
=20
 http://www.reddit.com/r/programming/comments/2wze7z/


proving_that_androids_javas_and_pythons_sorting/

=20
 Ali


their KeY system is very interesting. i'm very curious what minimal=20
changes can be made for D to integrate something like it into the source=20
code. i.e. turn all that pseudo-comment things that KeY is using into=20
valid D code. compiler can check code semantics, so all contracts are at=20
least syntactically correct. and then KeY-like tool can try to prove the=20
correctness.

we already has `in` and `out`, and `invariant` for structs/classes. i=20
believe that `invariant` can be reused for other invariants (like loop=20
invariant)...

and it's interesting what complications templates can bring. testing=20
templates is relatively hard now, 'cause programmer must ensure that=20
every path is instantiated (i'm constantly hitting by the bugs in my=20
templates due to missing some codepathes).

sorry for derailing the thread.=
Feb 24 2015
parent reply =?UTF-8?B?QWxpIMOHZWhyZWxp?= <acehreli yahoo.com> writes:
On 02/24/2015 11:15 AM, ketmar wrote:


 and it's interesting what complications templates can bring. testing
 templates is relatively hard now, 'cause programmer must ensure that
 every path is instantiated (i'm constantly hitting by the bugs in my
 templates due to missing some codepathes).


I was going to suggest dmd's code coverage tool but I've just witnessed 
the problem first-hand: Uninstantiated template code is not visible to 
the coverage analyser! :-o

Here is the program, where the code inside 'static if' is not covered 
(because argument 'a' is char):

T foo(T)(T v)
{
     static if (T.sizeof == 4) {
         ++v;
     }

     return v;
}

void main()
{
     int a = foo('a');
}

$ dmd deneme.d -cov
$ ./deneme
$ tail --lines=14 deneme.lst
        |T foo(T)(T v)
        |{
        |    static if (T.sizeof == 4) {
        |        ++v;
        |    }
        |
       1|    return v;
        |}
        |
        |void main()
        |{
       1|    int a = foo('a');
        |}
deneme.d is 100% covered

Yay! 100% covered. WAT? :p

Ali
Feb 24 2015
parent ketmar <ketmar ketmar.no-ip.org> writes:
On Tue, 24 Feb 2015 11:48:37 -0800, Ali =C3=87ehreli wrote:


 I was going to suggest dmd's code coverage tool but I've just witnessed
 the problem first-hand: Uninstantiated template code is not visible to
 the coverage analyser! :-o


yes. i don't think that this is a bug, though: coverage analyser analyses=20
only actually existing code, and non-instantiated template is=20
inexisting. ;-)

and forcing compiler to instantiate all possible template variants is=20
both impractical and not even possible, i think.

yet symbolic checker like KeY can be very handy here, i think. it can=20
prove that some instantiations are effectively the same, for example.=
Feb 24 2015
prev sibling parent reply ketmar <ketmar ketmar.no-ip.org> writes:
On Tue, 24 Feb 2015 10:47:19 -0800, Ali =C3=87ehreli wrote:


 Some implementation out there are buggy:
=20
=20
 http://www.reddit.com/r/programming/comments/2wze7z/


proving_that_androids_javas_and_pythons_sorting/

=20
 Ali


p.s. and yes, `TimSortImpl` is broken.=
Feb 24 2015
next sibling parent reply =?UTF-8?B?QWxpIMOHZWhyZWxp?= <acehreli yahoo.com> writes:
On 02/24/2015 11:20 AM, ketmar wrote:

 On Tue, 24 Feb 2015 10:47:19 -0800, Ali Çehreli wrote:


 Some implementation out there are buggy:


 http://www.reddit.com/r/programming/comments/2wze7z/


 proving_that_androids_javas_and_pythons_sorting/

 Ali


 p.s. and yes, `TimSortImpl` is broken.


Thanks. Posted:

   https://issues.dlang.org/show_bug.cgi?id=14223

Ali
Feb 24 2015
next sibling parent ketmar <ketmar ketmar.no-ip.org> writes:
On Tue, 24 Feb 2015 13:35:09 -0800, Ali =C3=87ehreli wrote:


 On 02/24/2015 11:20 AM, ketmar wrote:

 On Tue, 24 Feb 2015 10:47:19 -0800, Ali =C3=87ehreli wrote:


 Some implementation out there are buggy:


 http://www.reddit.com/r/programming/comments/2wze7z/


 proving_that_androids_javas_and_pythons_sorting/

 Ali


 p.s. and yes, `TimSortImpl` is broken.


 Thanks. Posted:
=20
    https://issues.dlang.org/show_bug.cgi?id=3D14223


i added a quick patch there. it would be fine if someone will run=20
unittests (and add a unittest for the case from the article), 'cause i=20
just did a mechanical translation of the fix without deep code analysing.=
Feb 24 2015
prev sibling parent "deadalnix" <deadalnix gmail.com> writes:
On Tuesday, 24 February 2015 at 21:35:10 UTC, Ali Çehreli wrote:

 On 02/24/2015 11:20 AM, ketmar wrote:

 On Tue, 24 Feb 2015 10:47:19 -0800, Ali Çehreli wrote:


 Some implementation out there are buggy:


 http://www.reddit.com/r/programming/comments/2wze7z/


 proving_that_androids_javas_and_pythons_sorting/

 Ali


 p.s. and yes, `TimSortImpl` is broken.


 Thanks. Posted:

   https://issues.dlang.org/show_bug.cgi?id=14223

 Ali


Beware, as commented on the original article, then linked on 
reddit and relinked here ( 
http://www.reddit.com/r/programming/comments/2wze7z/proving_that_androids_javas_and_pyt
ons_sorting/cow0de5 
) most of the proposed "fix" have the same issue as the blamed 
ode in the first place.
Feb 24 2015
prev sibling parent ketmar <ketmar ketmar.no-ip.org> writes:
On Tue, 24 Feb 2015 19:20:08 +0000, ketmar wrote:


 On Tue, 24 Feb 2015 10:47:19 -0800, Ali =C3=87ehreli wrote:
=20

 Some implementation out there are buggy:
=20
=20
 http://www.reddit.com/r/programming/comments/2wze7z/


 proving_that_androids_javas_and_pythons_sorting/

=20
 Ali


=20
 p.s. and yes, `TimSortImpl` is broken.


p.p.s. i can't really check that java code (it OOMs), and i supposed=20
"brokenness" from simply reading `TimSortImpl` (as it uses the same=20
algorithm as other implementations). so far it seems that to hit the bug=20
the arrays must be extraordinarily huge, so there is no need to take an=20
urgent action.=
Feb 24 2015