4 ms·

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 w

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 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.

mdaniel 4y ago
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_sparse_row_(CSR,_CRS_or_Yale_format) https://en.wikipedia.org/wiki/Sparse_matrix#Compressed_spars...
- semihsalihoglu 4y ago
  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.
  - semihsalihoglu 4y ago
    provide a lesson -> provide a proof.

mdaniel 4y ago

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_sparse_row_(CSR,_CRS_or_Yale_format) https://en.wikipedia.org/wiki/Sparse_matrix#Compressed_spars...

semihsalihoglu 4y ago
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.
- semihsalihoglu 4y ago
  provide a lesson -> provide a proof.