4 ms·

There's an unofficial Jepsen test for TigerBeetle here: https://github.com/nurturenature/jepsen-tigerbeetle https://github.com/nurturenature/jepsen-tigerbeetle.

There's an unofficial Jepsen test for TigerBeetle here: https://github.com/nurturenature/jepsen-tigerbeetle 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.

matklad 4y ago
Also worth mentioning our simulation testing setup: https://github.com/tigerbeetledb/tigerbeetle/blob/b642c042614eec11dca4e0cad1ceb2beb45cff67/docs/HACKING.md#simulation-tests 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_random_testing_effective_for_partition_tolerance_bugs 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.
- losvedir 4y ago
  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?
  - pverghese 4y ago
    Not everything needs to be rewritten in rust or started in rust.
  - matklad 4y ago
    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 https://github.com/ziglang/zig/issues/3028 is a big component of that.
    - jorangreef 4y ago
      Is there a secret plan to improve Zig's IDE support? :)

matklad 4y ago

Also worth mentioning our simulation testing setup: https://github.com/tigerbeetledb/tigerbeetle/blob/b642c042614eec11dca4e0cad1ceb2beb45cff67/docs/HACKING.md#simulation-tests 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_random_testing_effective_for_partition_tolerance_bugs 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.

losvedir 4y ago
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?
- pverghese 4y ago
  Not everything needs to be rewritten in rust or started in rust.
- matklad 4y ago
  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 https://github.com/ziglang/zig/issues/3028 is a big component of that.
  - jorangreef 4y ago
    Is there a secret plan to improve Zig's IDE support? :)