Articles


Modeling ZLog in Promela: Part 2

Dec 2017 in the second part we are going to tackle the bug we saw in the first that occurred when the sequencer restarted Articles in this series: This post is part of the following series: Background The basic issue in the previous version was that objects allowed client operations to succeed when those clients had stale knowledge about the system state. CORFU handles this through a mechanism called seal and retry logic in the client.

Modeling ZLog in Promela: Part 1

Dec 2017 Introduction blurb about this post. Articles in this series: This post is part of the following series: ZLog Links Basic ZLog Is it correct? Modeling Basic idea about modeling Other approaches We are using Spin in this article A ZLog Spin Model We start with a constrained and simplified model of the system. Over the course of several posts we will increase the detail of the model until it accurately reflects the real-world implementation.