# Problem Set 3: Transition Systems, Logical Clocks, and Single-decree Paxos Due: Sunday, February 6, 11:59pm via Gradescope Each question is worth 5 points unless otherwise noted. ## Transition Systems For the next few problems, consider the following transition system: \[ \begin{align} S &= \mathbb{Z} \times \mathbb{Z}\\ S_0 &= \{(0, 5)\}\\ {\to} &= \{((x,y),\ (x+1, y-1)) \mid x,y\in\mathbb{Z}\}\\ \end{align} \] and the property \(P\) defined as \[ P = \{(x,y)\mid x,y\in\mathbb{Z}\text{ and (if }y=0\text{ then }x=5\text{)}\} \] It might help to draw yourself a 2d picture of the state space of this transition system. 1. Explain briefly and informally why \(P\) is an invariant. (Approximately one or two sentences.) 1. Show that \(P\) is *not* an inductive invariant by giving a counterexample to induction (CTI). No need to explain or prove anything, just state your counterexample. 1. (10 points) Define \(I\) by \[ I = \{(x,y)\mid x,y\in\mathbb{Z}\text{ and } x + y = 5\} \] Show that \(I\) is an inductive invariant of the transition system. (Approximately one paragraph.) 1. Prove that \(I\) is a subset of \(P\). (Approximately one sentence.) This finishes the proof that \(P\) is an invariant. Remember the definition of an inductive invariant: \(I\) is an inductive invariant if - \(I\) contains all initial states, i.e., \(S_0\subseteq I\), and - \(I\) is closed under transitions, i.e., whenever \(s\in I\) and \(s\to s'\), then \(s'\in I\). The next problem is about *stable properties*. A stable property is a set that satisfies the second bullet point above, but not necessarily the first bullet point. In other words, a stable property is a set that is closed under transitions (but may or may not contain all initial states). 1. Using the transition system from the previous few problems, give an example of a stable property that is *not* an inductive invariant. In other words, describe a set that is closed under transitions but does *not* contain the initial state. No need to prove or explain anything, just give your example. ## Logical Clocks Here is the example from the lecture 9 whiteboard. There are three process, \(P\), \(Q\), and \(R\), who communicate through message passing, as well as executing some local events (circles with no incoming or outgoing arrows). Recall that the happens-before relation \(e_1 \prec e_2\) is defined inductively by: - \(e_1\) and \(e_2\) occur in the same process and \(e_2\) is executed after \(e_1\) in that process - \(e_1\) is a message send event that sends message \(m\) and \(e_2\) is a message receive event that receives the same message \(m\) - there exists \(e_3\) such that \(e_1\prec e_3\) and \(e_3\prec e_2\) Intuitively, \(e_1 \prec e_2\) if there is a path from \(e_1\) to \(e_2\) in the graph whose edges are message send-receive pairs, plus an edge between subsequent events within a single process. In class we discussed the example \(p_1 \prec r_4\), since \[ \begin{align} p_1 &\prec q_2\\ &\prec q_4\\ &\prec r_3\\ &\prec r_4 \end{align} \] 1. Briefly explain why \(r_1\prec q_8\). (Just give the path.) Recall from lecture that we define two events \(e_1\) and \(e_2\) to be *concurrent* if \(e_1 \not\prec e_2\) and \(e_2 \not\prec e_1\), i.e., if neither event happens before the other. We write \(e_1 \parallel e_2\) to mean "\(e_1\) and \(e_2\) are concurrent". 1. Briefly explain why \(r_1\parallel p_4\). (Approximately two sentences. Explain why there is not a path from \(r_1\) to \(p_4\) and vice versa.) Suppose we implement logical clocks according to the technique discussed in lecture (which is the same as discussed in Lamport's paper). - Each process keeps track of its current logical time, which is an integer. Assume each process's clock starts at 0. - Each process increments its local time between every event it executes. - When sending a message, the sending process tags it with a timestamp, the value of the sender's logical clock at the time the message was sent. - When receiving a message, the receiving process sets its local clock to the maximum of (1) the message timestamp \(+1\) and (2) its current local clock value. (Note in the last bullet point: bullet point 2 still applies—the receiver still increments its local clock again after receiving the message and before executing the next event.) We will use the notation \(C(e)\) to mean the timestamp of event \(e\), as computed by Lamport's logical clock strategy described above. 1. Give a pair of events \(e_1\) and \(e_2\) from the graph above where \(C(e_1) < C(e_2)\) but \(e_1\not\prec e_2\). In other words, \(e_1\) is assigned an earlier logical timestamp than \(e_2\), but the events are not ordered by the happens-before relation. No need to prove or explain anything, just give your example. ## Single-decree Paxos There will be two or three questions here about single-decree Paxos. (EDIT: just kidding—moved to next week) ## Feedback 1. (This feedback question is also worth 5 points. It's optional, just like everything else.) How much time did you spend on this problem set? Feel free to include other feedback here.