TLA+ model checking made symbolic

TLA+ model checking made symbolic Konnov et al., OOPSLA'19 TLA+ is a formal specification language (Temporal Logic of Actions) particularly well suited to reasoning about distributed algorithms. In addition to the specification language, the TLA+ toolset includes a model checker (TLC) and a theorem prover (TLAPS). Given the huge state spaces involved in many real-world … Continue reading TLA+ model checking made symbolic

Mergeable replicated data types – Part II

Mergeable replicated data types - part II Kaki et al., OOPLSA '19 Last time out we saw how Mergeable Replicated Data Types (MRDTs) use a bijection between the natural domain of a data type and relational sets to define merge semantics between two concurrently modified versions given their lowest common ancestor (LCA). Today we’re picking … Continue reading Mergeable replicated data types – Part II

Mergeable replicated data types – Part I

Mergeable replicated data types Kaki et al., OOPSLA'19 This paper was published at OOPSLA, but perhaps it’s amongst the distributed systems community that I expect there to be the greatest interest. Mergeable Replicated Data Types (MRDTs) are in the same spirit as CRDTs but with the very interesting property that they compose. Furthermore, a principled … Continue reading Mergeable replicated data types – Part I

PlanAlyzer: assessing threats to the validity of online experiments

PlanAlyzer: assessing threats to the validity of online experiments Tosch et al., OOPSLA'19 It’s easy to make experimental design mistakes that invalidate your online controlled experiments. At an organisation like Facebook (who kindly supplied the corpus of experiments used in this study), the state of art is to have a pool of experts carefully review … Continue reading PlanAlyzer: assessing threats to the validity of online experiments

Local-first software: you own your data, in spite of the cloud

Local-first software: you own your data, in spite of the cloud Kleppmann et al., Onward! '19 Watch out! If you start reading this paper you could be lost for hours following all the interesting links and ideas, and end up even more dissatisfied than you already are with the state of software today. You might … Continue reading Local-first software: you own your data, in spite of the cloud

Formal foundations of serverless computing

Formal foundations of serverless computing Jangda et al., OOPSLA'19 Jangda et al. won a distinguished paper award at OOPSLA this year for their work on ‘Formal foundations of serverless computing.’ Central to the paper is their observation that the serverless execution environment has a number of unique properties (such as warm starting / reuse of … Continue reading Formal foundations of serverless computing