<p>I understand the proof as follows.
Start with an arbitrary execution of the above algorithm. In this execution each operation on $TS[i]$ and $Val[i]$ has already been linearlized by assuming that these are single-writer multi-reader atomic registers. Therefore, by assumption, the schedule linearizes these low level operations.</p>

<p>The remainder of the proof shows that there exists some unique assignment of distinct times for each high-level operation such that the following are true.</p>

<ol>
<li>For each such operation that starts at time $t_s$ and ends at time
$t_e$, the assigned time $t_a$ is in the interval $[t_s,t_e]$. </li>
<li>The sequence of high-level  reads and writes, as determined by this assignment of times, satisfies the linearlizability.</li>
</ol>

CC BY-SA 3.0
2013-10-02T04:15:55.203Z
To confirm: Given an arbitrary execution of the simulation algorithm, the linearization points of *low-level operations* are fixed by assumption. Then, the assignment of linearization points of *high-level operations* does not change that of *low-level operations*.
hengxin
CC BY-SA 3.0
2013-10-01T20:42:33.853Z
2013-10-02T04:29:57.813Z
2013-10-02T04:29:57.813Z
Srikanth Sastry
<p><strong>Backgroud</strong></p>

<p>I am reading Chapter 10 ``Fault-Tolerant Simulations of Read/Write Objects'' of the Book <a href="http://www.cs.technion.ac.il/~hagit/DC/" rel="nofollow noreferrer">Distributed Computing (by Hagit Attiya &amp; Jennifer Welch)</a>. Specifically, in section 10.2.3, it simulates a multi-writer multi-reader read/write register from single-writer multi-reader registers.</p>

<p><strong>Simulation Algorithm</strong></p>

<blockquote>
  <p>The idea of the algorithm is to have each writer announce each value it desires to write to all the readers, by writing it in its own (single-writer multi-reader) registers; each reader reads all the values written by the writers and picks the most recent one among them.</p>
</blockquote>

<p>The algorithm uses vector clock to compare the values written by the writers and find the most recent one among them. The pseudocode appears in Figure <img src="https://i.sstatic.net/bOQ3X.png" alt="Simulation Algorithm">, where</p>

<blockquote>
  <ol>
  <li>$TS[i]:$ The vector timestamp of writer $p_i$, $0 \le i \le m - 1$. It is written by $p_i$ and read by all writers.</li>
  <li>$Val[i]:$ The latest value written by writer $p_i$, $0 \le i \le m - 1$, together with the vector timestamp associated with that value. It is written by $p_i$ and read by all readers.</li>
  </ol>
</blockquote>

<p><strong>Correctness Proof</strong></p>

<p>There are two types of operations in the algorithm:</p>

<ol>
<li><em>high-level operation:</em> operation on simulated object $R$ (i.e., $read_r(R)$ and $write_w(R,v)$ in the pseudocode).</li>
<li><em>low-level operation:</em> operation on $TS[i]$ and $Val[i]$.</li>
</ol>

<blockquote>
  <p>To prove that the simulation is correct we have to show that every admissible execution is linearizable. Consider any admissible execution $\alpha$. To show that $\alpha$ is linearizable, we have to show that there is a permutation $\pi$ of the <strong>high-level operations</strong> in $\alpha$ that preserves the order of non-overlapping operations, and in which every read operation returns the value of the latest preceding write.</p>
</blockquote>

<p><strong>My Problem</strong></p>

<p>As the last paragraph indicated, we consider the schedule of <strong>high-level operations</strong>. So my problem is:</p>

<blockquote>
  <p>Should the schedule of <strong>high-level operations</strong> also respect the linearizability of <strong>low-level operations</strong>?</p>
</blockquote>

<p>To illustrate, consider the following admissible (according to the simulation algorithm) execution:</p>

<blockquote>
  <p>Assume $TS[i][i] = 0, \forall 0 \le i \le m - 1$ initially. $m$ writers write concurrently. They all first execute Line 10 - Line 11 in procedure $NewCTS_w()$ and thus obtain $TS[i][i] = 0, \forall 0 \le i \le m - 1$. Then, they execute Line 12 in some order (for example, in the order of pid). In this scenario, when all writers finish, the system state can be stated as
  $$S = \left\{ \begin{array}{ll}
\langle 1, 0 , 0, \ldots, 0 \rangle \\
\langle 0, 1 , 0, \ldots, 0 \rangle \\
\langle 0, 0 , 1, \ldots, 0 \rangle \\
\langle 0, 0 , 0, \ldots, 1 \rangle
\end{array} \right.$$ </p>
</blockquote>

<p>In the linearizability proof, the $m$ <strong>high-level</strong> writes will be put in an order, for example, according to their pids. However, if we consider the <strong>low-level</strong> operations in such order, the second writer cannot obtain $\langle 0, 1, 0, \ldots, 0 \rangle$. Instead, it should obtain $\langle 1, 1, 0, \ldots, 0 \rangle$, because it is put after the first writer's <strong>high-level</strong> write operation.</p>

<blockquote>
  <p><strong>Problem:</strong> I am confused about the situation. What is wrong of my argument? Should the schedule respect the linearizability of <em>low-level operations</em> in simulation algorithm? Or, what does it mean to respect it?</p>
</blockquote>

<dc.parallel-comp><dc.distributed-comp><concurrency>
Should the Schedule of ``High-level Operations'' Respect the Linearizability of ``Low-level Operations'' in Proof of Simulation Algorithm?
hengxin
# Should the Schedule of ``High-level Operations'' Respect the Linearizability of ``Low-level Operations'' in Proof of Simulation Algorithm?

(Asked by: username_0 on 2013-10-01)

**Backgroud**

I am reading Chapter 10 ``Fault-Tolerant Simulations of Read/Write Objects'' of the Book [Distributed Computing (by Hagit Attiya & Jennifer Welch)](http://www.cs.technion.ac.il/~hagit/DC/). Specifically, in section 10.2.3, it simulates a multi-writer multi-reader read/write register from single-writer multi-reader registers.

**Simulation Algorithm**

> The idea of the algorithm is to have each writer announce each value it desires to write to all the readers, by writing it in its own (single-writer multi-reader) registers; each reader reads all the values written by the writers and picks the most recent one among them.

The algorithm uses vector clock to compare the values written by the writers and find the most recent one among them. The pseudocode appears in Figure ![Simulation Algorithm](https://i.sstatic.net/bOQ3X.png), where

> 1. $TS[i]:$ The vector timestamp of writer $p\_i$, $0 \le i \le m - 1$. It is written by $p\_i$ and read by all writers.
> 2. $Val[i]:$ The latest value written by writer $p\_i$, $0 \le i \le m - 1$, together with the vector timestamp associated with that value. It is written by $p\_i$ and read by all readers.

**Correctness Proof**

There are two types of operations in the algorithm:

1. *high-level operation:* operation on simulated object $R$ (i.e., $read\_r(R)$ and $write\_w(R,v)$ in the pseudocode).
2. *low-level operation:* operation on $TS[i]$ and $Val[i]$.

> To prove that the simulation is correct we have to show that every admissible execution is linearizable. Consider any admissible execution $\alpha$. To show that $\alpha$ is linearizable, we have to show that there is a permutation $\pi$ of the **high-level operations** in $\alpha$ that preserves the order of non-overlapping operations, and in which every read operation returns the value of the latest preceding write.

**My Problem**

As the last paragraph indicated, we consider the schedule of **high-level operations**. So my problem is:

> Should the schedule of **high-level operations** also respect the linearizability of **low-level operations**?

To illustrate, consider the following admissible (according to the simulation algorithm) execution:

> Assume $TS[i][i] = 0, \forall 0 \le i \le m - 1$ initially. $m$ writers write concurrently. They all first execute Line 10 - Line 11 in procedure $NewCTS\_w()$ and thus obtain $TS[i][i] = 0, \forall 0 \le i \le m - 1$. Then, they execute Line 12 in some order (for example, in the order of pid). In this scenario, when all writers finish, the system state can be stated as
> $$S = \left\{ \begin{array}{ll}
> \langle 1, 0 , 0, \ldots, 0 \rangle \\
> \langle 0, 1 , 0, \ldots, 0 \rangle \\
> \langle 0, 0 , 1, \ldots, 0 \rangle \\
> \langle 0, 0 , 0, \ldots, 1 \rangle
> \end{array} \right.$$

In the linearizability proof, the $m$ **high-level** writes will be put in an order, for example, according to their pids. However, if we consider the **low-level** operations in such order, the second writer cannot obtain $\langle 0, 1, 0, \ldots, 0 \rangle$. Instead, it should obtain $\langle 1, 1, 0, \ldots, 0 \rangle$, because it is put after the first writer's **high-level** write operation.

> **Problem:** I am confused about the situation. What is wrong of my argument? Should the schedule respect the linearizability of *low-level operations* in simulation algorithm? Or, what does it mean to respect it?

**Tags:** dc.parallel-comp, dc.distributed-comp, concurrency

---

## 1 answers

### Answer by username_1 on 2013-10-01. Score: 1 | Accepted answer

I understand the proof as follows.
Start with an arbitrary execution of the above algorithm. In this execution each operation on $TS[i]$ and $Val[i]$ has already been linearlized by assuming that these are single-writer multi-reader atomic registers. Therefore, by assumption, the schedule linearizes these low level operations.

The remainder of the proof shows that there exists some unique assignment of distinct times for each high-level operation such that the following are true.

1. For each such operation that starts at time $t\_s$ and ends at time
   $t\_e$, the assigned time $t\_a$ is in the interval $[t\_s,t\_e]$.
2. The sequence of high-level reads and writes, as determined by this assignment of times, satisfies the linearlizability.

> **Comments:**
> **username_0**: To confirm: Given an arbitrary execution of the simulation algorithm, the linearization points of *low-level operations* are fixed by assumption. Then, the assignment of linearization points of *high-level operations* does not change that of *low-level operations*.  

---

