Verified Foundations of Large-Scale Distributed Graph Systems – VERDI

Traditional relational data management systems are challenged by the abundance of highly interconnected heterogeneous data. This led to a surge in the popularity of graph databases in many industry and academic areas. For example, graph datasets with world-wide multi-omics data for genomic analyses and contact tracing were collaboratively curated during the pandemic (EU Datathon, CovidGraph, Covid-19 Knowledge Graph). Other critical societal graph databases use-cases include finance, telecommunications, journalism, and intelligent transportation. However, when processing geo-distributed graph data at scale, custom distribution models are needed, whose support still poses practical challenges. These are: replication, to mitigate slow and unreliable networks; sharding, to horizontally partition large graphs; and partial replication, to favor access locality, replicating data close to clients. Moreover, local-first models provide high availability, combining sharding and replication for read and write access to a relevant data subset, even when disconnected. While distribution mechanisms, such as Replicated Data Types (RDTs), have become well-established for local-first key-value stores, their usage in graph databases is largely unexplored. This is a more complex setting, due to its stronger demands to compositionally maintain connectivity invariants. VERDI proposes a novel interdisciplinary methodology to reliably devise such foundational distribution devices, cross-cutting the areas of databases, distributed systems, formal methods, and programming languages. It comprises four work packages (WPs). WP1 will build a unified formal foundation for prototyping and extracting correct-by-construction graph RDTs (GRDTs). WP2 will tailor these to provably enforce complex invariants under weak consistency models. WP3 will extend GRTDs with parametricity and transactional support and WP4 will evaluate their performance on a decentralized graph-based ledger industrial use-case.