linenum

# Efficient Distributed Data Structures for Future Many-core Architectures

Panagiota Fatourou
FORTH-ICS & Univ. of Crete
<EMAIL_ADDRESS>Nikolaos D. Kallimanis
ISI / Athena RC & University of Ioannina
<EMAIL_ADDRESS>Eleni Kanellou
FORTH-ICS
<EMAIL_ADDRESS>Contact author. Address: FORTH-ICS. N. Plastira 100,
Vassilika Vouton. GR-70013 Heraklion (Crete), Greece. Tel.: +302810391709
Odysseas Makridakis
Univ. of Crete
<EMAIL_ADDRESS>Christi Symeonidou
Univ. of Crete
<EMAIL_ADDRESS>

###### Abstract

We study general techniques for implementing distributed data structures on
top of future many-core architectures with non cache-coherent or partially
cache-coherent memory. With the goal of contributing towards what might
become, in the future, the concurrency utilities package in Java collections
for such architectures, we end up with a comprehensive collection of data
structures by considering different variants of these techniques. To achieve
scalability, we study a generic scheme which makes all our implementations
hierarchical. We consider a collection of known techniques for improving the
scalability of concurrent data structures and we adjust them to work in our
setting. We have performed experiments which illustrate that some of these
techniques have indeed high impact on achieving scalability. Our experiments
also reveal the performance and scalability power of the hierarchical
approach. We finally present experiments to study energy consumption aspects
of the proposed techniques by using an energy model recently proposed for such
architectures.

##  1 Introduction

The dominant parallelism paradigm used by most high-level, high productivity
languages such as Java, is that of threads and cache-coherent shared memory
among all cores. However, cache-coherence does not scale well with the number
of cores [1]. So, future many-core architectures are not expected to support
cache-coherence across all cores. They would rather feature multiple coherence
islands, each comprised of a number of cores that share a coherent view of a
part of the memory, but no hardware cache-coherence will be provided among
cores of different islands. Instead, the islands will be interconnected using
fast communication channels. In recent literature, we meet even more
aggressive approaches with Intel having proposed two fully non cache-coherent
architectures, Runnemede [2] and SSC [3]. Additionally, [4] presents the
Formic board, a 512-core non cache-coherent prototype.

Such architectures impose additional effort in programming them, since they
require to explicitly code all communication and synchronization using
messages between processors. Previous works [5, 6, 7] indicate the community’s
interest in bridging the gap between non cache-coherent or distributed
architectures, and high-productivity programming languages by implementing
runtime environments, like the Java Virtual Machine (JVM), for such
architectures, which maintain the shared-memory abstraction.

The difficulty in parallelizing many applications comes from those parts of
the computation that require communication and synchronization via data
structures. Thus, the design of effective concurrent data structures is
crucial for many applications. On this avenue, java.util.concurrent, which is
Java’s concurrency utilities package (JSR 166) [8, 9] provides a wide
collection of concurrent data structures [8, 10, 11, 12]. To run Java-written
programs on a non cache-coherent architecture, Java’s VM must be ported to
that architecture, and some fundamental communication and synchronization
primitives (such as CAS, locks, and others) must be implemented. Normally,
once this is done, it will be possible to execute applications that employ the
concurrency utilities package without any code modification. However, the
algorithms provided in the package have been chosen to perform well on shared
memory architectures. So, they take no advantage of the communication and
synchronization features of non cache-coherent architectures and do not cope
with load balancing issues or with the distribution of data among processors.
Thus, they are expected to be inefficient when executing through JVMs ported
for such an architecture, even if optimized implementations of locks, CAS, and
other primitives are provided on top of the architecture. Therefore, there is
an urgent need to develop novel data structures and algorithms, optimized for
non cache-coherent architectures.

We study general techniques for implementing distributed data structures, such
as stacks, queues, dequeues, lists, and sets, on many-core architectures with
non or partially cache-coherent memory. With the goal of contributing to what
might become, in the future, the concurrency utilities package in Java
collections for such architectures, we end up, by considering different
variants of these techniques, ending up with a comprehensive collection of
data structures, richer than those provided in java.util.concurrent. Our
collection, which is based on message-passing to achieve the best of
performance, facilitates the execution of Java-written code on non-cache
coherent architectures, without any modification, in a highly efficient way.

To achieve scalability, that is, maintaining good performance as the number of
cores increases [13], we study a generic scheme, which can be used to make all
our implementations hierarchical [14, 15]. The hierarchical version of an
implementation exploits the memory structure and the communication
characteristics of the architecture to achieve better performance.
Specifically, just one core from each island, the island master, participates
in the execution of the implemented distributed algorithm, whereas the rest
submit their requests to this core. To execute the implemented distributed
algorithm, the island masters must exploit the communication primitives
provided for fast communication among different islands. In architectures with
thousands of cores, we could employ a more advanced hierarchical structure,
e.g. a tree-like hierarchy, of intermediate masters for better scalability.
Depending on the implemented data structure, the island master employs
elimination [16], batching and other techniques to enhance scalability and
performance. In the partially cache-coherent case, the cores of the same
island may synchronize by employing combining [15, 17].

For efficiency, in some of our implementations, we employ a highly scalable
distributed hash table (DHT) which uses a simple standard technique [18, 19,
20] to distribute the data on different nodes. Based on it and by employing
counting networks [21, 22], we can come up with fully decentralized, scalable
implementations of queues and stacks. We also present implementations of
(sorted and unsorted) lists, some of which support complex operations like
range queries. To design our algorithms, we derive a theoretical framework
which captures the communication characteristics of non cache-coherent
architectures. This framework may be of independent interest. In this spirit,
we further provide full theoretical proofs of correctness for some of the
algorithms we present.

We have performed experiments on top of a non cache-coherent 512-core
architecture, built using the Formic [4] hardware prototyping board. We
distill the experimental observations into a metric expressing the scalability
potential of such implementations. The experiments illustrate nice scalability
characteristics for some of the proposed techniques and reveal the performance
and scalability power of the hierarchical approach.

##  2 Related Work

Distributed transactional memory (DTM) [23, 24, 25, 26, 27, 28, 29, 30] is a
generic approach for achieving synchronization, so data structures can be
implemented on top of it. Transactional memory (TM) [31, 32] is a programming
paradigm which provides the transaction’s abstraction; a transaction executes
a piece of code containing accesses to data items. TM ensures that each
transaction seems to execute sequentially and in isolation. However, it
introduces significant performance overheads whenever reads from or writes to
data items take place, and requires the programmer to write code in a
transactional-compatible way. (When the transactions dynamically allocate
data, as well as when they synchronize operations on dynamic data structures,
compilers cannot detect all possible data races without trading performance,
by introducing many false positives.) Our work is on a different avenue:
towards providing a customized library of highly-scalable data structures,
specifically tailored for non cache-coherent machines.

TM2C [26] is a DTM proposed for non cache-coherent machines. The paper
presents a simple distributed readers/writers lock service where nodes are
responsible for controlling access to memory regions. It also proposes two
contention management (CM) schemes (Wholly and FairCM) that could be used to
achieve starvation-freedom. However, in Wholly, the number of times a
transaction $T$ may abort could be as large as the number of transactions the
process executing $T$ has committed in past, whereas in FairCM, progress is
ensured under the assumption that there is no drift [33, 34] between the
clocks of the different processors of the non cache-coherent machine. Read-
only transactions in TM2C can be slow since they have to synchronize with the
lock service each time they read a data item, and in case of conflict, they
must additionally synchronize with the appropriate CM module and may have to
restart several times from scratch. Other existing DTMs [23, 24, 35, 30, 36],
also impose common DTM overheads.

The data structure implementations we propose do not cause any space overhead,
read-only requests are fast, since all nodes that store data of the
implemented structure search for the requested key in parallel, and the number
of steps executed to perform each request is bounded. We remark that, in our
algorithms, information about active requests is submitted to the nodes where
the data reside, and data are not statically assigned to nodes, so our
algorithms follow neither the data-flow approach [37, 36] nor the control-flow
approach [23, 35] from DTM research.

Distributed directory protocols [38, 39, 40, 41, 42] have been suggested for
locating and moving objects on a distributed system. Most of the directory
protocols follow the simple idea that each object is initially stored in one
of the nodes, and as the object moves around, nodes store pointers to its new
location. They are usually based either on a spanning tree [43, 42] or a
hierarchical overlay structure [38, 40, 41]. Remarkably, among them, COMBINE
[38] attempts to cope with systems in which communication is not uniform.
Directory protocols could potentially serve for managing objects in DTM.
However, to implement a DTM system using a directory protocol, a contention
manager must be integrated with the distributed directory implementation. As
pointed out in [39], this is not the case with the current contention managers
and distributed directory protocols. It is unclear how to use these protocols
to get efficient versions of the distributed data structures we present in
this paper.

Previous research results [44, 45, 46, 47] propose how to support dynamic data
structures on distributed memory machines. Some are restricted on tree-like
data structures [46, 47], other focus on data-parallel programs [44], some
favor code migration, whereas other focus on data replication. We optimize
beyond simple distributed memory architectures by exploiting the communication
characteristics of non cache-coherent multicore architectures. Some techniques
from [44, 45, 46] could be of interest though to further enhance performance,
fault-tolerance and scalability in our implementations.

Distributed data structures have also been proposed [48, 49, 50, 51, 52] in
the context of peer-to-peer systems or cluster computing, where dynamicity and
fault-tolerance are main issues. They tend to provide weak consistency
guarantees. Our work is on a different avenue.

Hazelcast [19] is an in-memory data grid middleware which offers
implementations for maps, queues, sets and lists from the Java concurrency
utilities interface. These implementations are optimized for fault tolerance,
so some form of replication is supported. Lists and sets are stored on a
single node, so they do not scale beyond the capacity of this node. The queue
stores all elements to the memory sequentially before flushing them to the
datastore. Like Hazelcast, GridGain [53], an in-memory data fabric which
connects applications with datastores, provides a distributed implementation
of queue from the Java concurrency utilities interface. The queue can be
either stored on a single grid node, or be distributed on different grid nodes
using the datastore that exists below GridGain. In a similar vein, Grappa [54]
is a software system that can provide distributed shared memory over a cluster
of machines. So-called delegate operations are used in order to access shared
memory, relieving the programmer of having to reason about remote or local
memory. However, Grappa does not provide the programmer with a data structure
library.

We extend some of the ideas from hierarchical lock implementations and other
synchronization protocols for NUMA cache-coherent machines [14, 15, 55] to get
hierarchical implementations for a non cache-coherent architecture. Tudor et
al. [56] attempt to identify patterns on search data structures, which favor
implementations that are portably scalable in cache-coherent machines. The
patterns they came up with cannot be used to automatically generate a
concurrent implementation from its sequential counterpart; they rather provide
hints on how to apply optimizations when designing such implementations.

##  3 Abstract Description of Hardware

Inspired by the characteristics of non cache-coherent architectures [2] and
prototypes [4], we consider an architecture which features $m$ islands (or
clusters), each comprised of $c$ cores (located in one or more processors).
The main memory is split into modules, with each module associated to a
distinct island (or core). A fast cache memory is located close to each core.
No hardware cache-coherence is provided among cores of different islands: this
means that different copies of the same variable residing on caches of
different islands may be inconsistent. The islands are interconnected with
fast communication channels.

The architecture may provide cache-coherence for the memory modules of an
island to processes executing on the cores of the island, i.e. the cores of
the same island may see the memory modules of the island as cache-coherent
shared memory. If this is so, we say that the architecture is partially cache-
coherent; otherwise, it is non cache-coherent. A process can send messages to
other processes by invoking send and it can receive messages from other
processes by invoking receive. The following means of communication between
cores (of the same or different islands) are provided:

Send/Receive mechanism: Each core has its own mailbox which is a FIFO queue
(implemented in hardware). (If more than one processes are executed on the
same core, they share the same hardware mailbox; in this case, the
functionality of send and receive can be provided to each process through the
use of software mailboxes.) A process executing on the core can send messages
to other processes by invoking send, and it can receive messages from other
processes by invoking receive. Messages are not lost and are delivered in FIFO
order. An invocation of receive blocks until the requested message arrives.
The first parameter of an invocation to send determines the core identifier to
which the message is sent.

Reads and Writes through DMA: A Direct Memory Access (DMA) engine allows
certain hardware subsystems to access the system’s memory without any
interference with the CPU. We assume that each core can perform Dma($A,B,d$)
to copy a memory chunk of size $d$ from memory address $A$ to memory address
$B$ using a DMA (where $A$ and $B$ may be addresses in a local or a remote
memory module). We remark that DMA is not executed atomically. It rather
consists of a sequence of atomic reads of smaller parts, e.g. one or a few
words, (known as bursts) of the memory chunk to be transferred, and atomic
writes of these small parts to the other memory module. DMA can be used for
performance optimization. Once the size of the memory chunk to be transferred
becomes larger (by a small multiplicative factor) than the maximum message
size supported by the architecture, it is more efficient to realize the
transfer using DMA (in comparison to sending messages). Specifically, we
denote by $MMS$ the maximum size of a message supported by the architecture.
(Usually, this size is equal to either a few words or a cache line). Consider
that the chunk of data that a core wants to send has size equal to $B$. To
send these data using messages, the core must send $\frac{B}{MMS}$ messages.
Each message has a cost $C_{M}$ to set it up. So, in total, to transfer the
data using messages, the overhead paid is $\frac{B}{MMS}*C_{M}$. Setting up a
DMA has a cost $C_{D}$, which in most architectures is by a small constant
factor larger than $C_{M}$. However, $C_{D}$ is paid only once for the entire
transfer of the chunk of data since it is done with a single DMA.
Additionally, sending and receiving $\frac{B}{MMS}$ messages requires that a
core’s CPU will be involved $\frac{B}{MMS}$ times to send each message and
another core’s CPU will be involved $\frac{B}{MMS}$ times to receive these
messages. This cost will be greatly avoided when using a single DMA to
transfer the entire chunk of data. Thus, it is beneficial in terms of
performance, to use DMA for transferring data whenever the size of the data to
be transferred is not too small.

##  4 Theoretical Framework

An implementation of a data structure (DS) stores its state in the memory
modules and provides an algorithm, for each process, to implement each
operation supported by the data structure. We model the submission and
delivery of messages sent by processes by including incoming and outgoing
message buffers in the state of each process (as described in standard books
[33, 57] on distributed computing).

We model each process as a state machine. We model a DMA request as a code
block which contains a sequence of interleaved burst reads from a memory
module and burst writes to a memory module. A DMA engine executes sequences of
DMA requests, so it can also be modeled as a simple state machine whose state
includes a buffer storing DMA requests that are to be executed. A
configuration is a vector describing the state of each process (including its
message buffers), the state of each DMA engine, the state of the caches (or
the shared variables in case shared memory is supported among the cores of
each island), and the states of the memory modules. In an initial
configuration, each process and DMA engine is in an initial state, the shared
variables and the memory modules are in initial states and all message and DMA
buffers are empty. An event can be either a step by some process, a step by a
DMA engine, or the delivery of a message; in one step, a process may either
transmit exactly one message to some process and at least one message to every
other process, or access (read or write) exactly one shared variable, or
initiate a DMA transfer, or invoke an operation of the implemented data
structure. In a DMA step a burst is read from or written to a memory module.
All steps of a process should follow the process’s algorithm. Similarly, all
steps of a DMA engine should be steps of the code block that performs a DMA
request submitted to this DMA engine.

An execution is an alternating sequence of configurations and events starting
with an initial configuration. The execution interval of an instance of an
operation $op$ that completes in an execution $\alpha$ is the subsequence of
$\alpha$ starting with the configuration preceding the invocation of this
instance of $op$ and ending with the configurations that follows its response.
If an instance of an operation $op$ does not complete in $\alpha$, then the
execution interval of $op$ is the suffix of $\alpha$ starting with the
configuration preceding the invocation of this instance of $op$. An execution
$\alpha$ imposes a partial order $\prec_{\alpha}$ on the instances of its
operations, such that for two instances $op_{1}$ and $op_{2}$ of some
operations in $\alpha$, $op_{1}\prec_{\alpha}op_{2}$ if the response of
$op_{1}$ precedes the invocation of $op_{2}$ in $\alpha$. If it neither holds
that $op_{1}\prec_{\alpha}op_{2}$ not that $op_{2}\prec_{\alpha}op_{1}$, then
we say that $op_{1}$ and $op_{2}$ are concurrent. If no two operation
instances in $\alpha$ are concurrent, then $\alpha$ is a sequential execution.

A step is enabled at a configuration $C$, if the process or DMA engine will
execute this step next time it will be scheduled. A finite execution $\alpha$
is fair if, for each process $p$ and each DMA engine $e$, no step by $p$ or
$e$ is enabled at the final configuration $C$ of $\alpha$ and all messages
sent in $\alpha$ have been delivered by $C$. An infinite execution $\alpha$ is
fair if the following hold:

  * •

for each process $p$, either $p$ takes infinitely many steps in $\alpha$, or
there are infinitely many configurations in $\alpha$ such that in each of them
(1) no step by $p$ is enabled, (2) for every prefix of $\alpha$ that ends at
such a configuration, all messages sent by $p$ have been delivered.

  * •

for each DMA engine $e$, either $e$ takes infinitely many steps in $\alpha$,
or there are infinitely many configurations in $\alpha$ such that in each of
them no step by $e$ is enabled (we remark that a DMA engine $e$ always have an
enabled step as long as its DMA buffer is not empty).

Correctness. For correctness, we consider linearizability [58]. This means
that, for every execution $\alpha$, there is a sequential execution $\sigma$,
which contains all the completed operations in $\alpha$ (and some of the
uncompleted ones) so that the response of each operation in $\sigma$ is the
same as in $\alpha$ and $\sigma$ respects the partial order of $\alpha$. In
such a linearizable execution $\alpha$, one can assign a linearization point
to each completed operation instance (and to some of the uncompleted ones) so
that the linearization point of each operation occurs after the invocation
event and before the response event the operation, and so that the order of
the linearization points is the same as the order of the operations in
$\sigma$.

Progress. We aim at designing algorithms that always terminate, i.e. reach a
state where all messages sent have been delivered and no step is enabled. We
do not cope with message or process failures.

Communication Complexity. Communication between the cores of the same island
is usually faster than that across islands. Thus, the communication complexity
of an algorithm for a non cache-coherent architecture is measured in two
different levels, namely the intra-island communication and the inter-island
communication. The inter-island communication complexity of an instance $inst$
of an operation $op$ in an execution $\alpha$ is the total number of messages
sent by every core $c$ to cores residing on different islands from that of $c$
for executing $inst$ in $\alpha$. The inter-island communication complexity of
$op$ in $\alpha$ is the maximum, over all instances $inst$ of $op$ in
$\alpha$, of the inter-island communication complexity of $inst$ in $\alpha$.
The inter-island communication complexity of $op$ for an implementation $I$ is
the maximum, over all executions $\alpha$ produced by $I$, of the inter-island
communication complexity of $op$ in $\alpha$. We remark that communication can
be measured in a more fine-grained way in terms of bytes transferred instead
of messages sent, as described in [57]. For simplicity, we focus on the higher
abstraction of measuring just the number of messages as described in [33].

If the architecture is non cache-coherent, then the intra-island communication
complexity is defined as follows. The intra-island communication complexity of
an instance $inst$ of $op$ in $\alpha$ is the maximum, over all islands, of
the total number of messages sent by every core $c$ of an island to cores
residing on the same island as $c$ for executing $inst$ in $\alpha$.

If the architecture is partially cache-coherent, then we measure the inter-
island communication complexity in terms of cache misses following the cache-
coherence (CC) shared-memory model (see e.g. [59, 60]). Specifically, in the
(CC) shared memory model, accesses to shared variables are performed via
cached copies of them; an access to a shared variable is a cache miss if the
cached copy of this variable is invalid. In this case, a cache miss occurs and
a valid copy of the variable should be fetched in the local cache first before
it can be accessed. Once the cache miss is served and as long as the variable
is not updated by processes that are being executed on other cores, future
accesses to the variable by processes that are being executed on this core do
not lead to further cache misses. In such a model, the inter-island
communication complexity of an instance $inst$ of an operation $op$ is the
maximum, over all islands, of the total number of cache-misses that the cores
of the island experience to execute $inst$.

We remark that independently of whether the architecture is partially or fully
non cache-coherent, the intra-island communication complexity of $op$ in
$\alpha$ is the maximum, over all instances $inst$ of $op$ in $\alpha$, of the
intra-island communication complexity of $inst$ in $\alpha$. Moreover, the
intra-island communication complexity of $op$ for an implementation $I$ is the
maximum, over all executions $\alpha$ produced by $I$, of the intra-island
communication complexity of $op$ in $\alpha$.

The DMA communication complexity of an instance $inst$ of an operation $op$,
is the total number of $DMA$ requests initiated by every process to execute
$inst$; in a more fine-grained model, we could instead measure the total
number of bursts performed by these DMA requests. The DMA communication
complexity of $op$ in $\alpha$ and of $op$ in $I$ are defined as for the other
types of communication complexities.

Time complexity. Consider a fair execution $\alpha$ of an implementation $I$.
A timed version of $\alpha$ is an enhanced version of $\alpha$ where each
event has been associated to a non-negative real number, the time at which
that event occurs. We define the delay of a message in a timed version of
$\alpha$ to be the time that elapses between the computation event that sends
the message and the event that delivers the message. We denote by ${\cal
T}_{\alpha}$ those timed versions of $\alpha$ for which the following
conditions hold: (1) the times must start at 0, (2) must be strictly
increasing for each individual process and the same must hold for each
individual DMA engine, (3) must increase without bound if the execution is
infinite, (4) the timestamps of two subsequent events by the same process (or
the same DMA engine) must differ by at most $1$, and (4) the delay of each
message sent must be no more than one time unit. Let ${\cal
T}=\cup_{\forall\alpha\mbox{ produced by }I}\\{{\cal T}_{\alpha}\\}$.

The time until some event $\rho$ is executed in an execution $\alpha$ is the
supremum of the times that can be assigned to $\rho$ in all timed versions of
$\alpha$ in ${\cal T}_{\alpha}$. The time between two events in $\alpha$ is
the supremum of the differences between the times in all timed versions of
$\alpha$ in ${\cal T}_{\alpha}$. The time complexity of an instance $inst$ of
an operation $op$ in $\alpha$ is the time between the events of its invocation
and its response. The time complexity of $op$ in $\alpha$ is the maximum, over
all instances $inst$ of $op$ in $\alpha$, of the time complexity of $inst$ in
$\alpha$. The time complexity of an operation $op$ for $I$ is the maximum,
over all executions $\alpha$ produced by $I$, of the time complexity of $op$
in $\alpha$.

Space Complexity. The space complexity of $I$ is determined by the memory
overhead introduced by $I$, and by the number and type of shared variables
employed (in case of partial non cache-coherence).

##  5 Directory-based Stacks, Queues, and Deques

The state of the data structure is stored in a highly-scalable distributed
directory whose data are spread over the local memory modules of the NS
servers. The directory supports the operations DirInsert, DirDelete,
BlockDirDelete, and DirSearch. DirDelete and BlockDirDelete both remove
elements from the directory; however, DirDelete returns $\bot$ if the
requested element is not contained in the directory, while BlockDirDelete
blocks until the element is found in the directory. To implement it, we employ
a simple highly-efficient distributed hash table implementation (also met in
[18, 19, 20]) where hash collisions are resolved by using hash chains
(buckets). Each server stores a number of buckets. For simplicity, we consider
a simple hash function which employs $\mod$ and works even if the key is a
negative integer. It returns an index which is used to find the server where a
request must be sent, and the appropriate bucket at this server, in which the
element resides (or must be stored).

To perform an operation, each client must first access a fetch&add object to
get a unique sequence number which it uses as the key for the requested data.
This object can be implemented using a designated server, called the
synchronizer and denoted by $s_{s}$. The client then communicates with the
appropriate server to complete its operation. The server locally processes the
request and responds to the process that initiated it. This approach suites
better to workloads where the state of the data structure is large.

The hash table implementation we use as our directory is presented in Section
5.1, for completeness. Similar hash table designs have been presented (or
discussed) in [18, 20, 19]. Section 5.2 presents the details of the directory-
based distributed stack. The directory-based queue implementation is discussed
in Section 5.3. Section 5.5 provides the directory-based deque. We remark that
our directory-based data structures would work even when using a different
directory implementation.

###  5.1 Distributed Hash Table

A hash table stores elements, each containing a key and a value (associated
with the key). Each server stores hash table elements to a local data
structure. This structure can be a smaller hash table or any other data
structure (array, list, tree, etc.) and supports the operations INSERT, SEARCH
and DELETE. To perform an operation on the DHT, a client $c$ finds the
appropriate server to submit its request by hashing the key value of interest.
Then, it sends a message to this server, which performs the operation locally
and sends back the result to $c$. A server $s$ processes all incoming messages
sequentially. After receiving a response message from the server, all client
functions return a boolean value depending on whether the operation was
successful or not.

###  5.2 Directory-Based Stack

Algorithm 1 Events triggered in the synchronizer of the directory-based stack. 1 |  int $top\\_key=-1$;
---|---
|
1 |  a message $\langle op,\ cid\rangle$ is received:
2 |  if ($op=={\tt PUSH}$)
3 |  $top\\_key++$;
4 |  send($cid$, $top\\_key$);
5 |  if ($op$ == POP) $\\{$
6 |  if ($top\\_key\neq-1$)
7 |  $top\\_key--$;
|  $\\}$

To implement a stack, the synchronizer $s_{s}$ maintains a variable $top$
which stores an integer counting the number of elements that are currently in
the stack.

To apply an operation op a client sends a message to the synchronizer $s_{s}$.
If op is a push operation, $s_{s}$ uses $top\\_key$ variable to assign unique
keys to the newly inserted data. Each time it receives a push request, $s_{s}$
sends the value stored in $top\\_key$ to the client after incrementing it by
one. Once a client receives a key from $s_{s}$ for the push operation it has
initiated, it inserts the new element in the directory by invoking DirInsert.
Similarly, if op is a pop operation, $s_{s}$ sends the value stored in
$top\\_key$ to the client and decrements it by one. The client then invokes
DirDelete repeatedly, until it successfully removes from the directory the
element with the received key. Notice that keys of elements are greater than
or equal to $0$ and therefore, $top\\_key$ has initial value $-1$, which
indicates that the stack is empty.

Event-driven pseudocode for the synchronizer is described in Algorithm 1 and
the code for the ClientPush() and ClientPop() operations, is presented in
Algorithms 2 and 3.

Algorithm 2 Push operation for a client of the directory-based stack. 8 |  void ClientPush(int $cid$, Data $data$) $\\{$
---|---
9 |  send($sid,\langle{\tt PUSH},cid\rangle$);
10 |  $key$ = receive(sid);
11 |  $status$ = DirInsert($key,data$);
12 |  return $status$;
|  $\\}$

Algorithm 3 Pop operation for a client of the directory-based stack. 13 |  Data ClientPop(int $cid$) $\\{$
---|---
14 |  send($sid,\langle{\tt POP},cid\rangle$);
15 |  $key$ = receive($sid$);
16 |  if ($key$ == $-1$) $status$ = $\bot$
17 |  else $\\{$
18 |  do $\\{$
19 |  $status$ = DirDelete($key$);
20 |  $\\}$ while ($status==\bot$);
|  $\\}$
21 |  return $status$;
|  $\\}$

The synchronizer receives, processes, and responds to clients’ messages. The
messages have an $op$ field that represents the operation to be performed
(PUSH or POP), and a $cid$ field with the client’s identification number,
needed for identifying the appropriate client to communicate with.

The ClientPop() function, presented in Algorithm 3 is analogous to the push
operation: it sends a POP message to $s_{s}$ and waits for its response (line
ln:104). Using the key that was received as argument, DirDelete() is
repeatedly called (line ln:100). This is necessary since another client
responsible for inserting the $key$ may not have finished yet its insertion.
In this case DirDelete returns $\bot$ (line ln:101). However, since the $key$
was generated previously by $s_{s}$, it is certain that it will be eventually
inserted into the directory service.

####  5.2.1 Proof of Correctness

Let $\alpha$ be an execution of the directory-based stack implementation. We
assign linearization points to push and pop operations in $\alpha$ by placing
the linearization point of an operation $op$ in the configuration resulting
from the execution of line ln:96 by the synchronizer for $op$.

Let $op$ be a push or a pop operation invoked by a client $c$ in $\alpha$ and
assume that the synchronizer executes line ln:96 for it. By inspection of the
pseudocode, we have that this line is executed after the synchronizer receives
a message by $c$ (line ln:90.1) and before $c$ receives the synchronizer’s
response (line ln:103.1 for a push operation, line ln:104 for a pop
operation). By the way the linearization points are assigned, we have the
following lemma.

######  Lemma 1.

The linearization point of a push (pop) operation $op$ is placed within its
execution interval.

Denote by $L$ the sequence of operations (which have been assigned
linearization points) in the order determined by their linearization points.
Let $C_{i}$ be the configuration in which the $i$-th operation $op_{i}$ of $L$
is linearized. Denote by $\alpha_{i}$, the prefix of $\alpha$ which ends with
$C_{i}$ and let $L_{i}$ be the prefix of $L$ up until the operation that is
linearized at $C_{i}$. We denote by $top_{i}$ the value of the local variable
$top\\_key$ of $s_{s}$ at configuration $C_{i}$; Let $C_{0}$ be the initial
configuration an let $top_{0}=-1$.

Notice that since only $s_{s}$ executes Algorithm 1, we have the following.

######  Observation 2.

Instances of Algorithm 1 are executed sequentially, i.e. their execution does
not overlap.

By the way linearization points are assigned, further inspection of the
pseudocode in conjunction with Observation 2 leads to the following.

######  Observation 3.

For each integer $i\geq 1$, the following hold at $C_{i}$: Let $op_{i}$ and
$op_{i+1}$ be two operations in $L$.

  * •

If $op_{i}$ is a push operation and $op_{i+1}$ is a push operation, then
$top_{i+1}=top_{i}+1$.

  * •

If $op_{i}$ is a push operation and $op_{i+1}$ is a pop operation, then
$top_{i+1}=top_{i}$.

  * •

If $op_{i}$ is a pop operation and $op_{i+1}$ is a pop operation, then, if
$top_{i}\neq-1$, $top_{i+1}=top_{i}-1$.

  * •

If $op_{i}$ is a pop operation and $op_{i+1}$ is a push operation, then, if
$top_{i}\neq-1$, $top_{i+1}=top_{i}$.

Let $\sigma$ be the sequential execution that results by executing the
operations in $L$ sequentially, in the order of their linearization points,
starting from an initial configuration in which the queue is empty. Let
$\sigma_{i}$ be the prefix of $\sigma$ that contains the operations in
$L_{i}$. Denote by $S_{i}$ the state of the sequential stack that results if
the operations of $L_{i}$ are applied sequentially to an initially empty
stack. Denote by $d_{i}$ the number of elements in $S_{i}$. We associate a
sequence number with each stack element such that the elements from the
bottommost to the topmost are assigned $0,\ldots,d_{i}-1$, respectively.
Denote by $sl_{d_{i}}$ the $d_{i}$-th element of $S_{i}$.

Let $L^{\prime}_{i}$ be the projection of $L_{i}$ that contains all operations
in $L_{i}$ except those pop operations that return $\bot$. Denote those
operations by $op^{\prime}_{i}$. Denote by $C^{\prime}_{i}$ the configuration
in which the $i$-th operation of $L^{\prime}_{i}$ is linearized. Let
$S^{\prime}_{i}$ be the state of the sequential stack after the operations of
$L^{\prime}_{i}$ have been applied to it, assuming an initially empty stack
and denote by $d^{\prime}_{i}$ the number of elements in $S^{\prime}_{i}$.
Again we associate a sequence number with each stack element such that the
elements from the bottommost to the topmost are assigned
$0,\ldots,d^{\prime}_{i}-1$, respectively. Denote by $sl_{d^{\prime}_{i}}$ the
$d^{\prime}_{i}$-th element of $S^{\prime}_{i}$. We denote by
$top^{\prime}_{i}$ the value of the local variable $top\\_key$ of $s_{s}$ at
configuration $C^{\prime}_{i}$. Let $k_{i}$ be the number of pop operations in
$L^{\prime}_{i}$.

By inspection of the pseudocode, it follows that:

######  Observation 4.

If $op_{i}$ is a push operation, it inserts a pair $\langle key,data\rangle$
in the directory, where $data$ is the argument of ClientPush executed for
$op_{i}$, and $key=top_{i}$. If $op_{i}$ is a pop operation then, if
$top_{i}\neq-1$, it removes a pair $\langle key,data\rangle$ with
$key=top_{i-1}$ from the directory and returns $data$; if $top_{i}=-1$, it
does not remove any pair from the directory and returns $\bot$.

######  Lemma 5.

For each integer $i>0$, it holds that:

  * •

If $op^{\prime}_{i}$ is a push operation, then it inserts element
$d^{\prime}_{i}$ into the stack and $top^{\prime}_{i}=d^{\prime}_{i}-1$.

  * •

If $op^{\prime}_{i}$ is a pop operation, then it removes element
$d^{\prime}_{i-1}$ from the stack, $top^{\prime}_{i}=d^{\prime}_{i-1}-1$ and
$top^{\prime}_{i}$ is equal to the value of $top\\_key$ of $s_{s}$ for the
${i-2*k_{i}+1}$-th push operation in $L^{\prime}_{i}$ .

###### Proof.

We prove the claim by induction on $i$.

Base case. We prove the claim for $i=1$. Recall that $S^{\prime}_{0}=\epsilon$
and $top^{\prime}_{0}=-1$. By definition of $L^{\prime}_{i}$,
$op^{\prime}_{1}$ is a push operation. By observation of the pseudocode (line
ln:92) we have that $top^{\prime}_{1}=-1+1=0$ and $op^{\prime}_{1}$ inserts an
element with sequence number $d^{\prime}_{1}-1=0$ into the stack. Thus, the
claim holds.

Hypothesis. Fix any $i$, $i>0$, and assume that the claim holds for
$C^{\prime}_{i}$.

Induction step. We prove that the claim also holds at $C^{\prime}_{i+1}$.
First, consider the case where $op^{\prime}_{i+1}$ is a push operation. We
distinguish two cases. Case (i): $op^{\prime}_{i}$ is a push operation, as
well. For $op^{\prime}_{i}$, the induction hypothesis holds. Therefore,
$op^{\prime}_{i}$ inserts the $d^{\prime}_{i}$-th element into the stack and
$top^{\prime}_{i}=d^{\prime}_{i}-1$. By Observation 3,
$top^{\prime}_{i+1}=top^{\prime}_{i}+1$. Since $S^{\prime}_{i}$ has
$d^{\prime}_{i}$ elements, $op^{\prime}_{i+1}$ inserts element
$d^{\prime}_{i+1}=d^{\prime}_{i}+1$, with sequence number
$d^{\prime}_{i+1}-1=(d^{\prime}_{i}+1)-1=d^{\prime}_{i}=top^{\prime}_{i}+1=top^{\prime}_{i+1}$
and the claim holds. Case (ii): $op^{\prime}_{i}$ is a pop operation, which
removes an element from the stack. Since the induction hypothesis holds,
$top^{\prime}_{i}=d^{\prime}_{i-1}-1$. Conversely, $op^{\prime}_{i+1}$ inserts
an element into the stack. By Observation 3, we have that
$top^{\prime}_{i+1}=top^{\prime}_{i}$ and the claim holds.

∎

From the above lemmas we have the following.

######  Theorem 6.

The directory-based distributed stack implementation is linearizable.

###  5.3 Directory-Based Queue

Algorithm 4 Events triggered in the synchronizer of the directory-based queue. 1 |  int $head\\_key=0,tail\\_key=0$;
---|---
|
2 |  a message $\langle op,cid\rangle$ is received:
3 |  if ($op$ == ENQ) $\\{$
4 |  $tail\\_key$++;
5 |  send($cid,tail\\_key$);
6 |  $\\}$ else if ($op$ == DEQ) $\\{$
7 |  if ($head\\_key<tail\\_key$) $\\{$
8 |  $head\\_key$++;
9 |  send($cid,head\\_key$);
10 |  $\\}$ else
11 |  send($cid,{\tt NACK}$);
|  $\\}$
|  $\\}$

The directory-based distributed queue is implemented in a way similar to the
directory-based stack implementation. To implement a queue, the synchronizer
$s_{s}$ maintains two counters, $head\\_key$ and $tail\\_key$, which store the
key associated with the first and the last, respectively, element in the
queue.

In order to perform an enqueue or dequeue operation, a client calls
ClientEnqueue() or ClientDequeue(), respectively (Algorithms 5 and 6,
respectively). To apply an operation $op$, a client sends a request to
$s_{s}$, in order to receive the key of the element to be inserted or deleted.
The client then calls DirInsert to insert the new element in the directory
(line ln:118). Each time $s_{s}$ receives an enqueue request, it increments
$tail\\_key$ and then sends the value stored in $tail\\_key$ to the client.

Each time $s_{s}$ receives a dequeue request, if $head\\_key\neq tail\\_key$,
then $s_{s}$ sends the value of $head\\_key$ to the client and increments
$head\\_key$ to store the key of the next element in the queue. The client
then uses this value as the key of the element to remove from the directory
(line ln:127). Otherwise, in case $head\\_key=tail\\_key$, $s_{s}$ sends NACK
to $c$ without changing $head\\_key$.

A dequeue operation for which $s_{s}$ sends a key value to the client by
executing line ln:122, is referred to as a successful dequeue operation. On
the other hand, a dequeue operation for which $s_{s}$ sends NACK to the client
by executing line ln:120, and for which in turn, the client returns $\bot$, is
referred to as an unsuccessul dequeue operation.

Algorithm 5 Enqueue operation for a client of the directory-based queue. 12 |  void ClientEnqueue(int $cid$, Data $data$) $\\{$
---|---
13 |  $sid$ = get the server id;
14 |  send($sid,\langle{\tt ENQ},cid\rangle$);
15 |  $tail\\_key$ = receive($sid$);
16 |  DirInsert($tail\\_key,data$);
|  $\\}$

Algorithm 6 Dequeue operation for a client of the directory-based queue. 17 |  Data ClientDequeue(int $cid$) $\\{$
---|---
18 |  $sid$ = get the server id;
19 |  send($sid,\langle{\tt DEQ},cid\rangle$);
20 |  $head\\_key$ = receive($sid$);
21 |  if($head\\_key=={\tt NACK}$)
22 |  return $\bot$;
23 |  $data$ = BlockDirDelete($head\\_key$);
24 |  return $data$;
|  $\\}$

####  5.3.1 Proof of Correctness

Let $\alpha$ be an execution of the directory-based queue implementation. We
assign linearization points to enqueue and dequeue operations in $\alpha$ as
follows: The linearization point of an enqueue operation $op$ is placed in the
configuration resulting from the execution of line ln:118 for $op$ by $s_{s}$.
The linearization point of a dequeue operation $op$ is placed in the
configuration resulting from the execution of either line ln:122 or line
ln:120 for $op$ (whichever is executed) by $s_{s}$.

######  Lemma 7.

The linearization point of an enqueue (dequeue) operation $op$ is placed
within its execution interval.

###### Proof.

Assume that $op$ is an enqueue operation and let $c$ be the client that
invokes it. The linearization point of $op$ is placed at the configuration
resulting from the execution of line ln:118 for $op$ by $s_{s}$. This line is
executed after the request by $c$ is received, i.e. after $c$ invokes
ClientEnqueue. Furthermore, it is executed before $c$ receives the response by
the server and thus, before ClientEnqueue returns. Therefore, the
linearization point is included in the execution interval of enqueue.

The argument regarding dequeue operations is similar. ∎

Denote by $L$ the sequence of operations which have been assigned
linearization points in $\alpha$ in the order determined by their
linearization points. Let $C_{i}$ be the configuration in which the $i$-th
operation $op_{i}$ of $L$ is linearized; denote by $C_{0}$ the initial
configuration. Denote by $\alpha_{i}$, the prefix of $\alpha$ which ends with
$C_{i}$ and let $L_{i}$ be the prefix of $L$ up until the operation that is
linearized at $C_{i}$. We denote by $head_{i}$ the value of the local variable
$head\\_key$ of $s_{s}$ at configuration $C_{i}$, and by $tail_{i}$ the value
of the local variable $tail\\_key$ of $s_{s}$ at $C_{i}$. By the pseudocode,
we have that the initial values of $tail\\_key$ and $head\\_key$ are $0$;
therefore, we consider that $head_{0}=tail_{0}=0$.

Notice that since only $s_{s}$ executes Algorithm 4, we have the following.

######  Observation 8.

Instances of Algorithm 4 are executed sequentially by $s_{s}$, i.e. their
execution does not overlap.

By inspection of Algorithm 4, we have that for some instance of it, either
lines ln:116 - ln:117, or lines ln:119 - ln:122, or lines ln:120.1 - ln:120
are executed, where either $tail\\_key$ or $head\\_key$ is incremented. Then,
by the way linearization points are assigned, and by Observation 8, we have
the following.

######  Observation 9.

Given two configurations $C_{i}$, $C_{i+1}$, $i\geq 0$, in $\alpha$, there is
at most one step in the execution interval between $C_{i}$ and $C_{i+1}$ that
modifies either $head\\_key$ or $tail\\_key$.

More specifically, regarding the values of $head_{i}$ and $tail_{i}$, we
obtain the following lemma.

######  Lemma 10.

For each integer $i\geq 1$, the following hold at $C_{i}$:

  1. 1.

If $op_{i}$ is an enqueue operation, then $tail_{i}=tail_{i-1}+1$ and
$head_{i}=head_{i-1}$.

  2. 2.

If $op_{i}$ is a dequeue operation and $head_{i-1}\neq tail_{i-1}$, then
$head_{i}=head_{i-1}+1$ and $tail_{i}=tail_{i-1}$; otherwise
$head_{i}=head_{i-1}$ and $tail_{i}=tail_{i-1}$.

  3. 3.

$head_{i}\leq tail_{i}$.

###### Proof.

We prove the claims by induction.

Base case. We prove the claims for $i=1$. Assume first that $op_{1}$ is an
enqueue operation. Then, the linearization point of $op_{1}$ is placed in the
configuration resulting from the execution of line ln:118. By inspection of
the pseudocode, we have that $tail\\_key$ is incremented by $s_{s}$ between
$C_{0}$ and $C_{1}$, before the linearization point of $op_{1}$. Notice also
that because of Observation 8 no process other than $s_{s}$ modifies neither
$tail\\_key$ nor $head\\_key$ between $C_{0}$ and $C_{1}$. Thus,
$tail_{1}=tail_{0}+1$. The value of $head\\_key$ is not modified by enqueue
operations (lines ln:116 - ln:117), therefore $head_{1}=head_{0}$. Thus, claim
1 holds.

Next, assume that $op_{1}$ is a dequeue operation. Then, the linearization
point of $op_{1}$ may be placed at the configuration resulting from the
execution of line ln:120 or line ln:122, whichever is executed by $s_{s}$ for
it. By inspection of the pseudocode (line ln:119), line ln:120 is executed
only in case $head_{0}<tail_{0}$. Since $head_{0}=tail_{0}=0$, line ln:120 is
not executed and $op_{1}$ is linearized at the configuration resulting from
the execution of line ln:122. By the pseudocode, line ln:121 and by
Observation 8, $head\\_key$ is incremented by $1$ in the execution step
preceding the linearization point of $op_{1}$, i.e. between configurations
$C_{0}$ and $C_{1}$. Thus, $head_{1}=head_{0}+1$. The value of $tail\\_key$ is
not modified by dequeue operations (lines ln:119 - ln:121), therefore
$tail_{1}=tail_{0}$. By the above, claim 2 also holds.

From the previous reasoning, we have that in case $op_{1}$ is an enqueue
operation, then $tail_{1}=1$ and $head_{1}=0$, while if $op_{1}$ is a dequeue
operation, $tail_{1}=0$ and $head_{1}=0$. In either case, $head_{1}\leq
tail_{1}$, thus claim 3 also holds.

Hypothesis. Fix any $i$, $i\geq 1$, and assume that the claims hold for $i-1$.

Induction Step. We prove that the claims also hold for $i$. First, assume that
$op_{i}$ is an enqueue operation. Then, the linearization point of $op_{i}$ is
placed in the configuration resulting from the execution of line ln:118. By
inspection of the pseudocode, we have that $tail\\_key$ is incremented by
$s_{s}$ between $C_{i-1}$ and $C_{i}$, before the linearization point of
$op_{i}$. Notice also that because of Observation 8 no process other than
$s_{s}$ modifies neither $tail\\_key$ nor $head\\_key$ between $C_{i-1}$ and
$C_{i}$. Thus, $tail_{i}=tail_{i-1}+1$. The value of $head\\_key$ is not
modified by enqueue operations (lines ln:116 - ln:117), therefore
$head_{i}=head_{i-1}$. Thus, claim 1 holds.

Next, assume that $op_{i}$ is a dequeue operation. Then, the linearization
point of $op_{i}$ may be placed at the configuration resulting from the
execution of line ln:120 or line ln:122, whichever is executed by $s_{s}$ for
it. Let $op_{i}$ be linearized at the execution of line ln:120. By the
induction hypothesis, $head_{i-1}\leq tail_{i-1}$. By inspection of the
pseudocode (line ln:119), line ln:120 is executed only in the case that
$head_{i-1}=tail_{i-1}$. By inspection of the pseudocode (lines ln:119 -
ln:120) and by Observation 8, it follows that in this case $head\\_key$ is not
modified in the execution interval between $C_{i-1}$ and $C_{i}$. Therefore,
$head_{i}=head_{i-1}$. Since a dequeue operation does not modify $tail\\_key$,
it also holds that $tail_{i}=tail_{i-1}$. Finally, let $op_{i}$ be linearized
at the execution of line ln:122. In this case, by the induction hypothesis and
reasoning as previously, $head_{i-1}\neq tail_{i-1}$. By the pseudocode, line
ln:121 and by Observation 8, $head\\_key$ is incremented by $1$ in the
computation step preceding the linearization point of $op_{i}$, i.e. between
configurations $C_{i-1}$ and $C_{i}$. Thus, $head_{i}=head_{i-1}+1$. The value
of $tail\\_key$ is not modified by dequeue operations (lines ln:119 - ln:121),
therefore $tail_{i}=tail_{i-1}$. By the above, claim 2 also holds.

By the induction hypothesis, we have that $head_{i-1}\leq tail_{i-1}$. From
the previous reasoning, we have that in case $op_{i}$ is an enqueue operation,
then $tail_{i}=tail_{i-1}+1$ and $head_{i}=head_{i-1}$. It follows that
$head_{i}\leq tail_{i}$. On the other hand, if $op_{i}$ is a dequeue
operation, $tail_{i}=tail_{i-1}$ and $head_{i}=head_{i-1}$ in case
$head_{i-1}=tail_{i-1}$. Otherwise, in case $head_{i-1}<tail_{i-1}$, then
$tail_{i}=tail_{i-1}$ and $head_{i}=head_{i-1}+1$. Since
$head_{i-1}<tail_{i-1}$, and since both $head\\_key$ and $tail\\_key$ are both
incremented in steps of $1$, it follows that $head_{i}\leq tail_{i}$. In
either of the previous cases, claim 3 also holds. ∎

Let $\sigma$ be the sequential execution that results by executing the
operations in $L$ sequentially, in the order of their linearization points,
starting from an initial configuration in which the queue is empty. Let
$\sigma_{i}$ be the prefix of $\sigma$ that contains the operations in
$L_{i}$. Let $Q_{i}$ be the state of the queue after the operations of $L_{i}$
have been applied to an empty queue sequentially. Let the size of $Q_{i}$
(i.e. the number of elements contained in $Q_{i}$) be $d_{i}$. Denote by
$sl_{i}^{j}$ the $j$-th element of $Q_{i}$, $1\leq j\leq d_{i}$. Consider a
sequence of elements $S$. If $e$ is the first element of $S$, we denote by
$S\setminus e$ the suffix of $S$ that results by removing only element $e$
from the first position of $S$. We further denote by $S^{\prime}=S\cdot e$ the
sequence that results by appending some element $e$ to the end of $S$.

By inspection of the pseudocode, it follows that:

######  Observation 11.

If $op_{i}$ is an enqueue operation, it inserts a pair $\langle
data,key\rangle$ in the directory, where $data$ is the argument of
ClientEnqueue executed for $op_{i}$, and $key=tail_{i}$. If $op_{i}$ is a
dequeue operation then, if $head_{i}\neq tail_{i}$, it removes a pair $\langle
data,key\rangle$ with $key=head_{i}$ from the directory and returns $data$; if
$head_{i}=tail_{i}$, it does not remove any pair from the directory and
returns $\bot$.

######  Lemma 12.

For each $i$, let $m_{i}$ be the number of enqueue operations in $L_{i}$ and
$k_{i}$ be the number of successful dequeue operations in $L_{i}$. Then:

  1. 1.

$Q_{i}$ contains the elements inserted by the $m_{i}-k_{i}$ last enqueue
operations in $L_{i}$, in order,

  2. 2.

$tail_{i}=m_{i}$,

  3. 3.

$head_{i}=k_{i}$,

  4. 4.

if $op_{i}$ is a dequeue operation, then it returns the same response in
$\alpha$ and $\sigma_{i}$. If $op_{i}$ is a successful dequeue operation that
removes the pair $\langle data,-\rangle$, from the directory, then its
response is the data inserted to the queue by the $k_{i}$-th enqueue operation
in $L_{i}$, whereas if $op_{i}$ is unsuccessful, then it returns $\bot$.

###### Proof.

We prove the claims by induction.

Base case. We prove the claim for $i$ = $1$. First, assume that $op_{1}$ is an
enqueue operation. Then, $m_{1}=1$ and $k_{1}=0$, and $Q_{1}$ contains a
single element, namely the element inserted by the $(m_{1}-k_{1})$-th enqueue
operation in $L_{1}$, which is $op_{1}$, thus claim 1 holds. By Lemma 10, we
have that at $C_{1}$, $tail_{1}=tail_{0}+1=1=m_{1}$, and
$head_{1}=head_{0}=0=k_{1}$. Thus, claims 2 and 3 also hold. Claim 4 holds
trivially.

Next, assume that $op_{1}$ is a dequeue operation. Thus, $m_{1}=0$. By
inspection of the pseudocode, $head_{0}=tail_{0}=0$. By the way linearization
points are assigned and by Observation 9, $op_{1}$ is the operation for which
the code of $s_{s}$ is executed for the first time. Thus, line ln:120 is
executed and $op_{1}$ is unsuccessful. Therefore, $k_{1}=0$. By Lemma 10,
$head_{1}=0$ and $tail_{1}=0$. It follows that $head_{1}=m_{1}$ and
$tail_{1}=k_{1}$. Thus, claims 2 and 3 hold.

Since $op_{1}$ is the first operation in $\sigma$ and since it is a dequeue
operation, it is an unsuccessful dequeue operation in $\sigma$. Since $Q_{0}$
is empty, it follows that $Q_{1}=\emptyset$, so claim 1 follows. By inspection
of the pseudocode, $op_{1}$ returns $\bot$ in $\alpha$. Since $op_{1}$ is an
unsuccessful dequeue in $\sigma$, it also returns $\bot$ in $\sigma$. Thus,
claim 4 also holds.

Hypothesis. Fix any $i$, $i>0$ and assume that the claims hold for $i-1$.

Induction step. We prove that the claims also hold for $i$. First, assume that
$op_{i}$ is an enqueue operation and let the $data$ argument of ClientEnqueue
for $op_{i}$ be $e$. By the induction hypothesis, $Q_{i-1}$ contains the
elements inserted by the $m_{i-1}-k_{i-1}$ last enqueue operations in
$L_{i-1}$, in order. Since $op_{i}$ is an enqueue operation, it follows that
$Q_{i}=Q_{i-1}\cdot e$, $m_{i}=m_{i-1}+1$, and claim 1 holds. Moreover,
$k_{i}=k_{i-1}$. By Lemma 10, we have that $tail_{i}=tail_{i-1}+1$ and that
$head_{i}=head_{i-1}$. By the induction hypothesis, $tail_{i-1}=m_{i-1}$ and
$head_{i}=k_{i-1}$. It follows that $tail_{i}=m_{i-1}+1=m_{i}$ and that
$head_{i}=head_{i-1}=k_{i-1}=k_{i}$. Thus, claims 2 and 3 also hold. Claim 4
holds trivially.

Now let $op_{i}$ be a dequeue operation. First, assume that $op_{i}$ is a
successful dequeue operation, i.e. $s_{s}$ executes line ln:122 for $op_{i}$.
By inspection of the pseudocode, by Observation 9 and the way linearization
points are assigned, it follows that when line ln:119 is executed,
$head\\_key$ and $tail\\_key$ have the values $head_{i-1}$ and $tail_{i-1}$
respectively. Since line ln:122 is executed, it follows that
$head_{i-1}<tail_{i-1}$. By the induction hypothesis, $head_{i-1}=k_{i-1}$ and
$tail_{i-1}=m_{i-1}$. Since $op_{i}$ is a dequeue operation, $m_{i}=m_{i-1}$
and $k_{i}=k_{i-1}+1$. By Lemma 10, we have that $tail_{i}=tail_{i-1}$ and
that $head_{i}=head_{i-1}+1$. So, $tail_{i}=m_{i}$ and $head_{i}=k_{i}$. Thus,
claims 2 and 3 hold.

By the induction hypothesis, $Q_{i-1}$ contains the elements inserted by the
$m_{i-1}-k_{i-1}$ last enqueue operations in $L_{i-1}$. Since
$m_{i-1}-k_{i-1}=m_{i-1}-(k_{i}-1)$, $Q_{i-1}$ contains $m_{i-1}-k_{i}+1$
elements. Since $op_{i}$ is a dequeue, it removes the first element of
$Q_{i-1}$, so $Q_{i}$ contains $m_{i}-k_{i}$ elements, and claim 1 follows.

Recall that $head_{i-1}<tail_{i-1}$. By the induction hypothesis (claims 2 and
3), it follows that $k_{i-1}<m_{i-1}$. Thus, $Q_{i-1}$ is not empty and
$op_{i}$ is a successful dequeue operation also in $\sigma$.

By the induction hypothesis, $Q_{i-1}$ contains the elements inserted by the
$m_{i-1}-k_{i-1}=m_{i}-(k_{i}-1)=m_{i}-k_{i}+1$ last enqueue operations in
$L_{i-1}$, in ascending order from head to tail. Since $m_{i}$ is the total
number of successful enqueue operations in $L_{i}$ and $k_{i}$ the total
number of successful dequeue operations, this means that in $\sigma$, $op_{i}$
removes the element inserted to the queue by the $k_{i}$-th enqueue operation.
By inspection of the pseudocode, the client removes the key with value
$head_{i}$ from the directory and returns the data that are associated with
this key. Since $head_{i}=k_{i}$, $op_{i}$ returns the data from a $\langle
data,key\rangle$ pair it removes from the directory. By inspection of the
pseudocode, the key used to remove the data has the value $head_{i}$.
Therefore, also in $\alpha$, $op_{i}$ returns the data associated with the
$k_{i}$-th enqueue operation in $L_{i}$, and claim 4 holds.

Assume now that $op_{i}$ is an unsuccessful dequeue operation, i.e. $s_{s}$
executes line ln:120 for $op_{i}$. By inspection of the pseudocode, by
Observation 9 and the way linearization points are assigned, it follows that
when line ln:119 is executed, $head\\_key$ and $tail\\_key$ have the values
$head_{i-1}$ and $tail_{i-1}$ respectively. Since line ln:120 is executed, it
follows that $head_{i-1}=tail_{i-1}$. By the induction hypothesis,
$head_{i-1}=k_{i-1}$ and $tail_{i-1}=m_{i-1}$. Since $op_{i}$ is an
unsuccessful dequeue operation, $m_{i}=m_{i-1}$ and $k_{i}=k_{i-1}$. By Lemma
10, we have that in this case, $tail_{i}=tail_{i-1}$ and that
$head_{i}=head_{i-1}$. So, $tail_{i}=m_{i}$ and $head_{i}=k_{i}$. Thus, claims
2 and 3 hold. Furthermore, since $head_{i-1}=tail_{i-1}$, it follows that
$m_{i-1}=k_{i-1}$, which means that $Q_{i-1}$ is empty, and thus, $op_{i}$ is
unsuccessful in $\sigma$. As $m_{i}=m_{i-1}$ and $k_{i}=k_{i-1}$ and $op_{i}$
is unsuccessful, claim 1 holds. Since $op_{i}$ is unsuccessful in $\alpha$, it
removes no $\langle data,key\rangle$ pair from the directory and returns
$\bot$. Thus, claim 4 also holds. ∎

From the above lemmas we have the following:

######  Theorem 13.

The directory-based queue implementation is linearizable.

###  5.4 Queues with Special Functionality

Synchronous queue. A synchronous queue $Q_{S}$ is an implementation of the
queue data type. Instead of storing elements, a synchronous queue matches
instances of $Dequeue()$ with instances of $Enqueue()$ operations. Thus, if
$op_{e}$ is an instance of an $Enqueue(x,Q_{S})$ operation and $op_{d}$ an
instance of a $Dequeue(Q_{S})$ such that $op_{d}$ returns the element $x$
enqueued by $op_{e}$, then a synchronous queue ensures that the execution
intervals of $op_{e}$ and $op_{d}$ are overlapping.

In order to derive a distributed synchronous queue from the directory-based
queue proposed here, $s_{s}$ must respond to a dequeue request with the value
of $head$ and increment $head$, even if $head=tail$. Moreover, $s_{s}$ must
use a local queue to store active enqueue requests together with the keys it
has assigned to them (notice that there can be no more such requests that the
number of clients); $s_{s}$ must send the key $k$ for each such enqueue
request to the client that initiated it, at the time that $head$ becomes equal
to $k$. In this way, the execution interval of an enqueue operation for
element $e$ overlaps that of the dequeue operation which gets $e$ as a
response, as specified by the semantics of a synchronous queue.

Delay queue. A delay queue $Q_{D}$ implements the queue abstract data type.
Each element $e$ of a delay queue is associated with a delay value $t_{e}$
that represents the time that $e$ must remain in the queue before it can be
removed from it. Thus, an $Enqueue(e,t_{e},Q_{D})$ inserts an element $e$ with
time-out value $t_{e}$ to $Q_{S}$. $Dequeue(Q_{D})$ returns the element $e$
residing at the head of $Q_{D}$ if $t_{e}$ has expired and blocks (or performs
spinning) if this is not the case. Notice that this implementation can easily
be provided by associating each element inserted in the directory with a time-
out value. We also have to change the way that the directory works so that it
takes into consideration the delay of each element before removing it.

###  5.5 Directory-Based Double-Ended Queue (Deque)

The implementation of the directory-based deque follows similar principles as
the stack and queue implementations. In order to implement a deque, $s_{s}$
also maintains two counters, $head$ and $tail$, which store the key associated
with the first and the last, respectively, element in the deque. However, in
this case, counters $head$ and $tail$ may store negative integers and are
incremented or decremented based on the operation to be performed.

####  5.5.1 Algorithm Description

Event-driven pseudocode for the synchronizer $s_{s}$ is presented in Algorithm
7; $s_{s}$ now performs a combination of actions presented for the
synchronizers of the stack and the queue implementations (Algorithms 1 and 4).

The synchronizer $s_{s}$ has two counters, $head\\_key$ and $tail\\_key$ (line
ln:alg-dirdeq-1), that store the key associated with the first and the last,
respectively, element in the deque. The $head\\_key$ is modified when
operations targeting the front are received by $s_{s}$ and the $tail\\_key$ is
modified when operations targeting the back are received by $s_{s}$. Because
each endpoint of a deque behaves as a stack, the actions for enqueuing and
dequeuing are similar as in Algorithm 1.

Algorithm 7 Events triggered in the synchronizer of the directory-based deque. 1 |  int $head\\_key=0$, $tail\\_key=0$;
---|---
|
2 |  a message $\langle op,\ cid\rangle$ is received:
3 |  switch ($op$) $\\{$
4 |  case ENQ_T:
5 |  $tail\\_key++$;
6 |  send($cid$, $tail\\_key$);
7 |  break;
8 |  case DEQ_T:
9 |  if ($tail\\_key==head\\_key$) $\\{$
10 |  send($cid$, NACK);
11 |  $\\}$ else $\\{$
12 |  do $\\{$
13 |  $status$ = DirDelete($tail\\_key$);
14 |  $\\}$ while ($status==\bot$);
15 |  $tail\\_key--$;
16 |  send($cid$, $status$);
|  $\\}$
17 |  break;
18 |  case ENQ_H:
19 |  send($cid$, $head\\_key$);
20 |  $head\\_key--$;
21 |  break;
22 |  case DEQ_H:
23 |  if ($tail\\_key==head\\_key$) $\\{$
24 |  send($cid$, NACK);
25 |  $\\}$ else $\\{$
26 |  $head\\_key++$;
27 |  do $\\{$
28 |  $status$ = DirDelete($head\\_key$);
29 |  $\\}$ while ($status==\bot$);
30 |  send($cid$, $status$);
31 |  $\\}$
32 |  break;
|  $\\}$

Upon a message receipt, if $s_{s}$ receives a request ENQ_T (line ln:alg-
dirdeq-4) it increments $tail\\_key$ by one (line ln:alg-dirdeq-5), and then
sends the current value of $tail\\_key$ to the client (line ln:alg-dirdeq-6).
The client uses the value that $s_{s}$ sends to it, as the key for the data to
insert in the directory. Likewise, if $s_{s}$ receives a request ENQ_H (line
ln:alg-dirdeq-14), it sends the current value of $head\\_key$ to the client
(line ln:alg-dirdeq-16), and then decrements $head\\_key$ by one (line ln:alg-
dirdeq-15).

When a message of type DEQ_T arrives (line ln:alg-dirdeq-7), $s_{s}$ first
checks whether the deque is empty (line ln:alg-dirdeq-8). If this is so,
$s_{s}$ sends a NACK to the client (line ln:alg-dirdeq-9). Otherwise, the
synchronizer repeatedly calls DirDelete($tail\\_key$) to remove the element
corresponding to a key equal to the value of $tail\\_key$ from the directory
(line ln:alg-dirdeq-12), and then decrements $tail\\_key$ (line ln:alg-
dirdeq-10). Finally, $s_{s}$ sends the data to the client (line ln:alg-
dirdeq-13). The synchronizer performs similar actions for a DEQ_H message, but
instead of decrementing the $tail\\_key$, it increments the $head\\_key$ (line
ln:alg-dirdeq-20).

The code for the clients operations for enqueue, is presented in Algorithm 8.
For enqueuing to the back of the deque, the client sends an ENQ_T message to
$s_{s}$ and blocks waiting for its response. When it receives the unique key
from $s_{s}$ , the client is free to insert the element lazily. For enqueuing
to the front of the deque, the client sends an ENQ_H message and performs the
same actions as for enqueuing to the back.

Algorithm 8 Enqueue operations for a client of the directory-based deque. 33 |  void EnqueueTail(int $cid$, Data $data$) $\\{$
---|---
34 |  $sid$ = get the synchronizer id;
35 |  send($sid,\langle{\tt ENQ\\_T},cid\rangle$);
36 |  $key$ = receive(sid);
37 |  DirInsert($key,data$);
|  $\\}$
38 |
39 |  void EnqueueHead(int $cid$, Data $data$) $\\{$
40 |  $sid$ = get the synchronizer id;
41 |  send($sid,\langle{\tt ENQ\\_H},cid\rangle$);
42 |  $key$ = receive(sid);
43 |  DirInsert($key,data$);
44 |  $\\}$

Algorithm 9 Dequeue operation for a client of the directory-based deque. 45 |  Data DequeueTail(int $cid$) $\\{$
---|---
46 |  $sid$ = get the synchronizer id;
47 |  send($sid,\langle{\tt DEQ\\_T},cid\rangle$);
48 |  $status$ = receive($sid$);
49 |  return $status$;
|  $\\}$
|
50 |  Data DequeueHead(int $cid$) $\\{$
51 |  $sid$ = get the synchronizer id;
52 |  send($sid,\langle{\tt DEQ\\_H},cid\rangle$);
53 |  $status$ = receive($sid$);
54 |  return $status$;
|  $\\}$

The client code for dequeue to the front and dequeue to the back, is presented
in Algorithm 9. For dequeuing to the back of the deque, the client sends an
DEQ_T message to $s_{s}$ and blocks waiting for its response. The synchronizer
performs the dequeue itself and sends back the response. For dequeuing to the
front of the deque, the client sends an DEQ_H message and performs the same
actions as for enqueue to the back.

####  5.5.2 Proof of Correctness

Let $\alpha$ be an execution of the directory-based deque implementation. We
assign linearization points to enqueue and dequeue operations in $\alpha$ as
follows:

The linearization point of an enqueue back operation $op$ is placed in the
configuration resulting from the execution of line ln:alg-dirdeq-6 for $op$ by
$s_{s}$. The linearization point of a dequeue back operation $op$ is placed in
the configuration resulting from the execution of either line ln:alg-dirdeq-9
or line ln:alg-dirdeq-13 for $op$ (whichever is executed) by $s_{s}$. The
linearization point of an enqueue front operation $op$ is placed in the
configuration resulting from the execution of line ln:alg-dirdeq-16 for $op$
by $s_{s}$. The linearization point of a dequeue front operation $op$ is
placed in the configuration resulting from the execution of either line
ln:alg-dirdeq-19 or line ln:alg-dirdeq-23 for $op$ (whichever is executed) by
$s_{s}$.

######  Lemma 14.

The linearization point of an enqueue (dequeue) operation $op$ executed by
client $c$ is placed within its execution interval.

###### Proof.

Assume that $op$ is an enqueue front (back) operation and let $c$ be the
client that invokes it. After the invocation of $op$, $c$ sends a message to
$s_{s}$ (line ln:enh02) and awaits a response from it. Recall that routine
receive() (line ln:enh03) blocks until a message is received. The
linearization point of $op$ is placed at the configuration resulting from the
execution of line ln:alg-dirdeq-16 for $op$ by $s_{s}$. This line is executed
after the request by $c$ is received, i.e. after $c$ invokes EnqueueHead
(EnqueueTail). Furthermore, it is executed before $c$ receives the response by
the server and thus, before EnqueueHead (EnqueueTail) returns. Therefore, the
linearization point is included in the execution interval of enqueue front
(back).

The argumentation regarding dequeue front (back) operations is similar. ∎

Denote by $L$ the sequence of operations which have been assigned
linearization points in $\alpha$ in the order determined by their
linearization points. Let $C_{i}$ be the configuration in which the $i$-th
operation $op_{i}$ of $L$ is linearized; denote by $C_{0}$ the initial
configuration. Denote by $\alpha_{i}$, the prefix of $\alpha$ which ends with
$C_{i}$ and let $L_{i}$ be the prefix of $L$ up until the operation that is
linearized at $C_{i}$. We denote by $head_{i}$ the value of the local variable
$head\\_key$ of $s_{s}$ at configuration $C_{i}$, and by $tail_{i}$ the value
of the local variable $tail\\_key$ of $s_{s}$ at $C_{i}$. By the pseudocode,
we have that the initial values of $tail\\_key$ and $head\\_key$ are $0$;
therefore, we consider that $head_{0}=tail_{0}=0$.

By analogous reasoning as the one followed in the case of the directory-based
queue, inspection of the pseudocode leads to the following observations.

######  Observation 15.

Instances of Algorithm 7 are executed sequentially, i.e. their execution does
not overlap.

######  Observation 16.

Given two configurations $C_{i}$, $C_{i+1}$, $i\geq 0$, in $\alpha$, there is
at most one step in the execution interval between $C_{i}$ and $C_{i+1}$ that
modifies $tail\\_key$.

Denote by $D_{i}$ the sequential deque that results if the operations of
$L_{i}$ are applied sequentially to an initially empty queue. Let the size of
$D_{i}$ (i.e. the number of elements contained in $D_{i}$) at $C_{i}$ be
$d_{i}$. Denote by $sl_{i}^{j}$ the $j$-th element of $D_{i}$, $1\leq j\leq
d_{i}$. Each element of $D_{i}$ is a pair of type $\langle key,data\rangle$
where the elements from the bottommost to the topmost are assigned integer
keys as follows: Let $f_{i}$ be the key of element $sl_{i}^{1}$ and $l_{i}$ be
the key of element $sl_{i}^{d_{i}}$ in some configuration $C_{i}$. We denote
the $key$ field of the $\langle data,key\rangle$ pair that comprises some
element $sl_{i}^{j}$, $1\leq j\leq d_{i}$, of $D_{i}$ by $sl_{i}^{j}.key$.
Then, if $d_{i}>1$, $sl_{i}^{j+1}.key=sl_{i}^{j}.key+1$, $1\leq j\leq d_{i}$.
We consider that if $op_{1}$ is an enqueue front operation, then
$f_{1}=l_{1}=0$, while if it is an enqueue back operation, then
$f_{1}=l_{1}=1$. Notice that $l_{i}-f_{i}+1=d_{i}$.

Consider a sequence of elements $S$. If $e$ is the first element of $S$, we
denote by $S\setminus_{f}e$ the suffix of $S$ that results by removing only
element $e$ from the first position of $S$. If $e$ is the last element of $S$,
we denote by $S\setminus_{b}e$ the prefix of $S$ that results by removing only
element $e$ from the last position of $S$. If $e$ is an element not included
in $S$, we denote by $S^{\prime}=S\cdot e$ the sequence that results by
appending element $e$ to the end of $S$, and by $S^{\prime\prime}=e\cdot S$
the sequence that results by prefixing $S$ with element $e$.

######  Lemma 17.

For each integer $i\geq 1$, the following hold at $C_{i}$:

  1. 1.

If $op_{i}$ is an enqueue back operation, then $tail_{i}$ = $tail_{i-1}+1$.

  2. 2.

If $op_{i}$ is a dequeue back operation, then it holds that $tail_{i}$ =
$tail_{i-1}-1$ if $tail_{i-1}\neq head_{i-1}$; otherwise,
$tail_{i}=tail_{i-1}$.

###### Proof.

Fix any $i\geq 1$. If $op_{i}$ is an enqueue back operation, the linearization
point of $op_{i}$ is placed at the configuration resulting from the execution
of line ln:alg-dirdeq-6. By inspection of the pseudocode (lines ln:alg-
dirdeq-5-ln:alg-dirdeq-6), we have that in the instance of Algorithm 7
executed for $op_{i}$, $tail\\_key$ is incremented before it is sent to the
client $c$ that invoked $op_{i}$. By Observations 15 and 16, this is the only
increment that occurs on $tail\\_key$ between $C_{i-1}$ and $C_{i}$. Thus,
Claim 1 holds.

If $op_{i}$ is a dequeue back operation, the linearization point of $op_{i}$
is placed either at the configuration resulting from the execution of line
ln:alg-dirdeq-9 or at the configuration resulting from the execution of line
ln:alg-dirdeq-13. Let $op_{i-1}$ be a dequeue back operation that is
linearized at the execution of line ln:alg-dirdeq-9. By inspection of the
pseudocode (line ln:alg-dirdeq-8), this occurs only in case
$head_{i-1}=tail_{i-1}$. Since the execution of this line does not modify
$tail\\_key$, $tail_{i}=tail_{i-1}$ and Claim 2 holds.

Now let $op_{i}$ be a dequeue back operation that is linearized at the
configuration resulting from the execution of line ln:alg-dirdeq-13. By the
pseudocode (lines ln:alg-dirdeq-10-ln:alg-dirdeq-13) and by Observation 8, it
follows that the execution of line ln:alg-dirdeq-10 is the only step in which
$tail\\_key$ is modified in the execution interval between $C_{i-1}$ and
$C_{i}$. Since line ln:alg-dirdeq-13 is executed, it holds that the condition
of the if clause of line ln:alg-dirdeq-8 evaluates to false, i.e. it holds
that $head_{i-1}\neq tail_{i-1}$. Furthermore, because of the execution of
line ln:alg-dirdeq-10, $tail_{i}=tail_{i-1}-1$. Thus, Claim 2 holds. ∎

######  Lemma 18.

For each integer $i\geq 1$, the following hold at $C_{i}$:

  1. 1.

In case $op_{i}$ is an enqueue front operation, then, if $i>1$ and $op_{i-1}$
is an enqueue front operation, it holds that $head_{i}$ = $head_{i-1}-1$;
otherwise $head_{i}=head_{i-1}$.

  2. 2.

In case $op_{i}$ is a dequeue front operation, then, if $head_{i-1}\neq
tail_{i-1}$, $i>1$, and $op_{i-1}$ is not an enqueue front operation, it holds
that $head_{i}$ = $head_{i-1}+1$ ; otherwise $head_{i}=head_{i-1}$.

###### Proof.

Fix any $i\geq 1$. Let $op_{i}$ be an enqueue front operation. If $i=1$, then
by inspection of the pseudocode, we have that $head\\_key$ is not modified
before the execution of line ln:alg-dirdeq-16. Since $head_{0}=0$ and the
execution of line ln:alg-dirdeq-16 does not modify $head\\_key$, it follows
that $head_{1}=0=head_{0}$ and Claim 1 holds. Now let $i>1$. By inspection of
the pseudocode and by Observation 15 we have that $head\\_key$ is not modified
by enqueue back and dequeue back operations. By the pseudocode, Observation 15
and the way linearization points are assigned, we have that although
$head\\_key$ is modified by dequeue front operations only before the
configuration in which the operation is linearized, it is modified by enqueue
front operations in the step (line ln:alg-dirdeq-15) right after the
configuration in which an enqueue front operation is linearized. Therefore, if
$op_{i-1}$ is an enqueue front operation, then $head\\_key$ is decremented
once (line ln:alg-dirdeq-15) in the execution interval between $C_{i-1}$ and
$C_{i}$. Thus, if $op_{i-1}$ is an enqueue front operation, then
$head_{i}=head_{i-1}+1$, while if $op_{i-1}$ is any other type of operation,
$head_{i}=head_{i-1}$. Thus, Claim 1 holds.

Now let $op_{i}$ be a dequeue operation. If $i=1$, then by inspection of the
pseudocode, we have that $head\\_key$ is not modified before the execution of
line ln:alg-dirdeq-10. By the pseudocode and by Observation 15, $tail\\_key$
is not modified as well before the execution of line ln:alg-dirdeq-10. Thus,
$head_{0}=0=tail_{0}$ and the if condition of line ln:alg-dirdeq-8 evaluates
to true. Then, $op_{1}$ is linearized in the configuration resulting from the
execution of line ln:alg-dirdeq-19. Notice that the execution of this line
does not modify $head\\_key$. It follows that $head_{1}=0=head_{0}$ and that
Claim 2 holds.

Now let $i>1$. The linearization point of $op_{i}$ may be placed at the
configuration resulting from the execution of line ln:alg-dirdeq-19 or line
ln:alg-dirdeq-23, whichever is executed by $s_{s}$ for it. Let the
linearization point be placed in the configuration resulting from the
execution of line ln:alg-dirdeq-19. In that case, $head_{i-1}=tail_{i-1}$.
Notice that the execution of that line does not modify $head\\_key$.
Therefore, $head_{i}=head_{i-1}$, and Claim 2 holds. Now let the linearization
point be placed in the configuration resulting from the execution of line
ln:alg-dirdeq-23. In case $op_{i-1}$ is an enqueue back or dequeue tail
operation, $head\\_key$ is not modified by it. Therefore, since line ln:alg-
dirdeq-20 is executed before line ln:alg-dirdeq-23, $head_{i}=head_{i+1}+1$
and Claim 2 holds. The same also holds if $op_{i-1}$ is a dequeue front
operation. If $op_{i-1}$ is an enqueue front operation, then by inspection of
the pseudocode (line ln:alg-dirdeq-15), we have that $head\\_key$ is
decremented in the step following the configuration in which $op_{i-1}$ is
linearized. Therefore, in this case and by Observation 15, $head\\_key$ is
decremented and then incremented once in the execution interval between
$C_{i-1}$ and $C_{i}$. This in turn implies that
$head_{i}=head_{i-1}-1+1=head_{i-1}$ and Claim 2 holds. ∎

Recall that $sl_{i}^{j}.key=f_{i}+j-1$ or $sl_{i}^{j}.key=l_{i}-j+1$ . By
inspection of the pseudocode (lines ln:alg-dirdeq-16/ln:alg-dirdeq-6), we see
that, when $op_{i}$ is an enqueue front/back operation, $head_{i}$/$tail_{i}$
is sent by $s_{s}$ to the client $c$ that invoked $op_{i}$. By further
inspection of the pseudocode (lines ln:enh03-ln:enh04/ln:ent04-ln:ent05), we
see that $c$ uses $head_{i}$/$tail_{i}$ as the $key$ field of the element it
enqueues, i.e. uses it as argument for auxiliary function
DirInsert()/DirDelete(). When $op_{i}$ is a dequeue front/back operation, by
inspection of the pseudocode (lines ln:alg-dirdeq-19/ln:alg-dirdeq-9), we have
that when $head\\_key=tail\\_key$, $s_{s}$ sends NACK to $c$, and that when
$c$ receives NACK, it does not enqueue any element and instead, returns $\bot$
(lines ln:dqh03-ln:dqh04/ln:dqt03-ln:dqt04). When $head\\_key\neq tail\\_key$,
$s_{s}$ uses $head_{i}$/($tail_{i}+1)$ as the $key$ field in order to
determine which element to dequeue (lines ln:alg-dirdeq-22/ln:alg-dirdeq-12).
Then, the following observation holds.

######  Observation 19.

If $op_{i}$ is an enqueue back operation, it inserts a pair with
$key=tail_{i}$ into the directory. If $op_{i}$ is a dequeue back operation,
then, if $head_{i}\neq tail_{i}$, it removes a pair with $key=tail_{i}+1$ from
the directory; if $head_{i}=tail_{i}$, it does not remove any pair from the
directory. If $op_{i}$ is an enqueue front operation, it inserts a pair with
$key=head_{i}$ into the directory. If $op_{i}$ is a dequeue front operation
then, if $head_{i}\neq tail_{i}$, it removes a pair with $key=head_{i}$ from
the directory; if $head_{i}=tail_{i}$, it does not remove any pair from the
directory.

######  Lemma 20.

At $C_{i}$, $i\geq 1$, the following hold:

  1. 1.

If $op_{i}$ is an enqueue back operation, then $tail_{i}=sl_{i}^{d_{i}}.key$.

  2. 2.

If $op_{i}$ is a dequeue back operation, then if $D_{i-1}\neq\epsilon$,
$tail_{i}=sl_{i-1}^{d_{i-1}}.key$. If $D_{i-1}=\epsilon$, then
$head_{i}=tail_{i}$.

  3. 3.

If $op_{i}$ is an enqueue front operation, then $head_{i}=sl_{i}^{1}.key$.

  4. 4.

If $op_{i}$ is a dequeue front operation, then if $D_{i-1}\neq\epsilon$,
$head_{i}=sl_{i-1}^{1}.key$. If $D_{i-1}=\epsilon$, then $head_{i}=tail_{i}$.

###### Proof.

We prove the claims by induction.

Base case. We prove the claim for $i$ = $1$.

Consider the case where $op_{1}$ is an enqueue back operation. Then, $d_{1}=1$
and by definition, $D_{1}$ contains only the pair $\langle 1,data\rangle$. By
Observation 15, it is the first operation in $\alpha$ for which an instance of
Algorithm 7 is executed by $s_{s}$. Therefore, by Lemma 17,
$tail_{1}=tail_{0}+1=1$. Thus, $tail_{1}=sl_{1}^{d_{1}}.key$ and Claim 1
holds.

Next, consider the case where $op_{1}$ is a dequeue back operation. By
Observation 15, $op_{1}$ is the first operation in $\alpha$ for which an
instance of Algorithm 7 is executed by $s_{s}$. Notice that then,
$Q_{1}=\epsilon$. Therefore, by Lemma 17, $tail_{1}=tail_{0}=0$. Since
$head\\_key$ is not modified by dequeue back operations,
$head_{1}=head_{0}=0$. Thus, $head_{1}=tail_{1}$, so Claim 2 holds.

Next, consider the case where $op_{1}$ is an enqueue front operation. Again,
by definition, $d_{1}=1$ and $D_{1}$ contains only the pair $\langle
0,data\rangle$. By Observation 15, it is the first operation in $\alpha$ for
which an instance of Algorithm 7 is executed by $s_{s}$. Therefore, by Lemma
18, $head_{1}=head_{0}=0$. Thus, $head_{1}=sl_{1}^{1}.key$ and Claim 3 holds.

Finally, consider the case where $op_{1}$ is a dequeue front operation. By
Observation 15, $op_{1}$ is the first operation in $\alpha$ for which an
instance of Algorithm 7 is executed by $s_{s}$. Notice that then,
$Q_{1}=\epsilon$. Therefore, by Lemma 18, $head_{1}=head_{0}=0$. Since
$tail\\_key$ is not modified by dequeue front operations,
$tail_{1}=tail_{0}=0$. Thus, $head_{1}=tail_{1}$ and Claim 4 holds.

Hypothesis. Fix any $i$, $i>0$ and assume that the lemma holds at $C_{i}$.

Induction step. We prove that the claims also hold at $C_{i+1}$. Assume that
$op_{i+1}$ is an enqueue back operation. By the induction hypothesis, if
$op_{i}$ is an enqueue back operation, then
$sl_{i}^{d_{i}}.key=tail_{i}=l_{i}$. Similarly, if $op_{i}$ is a dequeue back
operation, then by the induction hypothesis,
$sl_{i-1}^{d_{i-1}}.key=tail_{i}$. Since the dequeue back operation removes
the last element in $D_{i-1}$, it follows that the last element
$sl_{i}^{d_{i}}$ of $D_{i}$ is $sl_{i-1}^{d_{i-1}}$. Thus, here also,
$tail_{i}=sl_{i}^{d_{i}}.key=l_{i}$. Notice that enqueue front and dequeue
front operations do not modify $tail\\_key$. Since these types of operation do
not affect the back of the sequential dequeue, it still holds that
$tail_{i}=sl_{i}^{d_{i}}.key=l_{i}$. Since $op_{i+1}$ is an enqueue back
operation, by Lemma 17, we have that $tail_{i+1}=tail_{i}+1$. By Observation
19, we have that the client $c$ that initiated $op_{i+1}$ inserts a pair with
$key=tail_{i+1}=tail_{i}+1$ into the directory. By definition,
$sl_{i+1}^{d_{i+1}}.key=sl_{i}^{d_{i}}.key+1$. Thus,
$sl_{i+1}^{d_{i+1}}.key=tail_{i}+1$, and Claim 1 holds.

Now assume that $op_{i+1}$ is a dequeue back operation. We examine two cases.
First, let $D_{i}\neq\epsilon$. By Lemma 17, it then holds that
$tail_{i+1}=tail_{i}-1$. By Observation 19, we have that a pair with
$key=tail_{i+1}=tail_{i}-1$ is removed from the directory. By definition, we
have that $D_{i+1}=D_{i}\setminus_{b}sl_{i}^{d_{i}}$. Also by definition, we
have that $sl_{i}^{d_{i}}.key=sl_{i}^{d_{i}-1}.key+1$. Because of $op_{i+1}$,
$sl_{i}^{d_{i}-1}=sl_{i+1}^{d_{i+1}}$. Since $tail_{i+1}=tail_{i}-1$, Claim 2
holds. Now let $D_{i}=\epsilon$. In this case, $op_{i+1}$ cannot have any
effect on the state of the deque. By inspection of the pseudocode, this
corresponds to the operation being linearized in the configuration resulting
from the execution of line ln:alg-dirdeq-9. Notice that in order for this to
be the case, the if condition of line ln:alg-dirdeq-8 must evaluate to true.
This occurs if $head_{i}=tail_{i}$, thus Claim 2 holds.

Next assume that $op_{i+1}$ is an enqueue front operation. By the induction
hypothesis, if $op_{i}$ is an enqueue front operation, then
$sl_{i}^{1}.key=head_{i}=f_{i}$. By Lemma 18, it holds then that
$head_{i+1}=head_{i}-1$. Since $op_{i+1}$ is an enqueue front operation, it
prepends an element to $D_{i}$ and therefore, $sl_{i}^{1}=sl_{i+1}^{2}$. By
definition of $D_{i+1}$, $sl_{i+1}^{1}.key=sl_{i+1}^{2}.key-1$. Since
$sl_{i+1}^{2}.key=head_{i}$, $sl_{i+1}^{1}.key=head_{i+1}$ and Claim 3 holds.

On the other hand, if $op_{i}$ is a dequeue front operation, then by the
induction hypothesis, $sl_{i-1}^{1}.key=head_{i}$. By Lemma 18, it also
follows that in this case, $head_{i+1}=head_{i}$. Notice that by definition,
$op_{i}$ removes element $sl_{i-1}^{1}$ from $D_{i-1}$. Then, for element
$sl_{i}^{1}$ of $D_{i}$, by definition, $sl_{i}^{1}.key=sl_{i-1}^{1}.key+1$.
This means that $sl_{i-1}^{1}.key=head_{i}=sl_{i}^{1}.key-1$. Since
$head_{i+1}=head_{i}$, Claim 3 holds.

Notice that enqueue back and dequeue back operations do not modify
$head\\_key$.

Finally, assume that $op_{i+1}$ is a dequeue front operation. We examine two
cases. First, let $D_{i}\neq\epsilon$. By Lemma 18, it then holds that
$head_{i+1}=head_{i}$. By Observation 19, we have that a pair with
$key=head_{i+1}=head_{i}$ is removed from the directory. By definition, we
have that $D_{i+1}=D_{i}\setminus_{b}sl_{i}^{1}$. Also by definition, we have
that $sl_{i}^{1}.key=sl_{i}^{2}.key-1$. Because of $op_{i+1}$,
$sl_{i}^{2}=sl_{i+1}^{1}$. Since $head_{i+1}=head_{i}$, Claim 4 holds. Now let
$D_{i}=\epsilon$. In this case, $op_{i+1}$ cannot have any effect on the state
of the deque. By inspection of the pseudocode, this corresponds to the
operation being linearized in the configuration resulting from the execution
of line ln:alg-dirdeq-19. Notice that in order for this to be the case, the if
condition of line ln:alg-dirdeq-18 must evaluate to true. This occurs if
$head_{i}=tail_{i}$, thus Claim 4 holds. ∎

From the above lemma, we have the following corollary.

######  Corollary 21.

$D_{i}=\epsilon$ if and only if $head_{i}=tail_{i}$.

######  Lemma 22.

If $op_{i}$ is a dequeue back operation, then it returns the value of the
field $data$ of $sl_{i-1}^{d_{i-1}}$ or $\bot$ if $D_{i-1}=\epsilon$.

###### Proof.

Consider the case where $D_{i-1}\neq\epsilon$. By definition of $D_{i}$, we
have that $D_{i}=D_{i-1}\setminus_{b}sl_{i-1}^{d_{i-1}}$. Let $op_{j}$ be the
enqueue operation that is linearized before $op_{i}$ and inserts an element
with key $tail_{i}+1$ to the queue. Notice by the pseudocode (lines ln:alg-
dirdeq-11-ln:alg-dirdeq-13), that the parameter of DirDelete is $tail_{i}+1$.
By the semantics of DirDelete, if at the point that the instance of DirDelete
is executed in the do \- while loop of lines ln:alg-dirdeq-11-ln:alg-dirdeq-12
for $op_{i}$, the instance of DirInsert of $op_{j}$ has not yet returned, then
DirDelete returns $\langle\bot,-\rangle$.

By Lemma 17, $tail_{i}+1$ is the $key$ of the last pair $sl_{i-1}^{d_{i-1}}$
in $D_{i-1}$. Therefore, when DirDelete returns a $status\neq\bot$, it holds
that it returns the $data$ field of $sl_{i-1}^{d_{i-1}}$, the last element in
$D_{i-1}$. Notice that this value is sent to the client $c$ that invoked
$op_{i}$ (line ln:alg-dirdeq-13) and that $c$ uses this value as the return
value of $op_{i}$ (lines ln:dqt03-ln:dqt04). Thus, the claim holds.

Now consider the case where $D_{i-1}=\epsilon$. Since, by Corollary 21, when
this is the case, $head_{i}=tail_{i}$, NACK is sent $c$ and, by inspection of
the pseudocode, $op_{i}$ returns $\bot$, i.e. the claim holds. ∎

In a similar fashion, we can prove the following.

######  Lemma 23.

If $op_{i}$ is a dequeue front operation, then it returns the value of the
field $data$ of $sl_{i-1}^{1}$ or $\bot$ if $D_{i-1}=\epsilon$.

From the above lemmas we have the following:

######  Theorem 24.

The directory-based deque implementation is linearizable.

###  5.6 Hierarchical approach, Elimination, and Combining.

In this section, we outline how the hierarchical approach, described in
Section LABEL:sec:impl-paradigms, is applied to the directory-based designs.

Each island master $m_{i}$ performs the necessary communication between the
clients of its island and $s_{s}$. In the stack implementation, each island
master applies elimination before communicating with $s_{s}$. To further
reduce communication with $s_{s}$, $m_{i}$ applies a technique known as
combining [61]. In the case of stack, once elimination has been applied, there
is only one type of requests that must be sent to the synchronizer; for all
these requests, $m_{i}$ sends just one message containing their number $f$ and
their type to the synchronizer. In case of push operations, this method allows
the synchronizer to directly increment $top$ by $f$ and respond to $m_{i}$
with the value $g$ that $top$ had before the increment. Once $m_{i}$ receives
$g$, it informs the clients (which initiated these requests) that the keys for
their requests are $g,g+1,\ldots,g+f-1$. In the case of queue, each message of
$m_{i}$ to $s_{s}$ contains two counters counting the number of active enqueue
and dequeue requests from clients of island $i$. When $s_{s}$ receives such a
message it responds with a message containing the current values of $tail$ and
$head$. It then increments $tail$ and $head$ by the value of the first and
second counter, respectively. Server $m_{i}$ assigns unique keys to active
enqueue and dequeue operations, based on the value of $tail$ and $head$ it
receives, in a way similar as in stacks. Combining can be used for deques (in
addition to elimination) in ways similar to those described above.

##  6 Token-based Stacks, Queues, and Deques

We start with an informal description of the token-based technique that we
present in this section. We assume that the servers are numbered from $0$ to
${\tt NS}\ -1$ and form a logical ring. Each server has allocated a chunk of
memory (e.g. one or a few pages) of a predetermined size, where it stores
elements of the implemented DS. A DS implementation employs (at least) one
token which identifies the server $s_{t}$, called the token server, at the
memory chunk of which newly inserted elements are stored. (A second token is
needed in cases of queues and deques.) When the chunk of memory allocated by
the token server becomes full, the token server gives up its role and appoints
another (e.g. the next) server as the new token server. A client remembers the
server that served its last request and submits the next request it initiates
to that server; so, each response to a client contains the id of the server
that served the client’s request. Servers that do not have the token for
handling a request, forward the request to subsequent servers; this is done
until the request reaches the appropriate token server. A server allocates a
new (additional) chunk of memory every time the token reaches it (after having
completed one more round of the ring) and gives up the token when this chunk
becomes full.

Section 6.1 presents the details of the token-based distributed stack. The
token-based queue implementation appears in Section 6.2. Section 6.3 provides
the token-based deque. We start by presenting static versions of the
implementations, i.e. versions in which the total memory allocated for the
data structure is predetermined during an execution and once it is exhausted
the data structure becomes full and no more insertions of elements can occur.
We then describe in Section 6.5, how to take dynamic versions of the data
structures from their static analogs.

###  6.1 Token-Based Stack

To implement a distributed stack, each server uses its allocated memory chunk
to maintain a local stack, $lstack$. Initially, $s_{t}$ is the server with id
$0$. To perform a push (or pop), a client $c$ sends a push (or pop) request to
the server that has served $c$’s last request (or, initially, to server $0$)
and awaits for a response. If this server is not the current token server at
the time that it receives the request, it forwards the request to its next or
previous server, depending on whether its local stack is full or empty,
respectively. This is repeated until the request reaches the server $s_{t}$
that has the token which pushes the new element onto its local stack and sends
an ACK to $c$. If $s_{t}$’s local stack does not have free space to
accommodate the new element, it sends the push request of $c$, together with
an indication that it gives up its token, to the next server. POP is treated
by $s_{t}$ in a similar way.

####  6.1.1 Algorithm Description

Algorithm 10 Events triggered in a server of the token-based stack. 1 | LocalStack $lstack$ = $\varnothing$;
---|---
2 |  int $my\\_sid$; /* each server has a unique id */
3 |  int $token=0$;
|
4 | a message $\langle op,data,id,tk\rangle$ is received:
5 |  switch ($op$) $\\{$
6 |  case PUSH:
7 |  if ($tk$ == TOKEN) $token=my\\_sid$;
8 |  if ($token\neq my\\_sid$) $\\{$
9 |  send($token,\langle op,data,id,tk\rangle$);
10 |  break;
|  $\\}$
11 |  if (!IsFull($lstack$)) $\\{$
12 |  push($lstack,data$);
13 |  send($id,\langle{\tt ACK},my\\_sid\rangle$);
14 |  $\\}$ else if ($my\\_sid\neq$ NS-1) $\\{$
15 |  $token$ = find_next_server($my\\_sid$);
16 |  send($token,\langle op,data,id,{\sf TOKEN}\rangle$);
17 |  $\\}$ else /* It’s the last server in the order, thus the stack is full */
18 |  send($id,\langle{\tt NACK},my\\_sid\rangle$);
19 |  break;
20 |  case POP:
21 |  if ($tk$ == TOKEN) $token=my\\_sid$;
22 |  if ($token\neq my\\_sid$) $\\{$
23 |  send($token,\langle op,data,id,tk\rangle$);
24 |  break;
|  $\\}$
25 |  if (!IsEmpty($lstack$)) $\\{$
26 |  $data$ = pop($lstack$);
27 |  send($id,\langle data,my\\_sid\rangle$);
28 |  $\\}$ else if ($my\\_sid\neq 0$) $\\{$
29 |  $token$ = find_previous_server($my\\_sid$);
30 |  send($token,\langle op,data,id,{\sf TOKEN}\rangle$);
31 |  $\\}$ else /* It’s the first server in the order, thus the stack is empty */
32 |  send($id,\langle{\tt NACK},my\\_sid\rangle$);
33 |  break;
|  $\\}$

Initially the elements are stored in the memory space allocated by server
$s_{0}$, the first server in the ring. At this point, $s_{0}$ is the token
server; the token server manages the top of the stack. Once the memory chunk
of the token server becomes full, the token server notifies the next server
($s_{1}$) in the ring to become the new token server.

The pseudocode for the server is presented in Algorithm 10. Each server $s$,
apart from a local stack ($lstack$), maintains also a local variable $token$
which identifies whether $s$ is the token server. The messages that are
transmitted during the execution are of type PUSH and POP, which are sent from
clients that want to perform the mentioned operation to the servers, or are
forwarded from any server towards the token server. Each message has four
fields: (1) $op$ with the operation to be performed, (2) $data$, containing
data in case of ENQ and $\bot$ otherwise, (3) $id$ that contains the id of the
sender and (4) a one-bit flag $tk$ which is set to TOKEN only when a forwarded
message denotes also a token transition.

If the message is of type PUSH (line ln:63), $s$ first checks whether the
message contains a token transition. If $tk$ is marked with TOKEN, $s$ changes
the $token$ variable to contain its id (line ln:60). If $s$ is not a token
server, it just forwards the message to the next server (line ln:65).
Otherwise, it checks if there is free space in $lstack$ to store the new
request (line ln:66). If there is such space, the server pushes the data to
the stack, and sends back an ACK to the client. In this implementation, the
push() function (line ln:lp3) does not need to return any value, since the
check for memory space has already been performed by the server on line ln:66,
hence push() is always successful.

If $s$ does not have any free space, it must notify the next server to become
the new token server. More specifically, if $s$ is not the server with id
${\tt NS}-1$ (line ln:67), it forwards to the next server the PUSH message it
received from the client, after setting the $tk$ field to TOKEN (line ln:70).
On the other hand, if $s$ is the server with id ${\tt NS}-1$, all previous
servers have no memory space available to store a stack element. In this case,
$s$ sends back to the client a message NACK(line ln:71).

If the message is of type POP (line ln:72) similar actions take place: $s$
checks whether the message contains a token transition and if its true, it
changes its local variable $token$ appropriately. Then $s$ checks if it is the
token server (line ln:73). If not, it just forwards the message towards the
server it considers as the token server (line ln:74). If $s$ is the token
server, it checks if its local stack is empty (line ln:75). If it is not
empty, the pop operation can be executed normally. At the end of the
operation, $s$ sends to the client the data of the previous top element (line
ln:lp2). In case of an empty local stack, if $s$ is not $s_{0}$ (line ln:76),
it forwards to the previous server the client’s POP message, after setting the
$tk$ field to TOKEN (line ln:79). On the other hand, if the server that
received the POP request is $s_{0}$ ($id==0$), then all the servers have empty
stacks and the server sends back to the client a NACK message (line ln:80).

Algorithm 11 Push operation for a client of the token-based stack. 34 |  $sid=0$;
---|---
35 | Data ClientPush(int $cid$, Data $data$) $\\{$
36 | send($sid,\langle{\tt PUSH},data,cid,\bot\rangle$);
37 |  $\langle status,sid\rangle$ = receive();
38 |  return $status$;
|  $\\}$

Algorithm 12 Pop operation for a client of the token-based stack. 39 |  $sid=0$;
---|---
40 | Data ClientPop(int $cid$) $\\{$
41 | send($sid,\langle{\tt POP},\bot,cid,\bot\rangle$);
42 |  $\langle status,sid\rangle$ = receive();
43 |  return $status$;
|  $\\}$

The clients execute the operations push and pop, by calling the functions
ClientPush() and ClientPop(), respectively. Each of these functions sends a
message to the server. Initially, the clients forward their requests to
$s_{0}$. Because the server that maintains the top element might change
though, the clients update the $sid$ variable through a lazy mechanism. When a
client $c$ wants to perform an operation, it sends a request to the server
with id equal to the value of $sid$ (lines ln:81 and ln:85). If the message
was sent to an incorrect server, it is forwarded by the servers till it
reaches the server that holds the token. That server is going to respond with
the status value of the operation and with the its id. This way, $c$ updates
the variable $sid$.

During the execution of the ClientPush() function, described in Algorithm 11,
the client sends a PUSH message to the server with id $sid$ (line ln:82). It
then, waits for its response (line ln:83). When the client receives the
response, it updates the $sid$ variable (line ln:83) and returns the $status$.
The $status$ is either ACK for a successful push, or NACK for a full stack.

The ClientPop() function operates in a similar fashion. The client sends a POP
message to the server with id $sid$ (line ln:86). It then, waits for its
response (line ln:87). The server responds with a NACK (for empty queue), or
with the value of the top element (otherwise). The server also forwards its
id, which is stored in client’s variable $sid$. The client finally, returns
the $status$ value and terminates.

####  6.1.2 Proof of Correctness

Let $\alpha$ be an execution of the token-based stack algorithm presented in
Algorithms 10, 11, and 12. Let $op$ be any operation in $\alpha$. We assign a
linearization point to $op$ by considering the following cases:

  * •

$op$ is a push operation. Let $s_{t}$ be the token server that responds to the
client that initiated $op$ (i.e. the receive of line ln:83 in the execution of
$op$ receives a message from $s_{t}$). If $op$ returns ACK, the linearization
point is placed at the configuration resulting from the execution of line
ln:lp1 by $s_{t}$ for $op$. Otherwise, the linearization point of $op$ is
placed at the configuration resulting from the execution of line ln:71 by
$s_{t}$ for $op$.

  * •

$op$ is a pop operation. Let $s_{t}$ be the token server that responds to the
client that initiated $op$ (line ln:87). If the operation returns NACK, the
linearization point of $op$ is placed at the configuration resulting from the
execution of line ln:80 by $s_{t}$ for $op$. Otherwise, the linearization
point of $op$ is placed at the configuration resulting from the execution of
line ln:lp2 by $s_{t}$ for $op$.

Denote by $L$ the sequence of operations (which have been assigned
linearization points) in the order determined by their linearization points.

######  Lemma 25.

The linearization point of a push (pop) operation $op$ is placed in its
execution interval.

###### Proof Sketch.

Assume that $op$ is a push operation and let $c$ be the client that invokes
it. After the invocation of $op$, $c$ sends a message to some server $s$ and
awaits a response. Recall that routine receive() (line ln:83) blocks until a
message is received. The linearization point of $op$ is placed either in the
configuration resulting from the execution of line ln:lp1 by $s_{t}$ for $op$,
where $s_{t}$ is the token server in this configuration, or in the
configuration resulting from the execution of line ln:71 by $s_{t}$ for $op$.

Either of these lines is executed after the request by $c$ is received, i.e.
after $c$ invokes ClientPush. Furthermore, they are executed before $c$
receives the response by $s_{t}$ and thus, before ClientPush returns.
Therefore, the linearization point is inside the execution interval of push.

The argumentation regarding pop operations is analogous. ∎

Each server maintains a local variable $token$ with initial value $0$
(initially, the server with id equal to $0$ is the token server). Whenever
some server $s_{i}$ receives a TOKEN message, i.e. a message with its $tk$
field equal to TOKEN (line ln:60), the value of $token$ is set to $i$. By
inspection of the pseudocode, it follows that the value of $token$ is set to
the id of the next server if the local stack of $s_{i}$ is full (line ln:68);
then, a TOKEN message is sent to the next server (line ln:70). Moreover, the
value of $token$ is set to the id of the previous server if the local stack
$lstack$ of $s_{i}$ is empty (line ln:76); then, a TOKEN message is sent to
the previous server (lines ln:77-ln:79). (Unless the server is $s_{0}$ in
which case a NACK is sent to the client (line ln:80 but no TOKEN message to
any server.) Thus, the following observation holds.

######  Observation 26.

At each configuration in $\alpha$, there is at most one server $s_{i}$ for
which the local variable $token$ has the value $i$.

At each configuration $C$, the server $s_{i}$ whose $token$ variable is equal
to $i$ is referred to as the token server at $C$.

######  Observation 27.

A TOKEN message is sent from a server with id $i$, $0\leq i<{\tt NS}-1$, to a
server with id $i+1$ only if the local stack of server $i$ is full. A TOKEN
message is sent from a server with id $i$, $0<i\leq{\tt NS}-1$, to a server
with id $i-1$ only when the local stack of server $i$ is empty.

By the pseudocode, namely the if clause of line ln:64 and the if clause of
line ln:73, the following observation holds.

######  Observation 28.

Whenever a server $s_{i}$ performs push and pop operations on its local stack
(lines ln:lp3 and ln:75.1), it holds that its local variable $token$ is equal
to $i$.

Let $C_{i}$ be the configuration at which the $i$-th operation $op_{i}$ of $L$
is linearized. Denote by $\alpha_{i}$, the prefix of $\alpha$ which ends with
$C_{i}$ and let $L_{i}$ be the prefix of $L$ up until the operation that is
linearized at $C_{i}$. Denote by $S_{i}$ the sequence of values that a
sequential stack contains after applying the sequence of operations in
$L_{i}$, in order, starting from an empty stack; let $S_{0}=\epsilon$, i.e.
$S_{0}$ is the empty sequence.

######  Lemma 29.

For each $i$, $i\geq 0$, if $s_{k_{i}}$ is the token server at $C_{i}$ and
$ls_{i}^{j}$ are the contents of the local stack of server $j$, $0\leq j\leq
k_{i}$, at $C_{i}$, then it holds that $S_{i}=ls_{i}^{0}\cdot
ls_{i}^{1}\cdot\ldots\cdot ls_{i}^{k_{i}}$ at $C_{i}$.

###### Proof.

We prove the claim by induction on $i$. The claim holds trivially for $i=0$.
Fix any $i\geq 0$ and assume that at $C_{i}$, it holds that $S_{i}$ =
$ls_{i}^{0}\cdot ls_{i}^{1}\cdot\ldots\cdot ls_{i}^{k_{i}}$. We show that the
claim holds for $i+1$.

We first assume that $op_{i+1}$ is a push operation initiated by some client
$c$. Assume first that $s_{k_{i}}=s_{k_{i+1}}$. Then, by induction hypothesis,
$S_{i}$ = $ls_{i}^{0}\cdot\ldots\cdot ls_{i}^{k_{i}}$. In case the local stack
of $s_{k_{i}}$ is not full, $s_{k_{i}}$ pushes the value $v_{i+1}$ of field
$data$ of the request onto its local stack and responds to $c$. Since no other
change occurs to the local stacks of $s_{0},\ldots,s_{k_{i}}$ from $C_{i}$ to
$C_{i+1}$, at $C_{i+1}$, it holds that $S_{i+1}=ls_{i}^{0}\cdot\ldots\cdot
ls_{i}^{k}\cdot\\{v_{i+1}\\}=ls_{i}^{0}\cdot\ldots\cdot ls_{i+1}^{k_{i}}$. In
case that the local stack of $s_{k_{i}}$ is full, since
$s_{k_{i}}=s_{k_{i+1}}$ and it is the token server, it follows that
$s_{k_{i}}=s_{{\tt NS}-1}$. In this case, $s_{k_{i}}$ responds with a NACK to
$c$ and the local stack remains unchanged. Thus, it holds that
$S_{i+1}=ls_{i}^{0}\cdot\ldots\cdot ls_{i}^{k}=S_{i}$.

Assume now that $s_{k_{i}}\neq s_{k_{i+1}}$. This implies that the local stack
of $s_{k_{i}}$ is full just after $C_{i}$. Observation 27 implies that
$s_{k_{i}}$ forwarded the token to $s_{k_{i}+1}$ in some configuration between
$C_{i}$ and $C_{i+1}$. Notice that then, $s_{k_{i}+1}=s_{k_{i+1}}$.
Observation 28 implies that the local stack of $s_{k_{i}+1}$ is empty. Thus,
the if condition of line ln:66 evaluates to true for server $s_{k_{i}+1}$ and
therefore, it pushes the value $v_{i+1}$ of $op_{i+1}$ onto its local stack.
Thus, at $C_{i+1}$, $ls_{i+1}^{k_{i}+1}$ = $\\{v_{i+1}\\}$. By definition,
$S_{i+1}$ = $S_{i}\cdot\\{v_{i+1}\\}$. Therefore, $S_{i+1}$ =
$ls_{i}^{0}\cdot\ldots\cdot ls_{i+1}^{k_{i}+1}$. And since by Observations 26
and 28, the contents of the local stacks of servers other than $k_{i}+1$ do
not change, it holds that $S_{i+1}=ls_{i+1}^{0}\cdot\ldots\cdot
ls_{i+1}^{k_{i}+1}=ls_{i+1}^{0}\cdot\ldots\cdot ls_{i+1}^{k_{i+1}}$.

The reasoning for the case where $op_{i+1}$ is an instance of a pop operation
is symmetrical. ∎

From the above lemmas and observations, we have the following.

######  Theorem 30.

The token-based distributed stack implementation is linearizable. The time
complexity and the communication complexity of each operation $op$ is $O({\tt
NS})$.

###  6.2 Token-Based Queue

To implement a queue, two tokens are employed: at each point in time, there is
a head token server $s_{h}$ and a tail token server $s_{t}$. Initially, server
$0$ plays the role of both $s_{h}$ and $s_{t}$. Each server $s_{r}$, other
than $s_{t}$ ($s_{h}$), that receives a request (directly) from a client $c$,
it forwards the request to the next server to ensure that it will either reach
the appropriate token server or return back to $s_{r}$ (after traversing all
servers). Servers $s_{t}$ and $s_{h}$ work in a way similar as server $s_{t}$
in stacks.

To prevent a request from being forwarded forever due to the completion of
concurrent requests which may cause the token(s) to keep advancing, each
server keeps track of the request that each client $c$ (directly) sends to it,
in a client table (there can be only one such request per client). Server
$s_{t}$ (and/or $s_{h}$) now reports the response to $s_{r}$ which forwards it
to $c$. If $s_{r}$ receives a response for a request recorded in its client
table, it deletes the request from the client table. If $s_{r}$ receives the
token (stack, tail, or head), it serves each request (push and pop, enqueue,
or dequeue, respectively) in its client array and records its response. If a
request, from those included in $s_{r}$’s client array, reaches $s_{r}$ again,
$s_{r}$ sends the response it has calculated for it to the client and removes
it from its client array. Since the communication channels are FIFO, the
implementations ensures that all requests, their responses, and the
appropriate tokens, move from one server to the next, based on the servers’
ring order, until they reach their destination. This is necessary to argue
that the technique ensures termination for each request.

####  6.2.1 Algorithm Description

The queue implementation follows similar ideas to those of the token-based
distributed stack, presented in Section 6.1. However, the queue implementation
employs two tokens, one for the queue’s tail and one for the queue’s head,
called head token and tail token, respectively. The tokens for the global head
and tail are initially held by $s_{0}$. However, they can be reassigned to
other servers during the execution. If the local queue of the server that has
the tail token becomes full, the token is forwarded to the next server.
Similarly, if the local queue of the server that has the head token becomes
empty, the head token is forwarded to the next server. If the appropriate
token server receives the request and serves it, it sends an ACK message back
to the server that initiated the forwarding. Then, the initial server responds
to the client with an ACK message, which also includes the id of the server
that currently holds the token.

The clients in their initial state store the id of $s_{0}$, which is the first
server to hold the head and tail tokens. The clients keep track of the servers
that hold either token in a lazy way. Specifically, a client updates its local
variable (either $enq\\_sid$ or $deq\\_sid$ depending on whether its current
active operation is an enqueue or a dequeue, respectively) with the id of the
token server when it receives a server response.

In this scheme, a client request may be transmitted indefinitely from a server
to the next without ever reaching the appropriate token server. This occurs if
both the head and the tail tokens are forwarded indefinitely along the ring.
Then, a continuous, never-ending race between a forwarded message and the
appropriate token server may occur. To avoid this scenario, we do the
following actions. When a server $s$ receives a client’s request $r$, if it
does not have the appropriate token to serve it, it stores information about
$r$ in a local array before it forwards it. Next time that the server receives
the tail (head) token, it will serve all enqueue (dequeue) requests. Notice
that since channels preserve the FIFO order and servers process messages in
the order they arrive, the appropriate token will reach $s$ earlier than the
$r$. When $s$ receives $r$, it has already processed it; however, it is then
that $s$ sends the response for $r$ to the client.

Algorithm 13 Token-based queue server’s local variables. 1 |  int $my\\_sid$;
---|---
2 |  LocalQueue $lqueue=\varnothing$;
3 |  LocalArray $clients=\varnothing$; /* Array of three values: $<$op, data, isServed$>$ */
4 |  boolean $fullQueue$ = false; /* True when tail and head are in the same
|  server and tail is before head */
5 |  boolean $hasHead$; /* Initially hasHead and hasTail are true in server 0, and false in the rest */
6 |  boolean $hasTail$;
Algorithm 14 Events triggered in a server of the token-based queue. 7 |  a message $\langle op,data,cid,sid,tk\rangle$ is received:
---|---
8 |  if (!clients[$cid$] AND clients[$cid$].$isServed$) $\\{$ /* If message has been served earlier. */
9 |  send($cid,\langle{\tt ACK},$ clients[$cid$].$data,\ my\\_sid\rangle$);
10 |  clients[$cid$] = $\bot$;
11 |  $\\}$ else $\\{$
12 |  switch ($op$) $\\{$
13 |  case ENQ:
14 |  if ($tk$ == TAIL_TOKEN) $\\{$
15 |  $hasTail$ = true;
16 |  if ($hasHead$) $fullQueue$ = true;
17 |  ServeOldEnqueues();
|  $\\}$
18 |  if (!$hasTail$) $\\{$ /* Server does not have token */
19 |  $nsid$ = find_next_server(($my\\_sid$);
20 |  if ($sid==-1$) $\\{$ /* From client. */
21 |  clients[$cid$] = $\langle{\tt ENQ},data,{\tt false}\rangle$;
22 |  send($nsid,\langle{\tt ENQ},data,cid,my\\_sid,\bot\rangle$);
23 |  $\\}$ else $\\{$ /* From server. */
24 |  send($nsid,\langle{\tt ENQ},data,cid,sid,\bot\rangle$);
|  $\\}$
25 |  $\\}$ else if (!IsFull($lqueue$)) $\\{$ /* Server can enqueue. */
26 |  enqueue($lqueue,data$);
27 |  if ($sid==-1$) /* From client. */
28 |  send($cid,\langle{\tt ACK},\bot,my\\_sid\rangle$);
29 |  else /* From server. */
30 |  send($sid,\langle{\tt ACK},\bot,cid,my\\_sid,\bot\rangle$);
31 |  $\\}$ else if ($fullQueue$) $\\{$ /* Global Queue full */
32 |  if ($sid$ == -1) /* From client. */
33 |  send($cid,\langle{\tt NACK},\bot,my\\_sid\rangle$);
34 |  else /* From server */
35 |  send($sid,\langle{\tt NACK},\bot,cid,my\\_sid,\bot\rangle$);
36 |  $\\}$ else $\\{$ /* Server moves the tail token to the next server */
37 |  $nsid$ = find_next_server($my\\_sid$);
38 |  $fullQueue$ = false;
39 |  $hasTail$ = false;
40 |  send($nsid,\langle op,data,cid,my\\_sid,{\tt TAIL\\_TOKEN}\rangle$);
|  $\\}$
41 |  break;
42 |  case DEQ:
---|---
43 |  if ($tk$ == HEAD_TOKEN) $\\{$
44 |  $hasHead$ = true;
45 |  ServeOldDequeues();
|  $\\}$
46 |  if (!$hasHead$) $\\{$
47 |  $nsid$ = find_next_server($my\\_sid$);
48 |  if ($sid==-1$) $\\{$ /* From client */
49 |  clients[$cid$] = $\langle{\tt DEQ},\bot,{\tt false}\rangle$;
50 |  send($nsid,\langle{\tt DEQ},\bot,cid,my\\_sid\rangle$);
51 |  $\\}$ else $\\{$ /* From server */
52 |  send($nsid,\langle{\tt DEQ},\bot,cid,sid,\bot\rangle$);
|  $\\}$
53 |  $\\}$ else if (!IsEmpty($lqueue$)) $\\{$ /* Server can dequeue. */
54 |  $data$ = dequeue($lqueue$);
55 |  if ($sid==-1$) /* From client */
56 |  send($cid,\langle{\tt ACK},data,my\\_sid\rangle$);
57 |  else /* From server */
58 |  send($sid,\langle{\tt ACK},data,cid,my\\_sid,\bot\rangle$);
59 |  $\\}$ else if ($hasTail$ AND !$fullQueue$) $\\{$ /* Queue is empty */
60 |  if ($sid==-1$) /* From client */
61 |  send($cid,\langle{\tt NACK},\bot,my\\_sid\rangle$);
62 |  else /* From server */
63 |  send($sid,\langle{\tt NACK},\bot,cid,my\\_sid,\bot\rangle$ );
64 |  $\\}$ else $\\{$ /* Server moves the head token to the next server */
65 |  $nsid$ = find_next_server($my\\_sid$);
66 |  $hasHead$ = false;
67 |  send($nsid,\langle op,\bot,cid,my\\_sid,{\tt HEAD\\_TOKEN}\rangle$);
|  $\\}$
68 |  break;
69 |  case ACK:
70 |  clients[$cid$] = $\bot$;
71 |  send($cid,\langle{\tt ACK},data,sid\rangle$);
72 |  break;
73 |  case NACK:
74 |  clients[$cid$] = $\bot$;
75 |  send($cid,\langle{\tt NACK},\bot,sid\rangle$);
76 |  break;
|  $\\}$
|  $\\}$

In Algorithm 13, we present the local variables of a server. Each server $s$
holds its unique id $my\\_sid$ and a local queue $lqueue$ that stores its part
of the queue. Also keeps two boolean flag variables, ($hasHead$ and
$hasTail$), indicating whether $s$ has the head token or the tail token, and
one more bit flag ($fullQueue$) indicating whether the queue is full. Finally,
$s$ has a local array of size $n$, where $n$ is the maximum number of clients,
used for storing all direct requests from clients (called $s$’s $clients$
array). In their initial state, all servers have $fullQueue$ set to false and
their $clients$ array and local queue empty. Also, all servers apart from
server 0, have both their flags $hasHead$ and $hasTail$ set to false, whereas
in server 0, they are set to true, as described above.

The messages sent to a server $s_{i}$ are of type ENQ or DEQ, describing
requests for enqueue or dequeue operations, respectively, sent by either a
server or a client, and ACK or NACK sent by another server $s_{j}$ which
executed a forwarded request, whose forwarding was initiated by $s_{i}$. The
token transition is encapsulated in a message of type ENQ or DEQ. The messages
have five fields: (1) $op$, which describes the type of the request (ENQ, DEQ,
ACK or NACK) , (2) $data$, which stores an element in case of ENQ, and $\bot$
otherwise, (3) $cid$, which stores the id of the client that issued the
request, (4) $sid$ which contains the id of the server if the message was sent
by a server, and -1 otherwise, and (5) $tk$, which contains TAIL_TOKEN or
HEAD_TOKEN in forwarded messages of type ENQ or DEQ, respectively, to indicate
if an additional tail (or head, respectively) token transition occurs, and it
is equal to $\bot$ otherwise.

Event-driven pseudocode for the server is presented in Algorithm 14. When a
server $s$ receives a message of type ENQ (line ln:a30-4), it first checks if
it contains a token transfer from another server (line ln:a30-36). If it does,
the server sets its token $hasTail$ to true (line ln:a30-37) and if it also
had the head token from a previous round, it changes $fullQueue$ flag to true
as well (line ln:a30-38). Then, $s$ serves all pending ENQ messages stored in
its $clients$ array (line ln:a30-39).

Then, $s$ continues to execute the ENQ request. It checks first whether it has
the tail token. If it does not (line ln:a30-9), it finds the next server
$s_{next}$ (line ln:a30-41), to whom $s$ is going to forward the request.
Afterwards, $s$ sends the received request to $s_{next}$ (lines ln:a30-13 and
ln:a30-14) and if that request came directly from a client (line ln:a30-11),
$s$ updates its $clients$ array storing in it information about this message
(line ln:a30-12).

If $s$ has the token, then it attempts to serve the request. If $s$ has
remaining space in its local queue ($lqueue$), it enqueues the given data and
informs the appropriate server with an ACK message (lines
ln:a30-6-ln:a30-5.1). If the implemented queue is full, $s$ sends a NACK
message to the client (line ln:a30-5-ln:a30-7.1). In any remaining case, the
server $s$ must give the tail token to the next server (line ln:a30-7). So,
$s$ forwards the ENQ message to $s_{next}$, after encapsulating in the message
the tail token (line ln:a30-10). After releasing the tail token, $s$ changes
the values of its local variables ($hasTail$ and $fullQueue$) to false.

In case a DEQ message is received (line ln:a30-15), the actions performed by
$s$ are similar to those for ENQ. Server $s$ checks whether the request
message contains a token transition (line ln:a30-33). If it does, the server
sets its token $hasHead$ to true (line ln:a30-34). Then, $s$ serves all
pending DEQ messages stored in its $clients$ array (line ln:a30-35), and then
attempts to serve the request. If $s$ does not hold the head token (line
ln:a30-23), it finds the next server $s_{next}$ in the ring (line ln:a30-19),
to whom $s$ is going to forward the request. Afterwards, $s$ sends the
received request to $s_{next}$ (lines ln:a30-25, ln:a30-26) and if that
request came directly from a client, $s$ updates its $clients$ array storing
in it information about this message (line ln:a30-24).

If $s$ has the head token, it does the following actions. If its local queue
($lqueue$) is not empty (line ln:a30-17), $s$ performs a dequeue on its local
queue and sends an ACK along with the dequeued data to the appropriate server.
If $s$ holds both head and tail tokens, but no other server has a queue
element stored, and $s$’s $lqueue$ is empty, it means that the global queue is
empty (line ln:a30-16). Thus, $s$ sends a NACK message to the appropriate
server. In the remaining cases, $s$ must forward its head token (line
ln:a30-18). Server $s$ finds the next server $s_{next}$ (line ln:a30-20),
which is going to receive the forwarded message and the head token transition.
Server $s$ sets the message field $tk$ to HEAD_TOKEN and sends the message
(line ln:a30-21). After releasing the head token, $s$ sets the value of its
local variable $hasHead$ to false (line ln:a30-22).

Algorithm 15 Auxiliary functions for a server of the token-based queue. 77 |  void ServeOldEnqueues(void) $\\{$
---|---
78 |  if (!$fullQueue$) $\\{$
79 |  for each $cid$ such that clients[$cid$].$op=={\tt ENQ}\ \\{$
80 |  if (!IsFull($lqueue$)) $\\{$
81 |  enqueue($lqueue$, clients[$cid$].$data$);
82 |  clients[$cid$].$isServed$ = true;
83 |  $\\}$ $\\}$ $\\}$ $\\}$
|
84 |  void ServeOldDequeues(void) $\\{$
85 |  for each $cid$ such that clients[$cid$].$op=={\tt DEQ}\ \\{$
86 |  if (!IsEmpty($lqueue$)) $\\{$
87 |  clients[$cid$].$data$ = dequeue($lqueue$);
88 |  clients[$cid$].$isServed$ = true;
|  $\\}$ $\\}$ $\\}$

If $s$ received a message of type ACK (line ln:a30-27) or NACK (line
ln:a30-30), then $s$ sets the entry $cid$ of its $clients$ array to $\bot$
(lines ln:a30-28, ln:a30-31) and sends an ACK (line ln:a30-29) or a NACK (line
ln:a30-32) to that client. The ACK and NACK messages a server $s$ receives,
are only sent by other servers and signify the result of the execution of a
forwarded message sent by $s$.

On lines ln:a30-12 and ln:a30-24, $s$ stores the client request in its
$clients$ array when it does not hold the appropriate token. A request
recorded in the $clients$ array is removed from the array either when an ACK
or NACK message is received for it (lines ln:a30-28 and ln:a30-31) or when the
server receives again the request (after a round-trip on the ring) (lines
ln:a30-1-ln:a30-2). Thus, the server, upon any message receipt, first checks
whether the message exists in its $clients$ array and has already been served.
In case of ENQ $s$ answers with an ACK message, whereas in case of DEQ $s$
answers with ACK and the dequeued data. Then, server $s$ proceeds with the
deletion of the entry in its clients array (lines ln:a30-1, ln:a30-2).

Functions ServeOldEnqueues() and ServeOldDequeues() are described in more
detail in Algorithm 15. ServeOldEnqueues() (line ln:a30h-1) processes all ENQ
requests stored in the $clients$ array, if the local queue has space (line
ln:a30h-3). Similarly, ServeOldDequeues() (line ln:a30h-4) processes all DEQ
requests stored in the $clients$ array, if the local queue is not empty (line
ln:a30h-5).

The clients call the functions ClientEnqueue() and ClientDequeue(), presented
in Algorithm 16, in order to perform one of these operations. In more detail,
during enqueue, the client sends an ENQ message to the $enq\\_sid$ server, and
waits for a response. When the client receives the response, it returns it.
Likewise, in ClientDequeue() the client sends a DEQ message to server
$deq\\_sid$ and blocks waiting for a response. When it receives the response,
it returns it.

Algorithm 16 Enqueue and Dequeue operations for a client of the token-based queue. 89 |  int $enq\\_sid=0$;
---|---
90 |  int $deq\\_sid=0$;
|
91 |  Data ClientEnqueue(int $cid$, Data $data$) $\\{$
92 |  send($enq\\_sid,\langle{\tt ENQ},data,cid,-1\rangle$);
93 |  $\langle status,\bot,enq\\_sid\rangle$ = receive($enq\\_sid$);
94 |  return $status$;
|  $\\}$
|
95 |  Data ClientDequeue(int $cid$) $\\{$
96 |  send($deq\\_sid,\langle{\tt DEQ},\bot,cid\rangle$);
97 |  $\langle status,data,deq\\_sid\rangle$ = receive($deq\\_sid$);
98 |  return $data$;
|  $\\}$

####  6.2.2 Proof of Correctness

Let $\alpha$ be an execution of the token-based queue algorithm presented in
Algorithms 14, 15, and 16. Each server maintains local boolean variables
$hasHead$ and $hasTail$, with initial values false. Whenever some server
$s_{i}$ receives a TAIL_TOKEN message, i.e. a message with its $tk$ field
equal to TAIL_TOKEN (line ln:a30-36), the value of $hasTail$ is set to true
(line ln:a30-37). By inspection of the pseudocode, it follows that the value
of $hasTail$ is set to false if the local queue of $s_{i}$ is full (line
ln:a30-6, ln:a30-7- ln:a30-10.1); then, a TAIL_TOKEN message is sent to the
next server (line ln:a30-10). The same holds for $hasHead$ and HEAD_TOKEN
messages, i.e. messages with their $tk$ field equal to HEAD_TOKEN. Thus, the
following observations holds.

######  Observation 31.

At each configuration in $\alpha$, there is at most one server for which the
local variable $hasHead$ ($hasTail$) has the value true.

######  Observation 32.

In some configuration $C$ of $\alpha$, TAIL_TOKEN message is sent from a
server $s_{j}$, $0\leq j<{\tt NS}-1$, to a server $s_{k}$, where
$k=(j+1)\mod{{\tt NS}}$ only if the local queue of $s_{j}$ is full in $C$.
Similary, a HEAD_TOKEN message is sent from $s_{j}$ to $s_{k}$ only if the
local queue of $s_{j}$ is empty in $C$.

By inspection of the pseudocode, we see that a server performs an enqueue
(dequeue) operation on its local queue $lqueue$ either when executing line
ln:a30-61 (line ln:a30-35) or when executing ServeOldEnqueues
(ServeOldDequeues). Further inspection of the pseudocode (lines
ln:a30-36-ln:a30-39, lines ln:a30-6-ln:a30-5, as well as lines
ln:a30-23-ln:a30-26, lines ln:a30-17-ln:a30-16), shows that these lines are
executed when $hasTail={\tt true}$. Then, the following observation holds.

######  Observation 33.

Whenever a server $s_{j}$ performs an enqueue (dequeue) operation on its local
queue, it holds that its local variable $hasTail$ ($hasHead$) is equal to
true.

By a straight-forward induction, the following lemma can be shown.

######  Lemma 34.

The mailbox of a client in any configuration of $\alpha$ contains at most one
incoming message.

If $hasTail={\tt true}$ ($hasHead={\tt true}$) for some server $s$ in some
configuration $C$, then we say that $s$ has the tail (head) token. The server
that has the tail token is referred to as tail token server. The server that
has the head token is referred to as head token server.

Let $op$ be any operation in $\alpha$. We assign a linearization point to $op$
by considering the following cases:

  * •

If $op$ is an enqueue operation for which a tail token server executes an
instance of Algorithm 14, then it is linearized in the configuration resulting
from the execution of either line ln:a30-61, or line ln:a30h-31, or line
ln:a30-51, whichever is executed for $op$ in that instance of Algorithm 14 by
the tail token server.

  * •

If $op$ is a dequeue operation for which a head token server executes an
instance of Algorithm 14, then it is linearized in the configuration resulting
from the execution of either line ln:a30-26.1, or line ln:a30h-51, or line
ln:a30-16.1, whichever is executed for $op$ in that instance of Algorithm 14
by the head token server.

######  Lemma 35.

The linearization point of an enqueue (dequeue) operation $op$ is placed in
its execution interval.

###### Proof.

Assume that $op$ is an enqueue operation and let $c$ be the client that
invokes it. After the invocation of $op$, $c$ sends a message to some server
$s$ (line ln:cl-enq:01) and awaits a response. Recall that routine receive()
(line ln:cl-enq:02) blocks until a message is received. The linearization
point of $op$ is placed either in the configuration resulting from the
execution of line ln:a30-61 by $s_{t}$ for $op$, in the configuration