Should the Schedule of ``High-level Operations'' Respect the Linearizability of ``Low-level Operations'' in Proof of Simulation Algorithm?

Question

Backgroud

I am reading Chapter 10 ``Fault-Tolerant Simulations of Read/Write Objects'' of the Book Distributed Computing (by Hagit Attiya & Jennifer Welch). 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 , 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?

Answer 1

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.