Hacker News Reader

Comment by mdaniel | Hacker News Reader

I've now been conditioned to say "ok, when can we expect the Jepsen?" when I see a new database. Although in this case the phrase "in-process" (and it apparently being built on top of Apache Arrow: https://github.com/kuzudb/kuzu/blob/master/external/arrow/ap... ) may make that nonsense, but the readme does also say "Serializable ACID transactions"

View on HN

I don't quite follow the question here but to clarify one thing: Kùzu is currently integrating Arrow not as a core storage structure but as a file format from which we can ingest data. We are writing Kùzu's entire storage, so it's our own design. It has three components: Vanilla columns for node properties, columnar compressed sparse row (https://tinyurl.com/2r2s4wpe) join indices and relationship properties, and a hash index for primary keys of node records. We don't use Arrow to store db files.

For serializability: yes, we support serializable transactions. So when you insert, delete or update node, rel records, you get all or nothing behavior (e.g., if you rollback none of your updates will be visible).

That said, supporting ACID transactions is a compeletely separate design decision in DBMSs, so our (or other systems') mechanisms to support transactions (for example whether it's based on write ahead logging or not) and storage designs are generally mutually exclusive decisions.

As sibling comments have said, "if you rollback none of your updates will be visible" is a claim but Jepsen is designed to prove such a thing. Same with the claims of transactional behavior, and claims of Serializable

My _personal_ opinion is that databases written in footgun languages need more formal verification of claims, not less, but I guess one needs to also take into consideration the size of the audience who would be impacted by any mistake when deciding if it's worth the investment or not

---

Please don't use link shorteners on HN; we're adults here and are capable of seeing long URLs, whereas link shorteners (a) die (b) obscure the destination

https://en.wikipedia.org/wiki/Sparse_matrix#Compressed_spars...

This is actually a very good point and unfortunately formal verification is not the current norm when developing DMBSs or complex systems software. If you asked how do you know DBMS X is correctly implementing snapshot isolation, no one will be able to provide a lesson for you. This is true for every system out there I'm aware of. This goes more deeply actually about questions like this: "how do you know you implement SQL or Cypher correctly". In fact, we can't even sometimes very formally answer "what is the meaning of this query X". Back in the day my PhD advisor Jennifer Widom, who had a background in programming languages, talked a lot about how we put DBMSs into everywhere, e.g., planes that are flying up in the air, yet we can't really precisely state what the outputs of queries should be. She had some excellent writing on this for implementation of triggers that were coming out of different groups. She was one of the pioneers of triggers before triggers existed in SQL. And as I assume you might know better than me, Leslie Lamport is known as a pioneer in the distributed systems space for formal verification of programs.

Your comment on shortened URLs is noted. This is my first HN post ever :), so I might need to pick up the customs.

provide a lesson -> provide a proof.

I don't Jepsen has any relevance to embedded (in-process) databases, nor to any single-node databases. The properties its testing for are related to network partition tolerance.

But the tool that jepsen uses to check whether a schedule is serializable would still be useful for any database that supports concurrent operations.

I agree with that. For example, Jepsen has analyzed non-replicated PostgreSQL: https://jepsen.io/analyses/postgresql-12.3

There are plenty of mistakes you can make in single-process code while implementing transactions.

Agreed.

Reply on news.ycombinator.com