# 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.