digitalmars.D - Is D's TimSort correct?
- =?UTF-8?B?QWxpIMOHZWhyZWxp?= (4/4) Feb 24 2015 Some implementation out there are buggy:
- ketmar (16/22) Feb 24 2015 their KeY system is very interesting. i'm very curious what minimal=20
- =?UTF-8?B?QWxpIMOHZWhyZWxp?= (36/40) Feb 24 2015 I was going to suggest dmd's code coverage tool but I've just witnessed
- ketmar (8/11) Feb 24 2015 yes. i don't think that this is a bug, though: coverage analyser analyse...
- ketmar (3/9) Feb 24 2015 p.s. and yes, `TimSortImpl` is broken.=
- =?UTF-8?B?QWxpIMOHZWhyZWxp?= (4/13) Feb 24 2015 Thanks. Posted:
- ketmar (4/21) Feb 24 2015 i added a quick patch there. it would be fine if someone will run=20
- deadalnix (6/22) Feb 24 2015 Beware, as commented on the original article, then linked on
- ketmar (6/17) Feb 24 2015 p.p.s. i can't really check that java code (it OOMs), and i supposed=20
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
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 Alitheir 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
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
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! :-oyes. 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
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 Alip.s. and yes, `TimSortImpl` is broken.=
Feb 24 2015
On 02/24/2015 11:20 AM, ketmar wrote:On Tue, 24 Feb 2015 10:47:19 -0800, Ali Çehreli wrote:Thanks. Posted: https://issues.dlang.org/show_bug.cgi?id=14223 AliSome implementation out there are buggy: http://www.reddit.com/r/programming/comments/2wze7z/proving_that_androids_javas_and_pythons_sorting/Alip.s. and yes, `TimSortImpl` is broken.
Feb 24 2015
On Tue, 24 Feb 2015 13:35:09 -0800, Ali =C3=87ehreli wrote:On 02/24/2015 11:20 AM, ketmar wrote: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.=On Tue, 24 Feb 2015 10:47:19 -0800, Ali =C3=87ehreli wrote:Thanks. Posted: =20 https://issues.dlang.org/show_bug.cgi?id=3D14223Some implementation out there are buggy: http://www.reddit.com/r/programming/comments/2wze7z/proving_that_androids_javas_and_pythons_sorting/Alip.s. and yes, `TimSortImpl` is broken.
Feb 24 2015
On Tuesday, 24 February 2015 at 21:35:10 UTC, Ali Çehreli wrote:On 02/24/2015 11:20 AM, ketmar wrote: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.On Tue, 24 Feb 2015 10:47:19 -0800, Ali Çehreli wrote:Thanks. Posted: https://issues.dlang.org/show_bug.cgi?id=14223 AliSome implementation out there are buggy: http://www.reddit.com/r/programming/comments/2wze7z/proving_that_androids_javas_and_pythons_sorting/Alip.s. and yes, `TimSortImpl` is broken.
Feb 24 2015
On Tue, 24 Feb 2015 19:20:08 +0000, ketmar wrote:On Tue, 24 Feb 2015 10:47:19 -0800, Ali =C3=87ehreli wrote: =20p.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.=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.
Feb 24 2015