3 ms·

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 fare

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!

eatonphil 4y ago
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? :)

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!

eatonphil 4y ago

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? :)