Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Fastest branchless binary search

mhdm.dev

Post reply on HN
Print view View original

141–150 of 155 posts

Re: Fastest branchless binary search

#141

Post by User23 »

LegionMammal978 wrote: post #135
User23 wrote: post #119

Earlier quoted context omitted.

You have to scroll down a bit, but see here[1]. Also searching [site:regehr.org compcert] will find more. CompCert C makes it impossible to reproduce at least some UB bugs: For CompCert, the high-level correctness theorems I proved are all of the first kind above: if the source program goes wrong, nothing is guaranteed about the behavior of the compiled code. It happens, however, that the stepwise simulation lemmas I…

Apart from compiler bugs, this issue with "time-traveling UB" shouldn't really occur in practice with any side effects other than volatile accesses. As noted by Martin Uecker [0], > In portable C code I/O is performed using function calls of the standard library. A compiler can generally not assume that a function returns to the caller, because the function could call ‘exit’, ‘abort’, ‘longjmp’, or enter an infinite…

> through. I'd say that even "some C bugs" is a overstatement outside of embedded programming, given the rarity of MMIO in a hosted environment.

I don’t concede your claims, but I’m enough out of the loop that I won’t attempt to refute them either. However, for what it’s worth, embedded programming is exactly where I most want that.

Furthermore, I don’t know of any other popular bare metal language that’s even close to having a compiler offering mechanically provable assertions about its compiled behavior. Do you?

Re: Fastest branchless binary search

#142

Post by thefifthsetpin »

Bognar wrote: post #139
thefifthsetpin wrote: post #117

Earlier quoted context omitted.

Binary search reduces the search space exponentially as it proceeds, so actually quite a lot of the total comparisons can hit L1d cache. (Maybe half of them for a ~250GB dataset.) Of course, you could keep a cacheable partial index of your huge dataset to accelerate the early part of your search as well.

Sounds like we're just reinventing B-trees.

Yep. I considered phrasing my answer that way.

Re: Fastest branchless binary search

#143

Post by fl0ki »

Pro tip, the footer link https://doc.rust-lang.org/src/core/slice/mod.rs.html#2520 is not a permalink because it doesn't include a commit ID. It looks like it's already linking to the wrong thing now (and the article is only two months old), and I don't know what the right thing was meant to be. I suggest using GitHub permalinks in future, pinned to specific commits.

Re: Fastest branchless binary search

#144

Post by eru »

User23 wrote: post #59
eru wrote: post #38

Earlier quoted context omitted.

> Also, what's wrong with C? Oodles and oodles of undefined behaviour, for example. C ain't clean.

Nah, thanks to CompCert[1] C actually has one of the highest quality and most predictable compilers. [1] https://compcert.org/

Well, that one tells you that the compilers translate your program according to the language spec.

That's helpful, but doesn't make the language itself saner.

Re: Fastest branchless binary search

#145

Post by eru »

User23 wrote: post #141
LegionMammal978 wrote: post #135

Earlier quoted context omitted.

Apart from compiler bugs, this issue with "time-traveling UB" shouldn't really occur in practice with any side effects other than volatile accesses. As noted by Martin Uecker [0], > In portable C code I/O is performed using function calls of the standard library. A compiler can generally not assume that a function returns to the caller, because the function could call ‘exit’, ‘abort’, ‘longjmp’, or enter an infinite…

> through. I'd say that even "some C bugs" is a overstatement outside of embedded programming, given the rarity of MMIO in a hosted environment. I don’t concede your claims, but I’m enough out of the loop that I won’t attempt to refute them either. However, for what it’s worth, embedded programming is exactly where I most want that. Furthermore, I don’t know of any other popular bare metal language that’s even close…

> Furthermore, I don’t know of any other popular bare metal language that’s even close to having a compiler offering mechanically provable assertions about its compiled behavior. Do you?

You can automatically extract low level code out of certain high level, provable languages. I think some of them might offer the guarantee you asked for (assuming you eg use a certified C compiler for the last leg).

Re: Fastest branchless binary search

#146

Post by LegionMammal978 »

User23 wrote: post #141
LegionMammal978 wrote: post #135

Earlier quoted context omitted.

Apart from compiler bugs, this issue with "time-traveling UB" shouldn't really occur in practice with any side effects other than volatile accesses. As noted by Martin Uecker [0], > In portable C code I/O is performed using function calls of the standard library. A compiler can generally not assume that a function returns to the caller, because the function could call ‘exit’, ‘abort’, ‘longjmp’, or enter an infinite…

> through. I'd say that even "some C bugs" is a overstatement outside of embedded programming, given the rarity of MMIO in a hosted environment. I don’t concede your claims, but I’m enough out of the loop that I won’t attempt to refute them either. However, for what it’s worth, embedded programming is exactly where I most want that. Furthermore, I don’t know of any other popular bare metal language that’s even close…

> Furthermore, I don’t know of any other popular bare metal language that’s even close to having a compiler offering mechanically provable assertions about its compiled behavior. Do you?

Well, if you ask the question that narrowly, then I suppose not, unless CakeML's GC is lightweight enough to be stuffed onto some board or another.

But 99% of the time (i.e., when I am not doing something intentionally strange to test the language's limits), the correctness of the program I'm writing, or at least of its dependencies (including the standard library), is far more questionable than the correctness of the compiler; after all, the output of, say, GCC and LLVM has been tested by oodles of real-world software. Even if I'm really paranoid, I can disable all optimizations and reenable any less-questionable ones individually.

Thus the GP's complaint, that C is filled to the brim with undefined behavior that will silently cause corruption in production code instead of failing loudly, since all the runtime sanitizers (AFAIK) swear up and down that they aren't very secure.

I do hope that that formal verification on the program's side becomes more accessible in the future, though, either via dedicated systems like Daphny or via "gradual verification" as permitted by things like Why3 frontends for different languages. (In particular, I've been meaning to look into the Creusot project for Rust.) But short of formal verification, robust runtime assertions and guardrails are generally the best bet, and C as a language simply doesn't provide very good tools for those.

Re: Fastest branchless binary search

#149

Post by ot »

dzaima wrote: post #127
ot wrote: post #19

Earlier quoted context omitted.

Which also does not affect cmov conversion. Every time this comes up I bring up this long-standing LLVM bug: https://bugs.llvm.org/show_bug.cgi?id=40027

__builtin_unpredictable is gonna be fixed in LLVM/clang 17: https://github.com/llvm/llvm-project/commit/09515f2c20111628... (also, bugs.llvm.org is old; the more up-to-date (but still open) issue is https://github.com/llvm/llvm-project/issues/39374 )

Amazing, finally!!!

Re: Fastest branchless binary search

#150

Post by VHRanger »

alain94040 wrote: post #109

I don't get it. The problem with binary search and branches is not the branches themselves, it's the fact that until you have done the comparison, you don't know which memory location in the array to fetch next. It doesn't matter if you use branches or anything else, the question is what do you want the processor to do? There is a data dependency: until I read the middle index, I can't tell if I want to search the da…

Right, this is why proper faster binary search use eytzinger array layout:

https://algorithmica.org/en/eytzinger

Post reply on HN