Problem Set 2: Correctness of Distributed Systems

Due: Friday, January 20, 11:59pm via Gradescope

Each problem is worth 5 points.

In Lecture 5, we defined the Incrementing Counter System as a transition system as follows:

• State space: pairs \((n, M\)) where \(n\) is a (mathematical) integer and \(M\) is a set of messages.
  • Messages: Only one message, Inc.
  • Therefore either \(M = \{\}\) or \(M = \{\mathtt{Inc}\}\)
• Initial state: \((0, \{\})\)
• Transitions:
  • The client can send an Inc message.
    • From any state \((n, M)\), this transition moves us into the state \((n, M\cup\{\mathtt{Inc}\})\).
  • The server can receive an Inc message.
    • From any state \((n, M)\) where \(\mathtt{Inc}\in M\), this transition moves us into the state \((n+1, M)\).

Also recall the definitions of an invariant and a stable property.

• A property is an invariant if it is true in all reachable states.
• A property is stable if, once it becomes true, it never becomes false again.
  • We call a property "unstable" if it is not stable.

Note that these definitions are relative to a specific system.

1. Demonstrate that the Incrementing Counter System models network duplication despite not having an explicit transition for duplicating a message by describing an execution where the client only sends the Inc message once, but the server increments its counter twice.

2. In lecture we mentioned that, in the Incrementing Counter System, \(n\ge 1\) is stable but not an invariant because it is false in the initial state. Describe another reachable state that is not the initial state where \(n \ge 1\) is also false.

3. Consider the property "\(n = 0\)" in the Incrementing Counter System. Is it unstable, stable but not an invariant, or an invariant? If it is unstable, describe an execution where the property is true at some point, but later false. (In this and subsequent problems, don't forget to follow the instructions at the top of this assignment about how to describe an execution.) If it is stable, explain why in one sentence. If it is not an invariant, describe a reachable state where it is false. If it is an invariant, explain why in one sentence.

4. Consider the property "\(M = \{\mathtt{Inc}\}\)" in the Incrementing Counter System. Is it unstable, stable but not an invariant, or an invariant? If it is unstable, describe an execution where the property is true at some point, but later false. If it is stable, explain why in one sentence. If it is not an invariant, describe a reachable state where it is false. If it is an invariant, explain why in one sentence.

5. Consider the property "\(n\ge -1\)" in the Incrementing Counter System. Is it unstable, stable but not an invariant, or an invariant? If it is unstable, describe an execution where the property is true at some point, but later false. If it is stable, explain why in one sentence. If it is not an invariant, describe a reachable state where it is false. If it is an invariant, explain why in one sentence.

6. Consider the property "\(M = \{\}\)" in the Incrementing Counter System. Is it unstable, stable but not an invariant, or an invariant? If it is unstable, describe an execution where the property is true at some point, but later false. If it is stable, explain why in one sentence. If it is not an invariant, describe a reachable state where it is false. If it is an invariant, explain why in one sentence.

Recall the Incrementing Counter System with Response Messages from lecture 5. Here is the transition system for your reference:

• State space: \((n, M)\) where \(n\in\mathbb{Z}\) is the server's count (an integer) and \(M\in \mathtt{Set\langle Msg\rangle}\) is the set of messages
  • A \(\mathtt{Msg}\) is either the message Inc or a message of the form \(\mathtt{Resp}(j)\) where \(j\) is an integer.
• Initial state: \((0, \{\})\).
• Transitions:
  • The client can send an Inc message.
    • From any state \((n, M)\), this transition moves us into the state \((n, M\cup\{\mathtt{Inc}\})\).
    • In other words, the server's count doesn't change and we add the Inc message to the set of sent messages.
  • The server can receive an Inc message.
    • From any state \((n, M)\) where \(\mathtt{Inc}\in M\), this transition moves us into the state \((n+1, M\cup\{\mathtt{Resp}(n+1)\})\).
    • In other words, we increment the server's count and send a response message back to the client with the new count.

What's new is the Resp messages, in which the server sends the client a copy of its current counter.

1. Consider the property "\(M = \{\mathtt{Inc}\}\)" in the Incrementing Counter System with Response Messages. Is it unstable, stable but not an invariant, or an invariant? If it is unstable, describe an execution where the property is true at some point, but later false. (In this and subsequent problems, don't forget to follow the instructions at the top of this assignment about how to describe an execution.) If it is stable, explain why in one sentence. If it is not an invariant, describe a reachable state where it is false. If it is an invariant, explain why in one sentence.

2. Is the state \((0, \{\mathtt{Inc}, \mathtt{Resp}(1)\})\) reachable in the Incrementing Counter System with Response Messages? If yes, describe an execution that reaches it. On the other hand, if this state is not reachable, describe an invariant that is false in this state. (In this case, explain why your invariant is an invariant in one sentence.)

3. Is the state \((1, \{\mathtt{Inc}, \mathtt{Resp}(1)\})\) reachable in the Incrementing Counter System with Response Messages? If yes, describe an execution that reaches it. On the other hand, if this state is not reachable, describe an invariant that is false in this state. (In this case, explain why your invariant is an invariant in one sentence.)

4. Is the state \((2, \{\mathtt{Inc}, \mathtt{Resp}(2)\})\) reachable in the Incrementing Counter System with Response Messages? If yes, describe an execution that reaches it. On the other hand, if this state is not reachable, describe an invariant that is false in this state. (In this case, explain why your invariant is an invariant in one sentence.)