Posts

Showing posts from October, 2016

Modeling the Dining Philosophers Algorithm in TLA+

Image
In this post I will provide a modeling of the dining philosophers algorithm in TLA+. If you have not heard about TLA+ before, take a look at my earlier posts on TLA+ to get some context.  Post1 and Post2

The dining philosophers problem is an instance/refinement of the mutual exclusion problem. The specification of the mutual exclusion problem dictates that when a node is in critical section, no other node in the system can be in the critical section. The dining philosopher relaxes this by taking into account the topology: When a node is in critical section, none of the neighbors of that node can be in critical section. Note that, this does not rule out two nodes to be in critical section simultaneously provided that they are not neighbors.

In the original formulation of the dining philosophers problem by Dijkstra, there are 5 philosophers sitting around a table. Between each philosopher is a fork and, in order to eat a philosopher must hold both of the forks. (The spaghetti is really …

It is about time

A couple months ago, I had visitors from SpectraCom. They gifted me a GPS timeserver. I am now the guy with the most accurate time in the department.
I have a GPS clock in my office. Syncs < 100 nanosecond of UTC. pic.twitter.com/9XkDFSMdKm — Murat Demirbas (@muratdemirbas) August 9, 2016
We met with these engineers for a couple hours discussing about time synchronization. It was a very enjoyable discussion and time flew by. We talked about how to achieve time synchronization at a box, how to distribute it, and its applications. I had taken some notes, and thought it would be useful to share them.

Estimated reading time: 6 minutes.
Suggested song to accompany (right-click and open link in new tab): Time from Pink Floyd

Precise clocks in a boxAtomic clocks often use Ribidium, which has a drift of only 1 microsecond a day. OCXO ovenized oscillators are the second best way to have precise clocks in a box. Temperature change has the most effect in crystal oscillation rate, which results …

Book Review: Smarter Faster Better (2016)

I read this book in early September. My review comes after a month's lag, so I am not fresh on the details of the book, and can't totally recall my reactions while reading each chapter. However, sometimes it is better to write a review not afresh, but after some gestation period, so you can provide a more balanced review.

Overall I liked the book. It is a fun read. Charles Duhigg is a great story teller. Maybe to a fault. In retrospect I think the stories diluted the focus of the book, and the real ideas/tips for becoming "smarter, faster, better" got shortchanged. After I briefly describe each chapter, I will revisit this point at the end of this post.

The first chapter is "Motivation". What motivates us to work hard and get after it? There is a physiological component to motivation regulated by the "striatum" in the subcortical part of the forebrain, a critical component of the reward system. This chapter talks about the case of a very successfu…

Popular posts from this blog

I have seen things

SOSP19 File Systems Unfit as Distributed Storage Backends: Lessons from 10 Years of Ceph Evolution

PigPaxos: Devouring the communication bottlenecks in distributed consensus

Frugal computing

Learning about distributed systems: where to start?

Fine-Grained Replicated State Machines for a Cluster Storage System

My Distributed Systems Seminar's reading list for Spring 2020

My Distributed Systems Seminar's reading list for Fall 2020

Cross-chain Deals and Adversarial Commerce

Book review. Tiny Habits (2020)