6 ms·

>I have to still do some extra correctness vetting and testing, and in particular exception-safety is still not yet fully implemented. This is important because

by xavxav 4y ago

>I have to still do some extra correctness vetting and testing, and in particular exception-safety is still not yet fully implemented. This is important because I wrote it in Rust where we must always give back a valid initialized array, even if a comparison operator caused a panic. But I do have some performance numbers to quote, that won't significantly change. Do you make extensive use of `unsafe` Rust? What other features do you use? I ask this as my PhD thesis is building a deductive verifier for (safe) Rust, and I'm always looking out for interesting challenges. If you would ever be interested in a collaboration proving your algorithm correct let me know :)

orlp 4y ago
> Do you make extensive use of `unsafe` Rust? Yes. Glidesort moves data back and forth between partially initialized buffers a lot, so unsafe code is unavoidable. I also need to concatenate slices that are adjacent in memory, which is impossible to do with safe slices (due to pointer provenance). Mixing pointers/slices in general is just a bad idea, so for the most part I simply use pointers. I use no other special (unstable) features, just pointers and ptr::copy(_nonoverlapping). > If you would ever be interested in a collaboration proving your algorithm correct let me know :) I might take you up on that, or at least ask you to take a look once I'm done polishing the code.
- xavxav 4y ago
  > Yes. Glidesort moves data back and forth between partially initialized buffers a lot, so unsafe code is unavoidable. I also need to concatenate slices that are adjacent in memory, which is impossible to do with safe slices (due to pointer provenance). Mixing pointers/slices in general is just a bad idea, so for the most part I simply use pointers. Ah, that's frustrating, my tool Creusot is meant for the verification of safe code, though I also worked on unsafe code verification as part of the RustHornBelt project (upcoming PLDI paper). I'd still love to chat and see how far we can push verification, you can reach me via email at xldenis @ lri . fr

by xavxav 4y ago

orlp 4y ago

> Do you make extensive use of `unsafe` Rust? Yes. Glidesort moves data back and forth between partially initialized buffers a lot, so unsafe code is unavoidable. I also need to concatenate slices that are adjacent in memory, which is impossible to do with safe slices (due to pointer provenance). Mixing pointers/slices in general is just a bad idea, so for the most part I simply use pointers. I use no other special (unstable) features, just pointers and ptr::copy(_nonoverlapping). > If you would ever be interested in a collaboration proving your algorithm correct let me know :) I might take you up on that, or at least ask you to take a look once I'm done polishing the code.

xavxav 4y ago
> Yes. Glidesort moves data back and forth between partially initialized buffers a lot, so unsafe code is unavoidable. I also need to concatenate slices that are adjacent in memory, which is impossible to do with safe slices (due to pointer provenance). Mixing pointers/slices in general is just a bad idea, so for the most part I simply use pointers. Ah, that's frustrating, my tool Creusot is meant for the verification of safe code, though I also worked on unsafe code verification as part of the RustHornBelt project (upcoming PLDI paper). I'd still love to chat and see how far we can push verification, you can reach me via email at xldenis @ lri . fr