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 re

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 box Atomic 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

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 succes

Popular posts from this blog

Hints for Distributed Systems Design

Learning about distributed systems: where to start?

Making database systems usable

Looming Liability Machines (LLMs)

Foundational distributed systems papers

Advice to the young

Linearizability: A Correctness Condition for Concurrent Objects

Scalable OLTP in the Cloud: What’s the BIG DEAL?

Understanding the Performance Implications of Storage-Disaggregated Databases

Designing Data Intensive Applications (DDIA) Book