HackerPapers

arXiv:1406.4291cs.DC

Vector Clocks in Coq: An Experience Report

Christopher Meiklejohn

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

This report documents the process of implementing vector clocks in the Coq proof assistant for extraction and use in the distributed Dynamo-inspired data store, Riak. In this report, we focus on the technical challenges of using Core Erlang code extracted from the proof assistant in a production-grade Erlang application, as opposed to verification of the model itself.

arXiv comments
Journal reference
DOI
Subjects
cs.DCDistributed, Parallel, and Cluster Computing cs.PLProgramming Languages cs.SESoftware Engineering

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Jul 2014 to Jul 2014.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Riak 2.0.0 RC1 1 comment

    • Full disclosure: I’m a current employee of Basho Technologies. Other than some supporting work [1] [2] introduced into 2.0 to provide advanced causality tracking, you’re correct in assuming we could have introduced more [3] CRDTs as part of the Riak 1.x series. We could have…

      cmeiklejohnView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.