BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//HasGeek//NONSGML Funnel//EN
DESCRIPTION:Read by Raghav Roy
X-WR-CALDESC:Read by Raghav Roy
NAME:PWL Dec 2023: "Verifying Strong Eventual Consistency in Distributed S
 ystems"
X-WR-CALNAME:PWL Dec 2023: "Verifying Strong Eventual Consistency in Distr
 ibuted Systems"
REFRESH-INTERVAL;VALUE=DURATION:PT12H
SUMMARY:PWL Dec 2023: "Verifying Strong Eventual Consistency in Distribute
 d Systems"
TIMEZONE-ID:Asia/Kolkata
X-PUBLISHED-TTL:PT12H
X-WR-TIMEZONE:Asia/Kolkata
BEGIN:VEVENT
SUMMARY:PWL Dec 2023: "Verifying Strong Eventual Consistency in Distribute
 d Systems"
DTSTART:20231216T070000Z
DTEND:20231216T100000Z
DTSTAMP:20260421T140532Z
UID:session/Tzrarrf854S1BZeb56aHKq@hasgeek.com
SEQUENCE:14
CREATED:20231202T073851Z
DESCRIPTION:\n## About the paper\nData replication is a well discussed con
 cept for maintaining up-to-date copies of shared data in distributed syste
 ms. Although it is critical for the correctness of a system\, implementing
  it still remains a challenging task. Despite decades of research\, achiev
 ing consistency in replicated systems is still not well understood\, in fa
 ct\, many previously published algorithms have been later shown to be inco
 rrect.\n\nIf we have to prove the correctness of Conflict-Free Replicated 
 Datatypes\, we need to formalise the guarantees it provides - Strong Event
 ual Consistency (SEC)\, and we have to do this in the context of a network
 -model that reflects real-world computer networks\, with all the asynchron
 ous and unreliable goodness modeled in as well.\n\nThe paper builds step b
 y step towards this goal of formalising SEC and then embedding various rep
 lication algorithms into this axiomatic network model. This is done using 
 Isabelle/HOL\, which is a strict\, type-inferred proof assistant.\n\nThe p
 aper is published here: https://www.cl.cam.ac.uk/~arb33/papers/GomesEtAl-V
 erifyingSEC-OOPSLA2017.pdf\n## Key Takeaways\n- Basic definitions and some
  necessary conditions for replication algorithms\, a great read to underst
 and concepts like SEC and what it guarantees\, and causality in the contex
 t of generalised network models\n- How we can move step-by-step defining c
 onditions\, locales and theorems for some really subtle concepts using Isa
 belle/HOL. Even if you are new to Formal Methods\, the approach this paper
  takes explaining it is intuitive.\n- Defining an axiomatic network model 
 that doesn't make wrong assumptions about the real-world and embedding som
 e simple replication algorithms like RGA\, Counter and OR-Set\n## About th
 e Presenter\nRaghav Roy is a systems engineer at VMware working with Netwo
 rk Virtualisation and the ESXi kernel. His interests (atleast relevant to 
 this paper) include distributed systems\, formalisation techniques and its
  application in real world systems\, and building systems that scale.\nHe 
 also contributes to open source\, which is mostly Kubernetes\, but the str
 uggle with maintaining closed source and open source contributions is some
 thing he is very vocal about.\n\n**Slides for this talk:** https://speaker
 deck.com/royra/pwl-dec-2023-verifying-strong-eventual-consistency-in-distr
 ibuted-systems
LAST-MODIFIED:20231216T163655Z
LOCATION:TBD - https://hasgeek.com/pwl_bangalore/16-12/
ORGANIZER;CN="Papers We Love Bangalore":MAILTO:no-reply@hasgeek.com
URL:https://hasgeek.com/pwl_bangalore/16-12/
BEGIN:VALARM
ACTION:display
DESCRIPTION:PWL Dec 2023: "Verifying Strong Eventual Consistency in Distri
 buted Systems" in 5 minutes
TRIGGER:-PT5M
END:VALARM
END:VEVENT
END:VCALENDAR