Does TigerBeetle have a formal proof of serializability or has it been verified by the Jepsen tests? It's mentioned in the blog post and I'm curious how it fares in that department.
This isn’t as thorough as model-checking or proving a formalization of the algorithm, but it has the benefit of working with the real code. It is a bit less real than Jepsen (as we essentially mock all syscalls), but is quite a bit faster.
Oh wow, are you on the TigerBeetle team then? I only knew of you as the rust-analyzer guy, with awesome posts on your blog.
Do you have any thoughts on how working on TigerBeetle with Zig is? It seems like for a high performance DB rust would be a natural choice. And how's the development experience without a zig-analyzer?
Yup, I am that matklad. I have thoughts, will put then into a post some time soonish.
zig-analyzer is great — much further along than I’d expected at this point. Though, I am still curious what the end game IDE support would look. https://github.com/ziglang/zig/issues/3028 is a big component of that.
Comments
Does TigerBeetle have a formal proof of serializability or has it been verified by the Jepsen tests? It's mentioned in the blog post and I'm curious how it fares in that department.
Cool project!
There's an unofficial Jepsen test for TigerBeetle here: https://github.com/nurturenature/jepsen-tigerbeetle. and we've worked with them (nurturenature) to fix some bugs they've found.
No formal proof at the moment either but it's something we're thinking about.
Also worth mentioning our simulation testing setup: https://github.com/tigerbeetledb/tigerbeetle/blob/b642c04261....
Everything is fully deterministic, time is externalized, so our simulation can run very fast and explore a lot of random permutations of events (which is quite effective: https://www.researchgate.net/publication/322133078_Why_is_ra...).
This isn’t as thorough as model-checking or proving a formalization of the algorithm, but it has the benefit of working with the real code. It is a bit less real than Jepsen (as we essentially mock all syscalls), but is quite a bit faster.
Oh wow, are you on the TigerBeetle team then? I only knew of you as the rust-analyzer guy, with awesome posts on your blog.
Do you have any thoughts on how working on TigerBeetle with Zig is? It seems like for a high performance DB rust would be a natural choice. And how's the development experience without a zig-analyzer?
Yup, I am that matklad. I have thoughts, will put then into a post some time soonish.
zig-analyzer is great — much further along than I’d expected at this point. Though, I am still curious what the end game IDE support would look. https://github.com/ziglang/zig/issues/3028 is a big component of that.
Is there a secret plan to improve Zig's IDE support? :)
Not everything needs to be rewritten in rust or started in rust.