Verified Vector Clocks An Unexpected Journey
summary
Coq extraction to Core Erlang generates runnable code and an explicit Coq extraction to Core Erlang pipeline plus a glue adapter for Basho’s database, but the work requires many manual fixes: missing data constructors, incorrectly qualified calls, lack of currying, and heavy type conversions. The extracted module passes the test suite but runs very slowly and adds unverified adapter logic. The usable outcome is a verified core algorithm and a manual adapter layer with many fixes; next idea is generating QuickCheck models from proofs.
AI-written summary · about
chapters (27)
- 0:00Introduction
- 1:22Outline
- 3:06CRDTs
- 7:03Contributions
- 7:50Out of Scope
- 11:30Bool
- 12:08QLang
- 15:43Caveats
- 18:01Vector Clocks Review
- 19:58Vector Clocks Implementation
- 22:31List
- 25:46Merge
- 27:11Pruning
- 28:07Extraction
- 28:57Missing Data Constructor
- 30:01Missing EraDS
- 30:28Lack of currying
- 31:16Adapter Layer
- 33:32Type Conversions
- 33:57Boolean
- 34:24Timestamp
- 34:45Actors
- 36:16Prune
- 37:29Normalize
- 38:51Evaluation
- 40:44Future Work
- 43:09Questions
related talks
22mTowards Modelling and Verification of Coupler Behaviour in Climate Models
20mAn Automated Scalable RISC-V Cache Coherency Verification Project
40mSo I used Erlang...is my system as scalable as they say it'd be?
14mBridging the Gap between Real-World and Formal Binary Lifting through(…)
30mVisual concurrency cookbook
24mErla+: Translating TLA+ Models into Executable Actor-Based Implementations
17mLet It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
15mModular Verification of Op-Based CRDTs in Separation Logic