Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                                   EN LIGNE
                             MARDI 7 juin, 10h30

                                 Kartik Nagar
                                  IIT Madras

                  Certified Mergeable Replicated Data Types

Replicated data types (RDTs) are data structures that permit
concurrent modification of multiple, potentially geo-distributed
replicas without coordination between them. RDTs are designed in such
a way that conflicting operations are eventually deterministically
reconciled ensuring convergence. Constructing correct RDTs remains a
difficult endeavour due to the complexity of reasoning about
independently evolving states of the replicas. With the focus on the
correctness of RDTs (and rightly so), existing approaches to RDTs are
less efficient compared to their sequential counterparts in terms of
the time and space complexity of local operations. This is unfortunate
since RDTs are often used in a local-first setting where the local
operations far outweigh remote communication.

In this talk, I will present Peepul, a pragmatic approach to building
and verifying efficient RDTs. To make reasoning about correctness
easier, we cast RDTs in the mould of the distributed version control
system, and equip it with a three-way merge function for reconciling
conflicting versions. Further, we go beyond just verifying
convergence, and provide a methodology to verify arbitrarily complex
specifications. We develop a replication-aware simulation relation to
relate RDT specifications to their efficient purely functional
implementations. We implement Peepul as an F* library that discharges
proof obligations to an SMT solver. The verified efficient RDTs are
extracted as OCaml code and used in Irmin, a distributed database
built on the principles of Git.

Joint work with Vimala S, Adharsh Kamath and KC Sivaramakrishnan.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                  https://webconf.math.cnrs.fr/b/fra-ryy-fjn