Wednesday, October 26, 2016

Modeling the Dining Philosophers Algorithm in TLA+

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 messy.) The philosophers cycle between 3 states: thinking, hungry, and eating. The dining philosopher protocol should satisfy 1. (safety) if a process is eating neither of its left neighbor or right neighbor can be eating, and 2. (progress) if a process is hungry, eventually it gets to eat.

Dijkstra's formulation is an example of a token-based approach to mutual exclusion. Unlike token-based solutions to mutual exclusion where there is only one token in the system (as only one node is allowed to be in the critical section at any given time), the dining philosophers formulation relaxes the requirement and introduces one token (i.e., fork) per edge. A node that is eating needs to possess all the forks on its side, hence the safety condition is easily satisfied: if a process is eating, neither/none of its neighbors can be eating. The progress condition on the other hand is more trickier to satisfy and we will devote most of our attention on satisfying the progress condition in the below algorithms.

PlusCal modeling of naive dining philosophers

Here is a PlusCal algorithm modeling of the dining philosophers problem.

There are N processes from 0..N-1. (You can provide N at model-checking time.) Each process is symmetric, they execute the same code instantiated with their ID. Each process has a variable called state, and loops through selecting 3 actions. From "state=thinking", the process can transition to "hungry". A hungry process first waits till the fork on its right is available and then grabs it. The hungry process then waits till the fork on its left is available and grabs it, and transitions into eating state. An "eating" process can transition to "thinking" by releasing its left and right forks.

OK, let's have the birds and bees talk now. How do we model a system at a suitable abstraction layer? When we are trying to get the basics of the algorithm right, we don't need to model the protocol at a message passing level. Let's get it right at the shared memory model first. Modeling the system at a suitable abstraction layer is an art. Novice users often make the mistake of writing Java-like iterative programs with PlusCal. This makes the code long and also very slow for model checking. After seeing better ways to model systems looking at other PlusCal code examples, novice users gradually learn to write more declarative math-like specifications. I believe this latter mode of thinking also helps improve their system design skills as well (which is what makes me most excited about using/teaching TLA+). I find that once you get the "define" block right, the rest of the PlusCal algorithm practically writes itself. But you may need to make a couple unsuccessful takes before you figure out the most suitable "define" block that leads to a succinct and elegant model.

In my modeling I use a shortcut to model the forks between two process. There are N forks, so I model the forks using an array of size N. The left fork of a philosopher is the fork that resides at the array index given by the ID of that philosopher. The right fork of a philosopher is the fork at index=ID+1 (modulo N). I say that a fork is available for grabs if the fork's value is set to N. When a process grabs its left fork or right fork, the fork's value is assigned to be equal to the ID of that process, so we denote that the fork is not available anymore. (Note that "self" refers to the ID of the process.)

When we model-check our algorithm, TLA+ complains and alerts us to a deadlock. Below is the deadlock trace provided by TLA+. You can see that all process are blocked at label "E:" where each one of them is waiting to grab its left fork. You can click on each step in the trace to see the program state at that step, and see how the final deadlock state is reached as a result. The problem turns out to be this: all the processes first grabbed their right fork, and when they try to grab their left fork, they can't because those forks have been grabbed by their respective right neighbors as a right fork.

Modeling dining philosophers with a distinguished philosopher

As a general principle in conflict resolution, it is necessary to break the symmetry. As long as each philosopher looks exactly like the others, the problem is hopeless, the processes run into a deadly embrace. So let's differentiate process 0 as being lefty: while all philosophers grab their right fork first, process 0 tries to grab its left fork first and its right fork later. This bit of asymmetry breaks the cyclic dependency for the availability of the forks. We changed only the second action of the program as below. When transitioning from hungry to eating, we introduced an if branch. If the process ID is 0, the process grabs left fork first instead of grabbing its right fork first.

When we model check this code, we find that since the symmetry is broken, the deadlock is avoided. However, TLA+ still complains about starvation. The "NoStarvation" predicate asserts that it is always the case that if a process is hungry, eventually that process gets to eat. In other words, no process starves. When we ask TLA+ to check NoStarvation in the temporal properties, TLA+ produces the following long counterexample. Inspecting the loop from state 19 to state 28, you see that process 2 can get to eat again and again while process 1 and 0 remains at the "hungry" state and starve. This counterexample is possible with a weak-fair scheduler. The scheduler chooses process 1 to execute every so often, but only when its left fork is unavailable so its left-fork grab action is disabled. (A strongly-fair scheduler would solve this deadlock, because process 1 will get chosen to execute the left-fork-grab action when the guard of the left-fork-grab is enabled. You can tell TLA+ to use strong-fairness by typing "fair+ process" in the PlusCal code. Also you would need to replace the either or construct with an "if else if else if else" construct, so TLA+ scheduler cannot get away with choosing to execute an inactive "or branch".)

The way to solve this problem under weak fairness is to introduce a flag to reduce the priority of a process once it eats, so that a hungry neighbor will have higher priority and can get to eat. We are going to look at such a solution in the next blog post on TLA+: the hygienic philosophers algorithm.


Naive Dining Philosophers model in TLA+
Dining Philosophers with a distinguished process model in TLA+ 

The PlusCal code for the two programs are accessible through the above links. When you want to model check the program, start a new model, and enter 3 for N, so the model checker is ready to start. In the model checker tab, click on Invariant pane and enter ME, so that the ME predicate is checked against any violation, and in the Properties pane enter NoStarvation so that the progress property is checked for satisfaction. If you make a modification to the PlusCal code, make sure you click on File, Translate Algorithm, so the PlusCal code gets translated to the TLA+ code, which is then used for the model-checking. See the TLA+ posts below about how this works.

Related Links

Using TLA+ for teaching distributed systems

My experience with using TLA+ in distributed systems class

There is a vibrant Google Groups forum for TLA+:!forum/tlaplus

By clicking on label "tla" at the end of the post you can reach all my posts about TLA+

Monday, October 24, 2016

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.

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 rate, which results in clock drift from "True Time". Ovenizing the oscillators provides a way to control/compensate temperature change. OCXO ovenized oscillators have a drift of 25 microsecond a day.

GPS time (box/distribution)

There are 4 big satellite  systems. GPS is the biggest and is maintained by US. Then comes GLONASS (yeah I know) by Russia,  Galileo by Europe, and  Beidou by China. India also has some regional satellites as well. Today all smartphones have support for GPS, and some recent ones also support GLONASS as well.

The satellites, which are up there around 20,000km altitude, have Ribidium based atomic clocks and they distribute time sync information. That looks like an awfully long distance, but that doesn't stop the satellites to serve as the most prominent time sync solution. Why? The answer has to do with distribution of time sync. Distribution of time sync over many hops/routers on the  Internet degrades the precision of the time sync. When distributing with wires, you have to relay: it is infeasible to have one long physical cable. And thus relaying/switching/routing adds nondeterministic delays to the time sync information. For the satellites, we have wireless distribution. Albeit the long distance, distribution from satellite is still one hop. And the distance delay is deterministic, because it can be calculated precisely by dividing the distance to the satellite with the speed of light. The accuracy of GPS time signals is ±10 ns.

GPS is an engineering marvel. Here you can read more (and admire) about GPS. Here are some interesting highlights about GPS synchronization. Constant ground-based correction is issued to the satellites to account for relativistic effects and other effects. Ground stations (US naval observatory NIST) transmit to satellites periodically to update/correct their atomic clocks for  Coordinated Universal Time (UTC). GPS is weatherproof. Even big storms would not degrade GPS signals significantly. However, jamming is more of a problem, since GPS is a very low power signal.

Assisted GPS helps smartphones lock on to the low power GPS signals. Celltowers provide smartphones with approximate time and position information. And also include GPS constellation information. So the smartphone knows where/which signals to lock to. There are also Pseudolites. These are stable on-the-ground satellite beacons. They simulate satellites and are now being considered for indoor localization systems. They spoof GPS, their signal overloads smartphones GPS chipsets.

Time sync distribution

NTP is by far the most popular time sync distribution protocol on the Internet. However, NTP clock sync errors can be amount to tens of milliseconds. The biggest source of problem for NTP distribution is the asymmetry in the links. Consider 100 mbps link feeding into 1 Gbps link. One way there is no delay, but coming back the other way there is queuing delay. This asymmetry introduces errors into time sync. NTP is also prone to security attacks. Having your timeservers are good for increased security against NTP attacks. Finance sector doesn't use NIST public source NTP servers since men-in-the-middle attack is possible. (Of course, it is also not that difficult to spoof GPS.) That all being said, I have great respect for the engineering efforts went into NTP, and what all NTP has provided for distributed systems over Internet. David Mills is a hero.

PTP IEEE 1588 is another time sync distribution protocol. PTP stands for precision time protocol PTP comes from industrial networking where it started as a multicast protocol. PTP enables hardware timestamping and has measures to eliminate link delay asymmetry. The time provider sends MAC-stamped time to the client, so the client can measure in-flight-time between time-server and itself. (In NTP time provider does not know the client, and is stateless with respect to the client. In NTP, the client asks and gets response from the NTP server which is oblivious to the client.) PTP does not have a standard reference implementation.

Applications of time sync

A big customer of time synchronization systems is power grids which use time synchronization to manage load balancing, distribution, and load shedding. Celltowers are also big customers of time synchronization. Celltowers used to have on-the-wire proprietary synchronization updated with sync-e or PTP. GPS-based synchronization has been replacing those quickly. As I mentioned earlier finance industry is a big client for time synchronization systems.

Time sync also have emerging applications in cloud/datacenter computing. The most prominent is probably Google Spanner which uses atomic clocks and GPS clocks to support externally-consistent distributed transactions at global scale.

I have been working on better clocks for distributed systems, and hybrid logical clocks and hybrid vector clocks resulted from that work. I am continuing that work to further explore the use of clocks for improving auditability of large scale distributed systems, as part of our project titled "Synchrony-aware Primitives for Building Highly Auditable, Highly Scalable, Highly Available Distributed Systems" (funded by NSF XPS, from 2015-2019, PI: Murat Demirbas and coPI: Sandeep Kulkarni):

"Auditability is a key property for developing highly scalable and highly available distributed systems; auditability enables identifying performance bottlenecks, dependencies among events, and latent concurrency bugs. In turn, for the auditability of a system, time is a key concept. However, there is a gap between the theory and the practice of distributed systems in terms of the use of time. The theory of distributed systems shunned the notion of time and considered asynchronous systems, whose event ordering is captured by logical clocks. The practical distributed systems employed NTP synchronized clocks to capture time but did so in ad hoc undisciplined ways. This project will bridge this gap and provide synchrony-aware system primitives that will support building highly auditable, highly scalable, and highly available distributed systems. The project has applications to cloud computing, distributed NewSQL databases, and globally distributed web services."

Wednesday, October 19, 2016

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 successful businessman who got a minor stroke in striatum and lost all interest in business and life. This chapter also presents a story from Marines bootcamp, and how the Marines find the motivation to endure through the tough challenge exercises. Yet another story in the first chapter is about mundanely subversive/rebellious behavior by the elderly in nursing houses. The common theme about all three stories, which is the key for motivation, is the concept of "choice". The elderly who displays minor acts of rebellion/subversiveness remain healthy and function longer, because they are exercising their power to choose, and not blindly obey. In the case of the businessman who lost his interest to live and succeed, his wife relentlessly helps him make small choices, and overtime he starts to recover. In the case of the Marines, their commanders train them to make choices and display "ownership". (In another recent book "Extreme Ownership" by Jocko Willinks and Leif Babin explore this issue.) When facing great challenges, the best way to get started is by making some choices. Albeit tiny, the choices we make give us a sense of control, takes us out of the frame of mind of learned helplessness and victimhood, and we start to exercise our internal locus of control. Another point made through the Marines bootcamp story is to keep "a big vision" to motivate you in following your goals. When we are feeling down, we should ask ourselves "why" we choose to endure these hardship, and get the big vision to motivate us to inch along to that direction.

The second chapter is "Teams". It presents the story of Julia as she graduates from Yale School of Management and joins Google's People Analytics group to investigate what makes teams more effective. Yes, there is no surprise: having diverse teams is better. But, surprisingly, the ultimate factor in effectiveness of teams is the psychological safety: do team members feel safe in expressing and defending opinions? The chapter also tells about the story of two hospital wards, one with high mistake rates, and the other with low mistake rates. In a twist ending, it turns out that the ward with lower mistake rates is not better, but that the members feel unsafe about reporting mistakes and mistakes are simply not accounted for. The ward with the higher mistake rates turns out to be the better functioning ward, because the members report every mistake, and those mistakes are mostly smaller mistakes and measures are taken to correct them before they escalate to critical problems. Finally, the chapter tells colorful stories about the good olden days of the Saturday Night Live, and how a team of misfits and rebels,argue each other continuously but manage to put on a fantastic show every weekend.

The third chapter is "Focus". It turns out too much focus could be a bad thing, because it can lead to a tunnel-vision of attention. This point was driven home by the heart-wrenching story of Air France Flight 447. What a nightmare! I got very uncomfortable even by reading the account of it. (Charles Duhigg is a great story teller, and managed to climb the tension/tragedy of the story expertly.) The pilots tunnel-vision to a wrong measure/lead, and things gradually spiral worse and worse. I almost started to yell, "how could you get things so wrong?". This plane could not possibly have gone down, yet there it does like a slow-motion trainwreck (taking place at an altitude of 30,000 feet). The chapter also tells the story of Qantas Flight 32, the most damaged Airbus A380 ever to land safely. The pilot managed to achieve this by thinking of the plane as a simple Cessna plane, and not getting tunneled into irrelevant metrics/leads, and staying vigilant by keeping this simple but holistic mental model in mind. The pilot and copilots kept their options open, did not delegate thinking, and managed to make good decisions under stress by the power of their mental model for the plane. The chapter also tells the story of nurse Darlene: she had the mental model of what a healthy baby should look like, and was able to recognized problematic babies much earlier and save their lives. The take home message from this chapter is that you should have narratives about what to focus and what to ignore and mental models of the process (which you constantly reevaluate and readjust), so you can stay vigilant and prepared.

The fourth chapter is on "Goal setting". The chapter has two very engaging stories: one about General Electrics, and the other about the Yom Kippur war, and makes points about how to set smart goals without getting too carried away. A smart goal is specific, measurable, achievable, realistic, has timeline (see, it is an acronym). The chapter first makes this point through the GE story, and then says, smart goals are not enough, you also need to have stretch goals, and makes this point in the second half of the GE story. The stretch goals are there to push the limits; you can't grow a system unless you strain it some. This brings the antifragility concept to mind. Through the Yom Kippur War story the chapter drives the point that, you shouldn't get too obsessed about your goals that you get carried away and rule out obstacles/threats to your strategy as very low-risk.

The fifth chapter is about "Managing others". Through two stories, General Motors Toyota partnership story and a kidnapping case FBI successfully solved, it makes points about agile thinking and building a culture of thrust. The stories are again engaging, but at this point, I was hoping that there would be less stories, because I was losing the thread of smarter, faster, better. Again it takes a special talent to weave two very unrelated stories to make a somewhat coherent case, but I got weary of following the stories and trying to figure out how these relate to the themes of other chapters and the other 10 stories told on those chapters. At this point, I declared maximum story saturation for myself.

The sixth chapter is about "Decision Making". The story is about how Annie Duke won the 2004 Tournament of Champions for poker. Again an engaging story, and there is some connection to how to weigh out possible future outcomes when planning. While the connection of poker and weighing possible future outcomes through Bayesian reasoning is literal, I wished that instead of reading a lengthy poker story I could read about more concrete and applicable tactics/strategies about decision making and weighing out possible outcomes.

The seventh chapter is about "Innovation". It tells the story of Disney's Frozen and also there is a story about creation of "West Side Story" (emphasis mine). I tried to remember back to what was the insight in this chapter, but couldn't recall a significant one. When I looked up the chapter again, I found that the insight was "creativity is just problem solving". So I was not much off the mark.

The final chapter is about "Absorbing Data". The lesson here is that even if you collect data and use data processing/visualization, if you are not internalizing the results, these are all for vain. This lesson was told through the story of some teachers that analyzed student evaluation data by hand, made up stories/hypothesis about how to interpret these, and put effort in the process, which helped improve the success of Cincinnati's public schools. The problem with relying on automation of analysis is that, it would be easy come easy go. If you haven't thought about it and internalize it, you didn't get benefit from it. You can't delegate thinking to computers (at least not yet).

In conclusion, I think Duhigg is a great story teller, and he overdid that in this book. Yes, the stories were super engaging, but they are just anecdotes and you can come up with many other stories to make counterpoints. Instead of so many stories, I would have loved to read more tips/ideas/heuristics about how to get smarter, faster, better, and more concrete application use cases.

The subtitle of the book promises us "the secrets of being productive in life and business", and, of course, the book fails to deliver that. Because there is no secret. There is no silver bullet for avoiding failures, and no bulletproof recipe for success. There is no shortcut. To be smarter, faster, and better, you should become smarter, faster, and better. Tips, ideas, even paradigm shifts may give us only some boost in getting there. Becoming smarter, faster, and better is a constant inward battle where we have to continuously struggle to earn our badges.

Two-phase commit and beyond

In this post, we model and explore the two-phase commit protocol using TLA+. The two-phase commit protocol is practical and is used in man...