\documentclass[dvips,11pt]{article}

\usepackage{listings}
\usepackage{fullpage}
\usepackage{color}
\usepackage[all]{xy}

\newtheorem{definition}{Definition}
\newtheorem{theorem}[definition]{Theorem}

\begin{document}

\lstset{language=java,mathescape=true,numbers=left,numberstyle=\tiny}

\title{Concurrent Red-Black Trees} 
\author{Franck van Breugel\\
        Department of Computer Science and Engineering, York University\\
        4700 Keele Street, Toronto, Ontario, Canada, M3J 1P3}
\date{\today}
\maketitle

\begin{abstract}
Three concurrent implementations of red-black trees are presented.
Only the operations \lstinline{Contains} and \lstinline{Add} are
considered.  The first implementation exploits monitors.  The second
implementation is based on a solution of the readers-writers problem,
where the readers are threads that perform the \lstinline{Contains} 
operation and the writers are the threads that perform the \lstinline{Add} 
operation.  The third implementation is an adaptation of the concurrent 
implementation of AVL trees by Ellis to the setting of red-black trees.  
In this implementation, the threads lock nodes of the tree.  A node can 
be locked in three different ways and different threads can have a lock
on a node simultaneously.
\end{abstract}

\section{Introduction}

Data structures such as sets can be efficiently implemented by means of 
red-black trees.  For example, the class \lstinline{TreeSet} of the
package \lstinline{java.util} of the Java standard library has been 
implemented by means of a red-black tree.  A red-black tree is a special 
type of binary search tree.  Such a tree is approximately balanced by 
colouring the nodes of the tree and placing certain restrictions on the 
way the nodes can be coloured.  

With the arrival of multicore machines, there is a need for concurrent
implementations of fundamental data structures such as sets.  In this
paper, we present a sequential implementation and three different 
concurrent implementations of red-black trees.  We first present the
sequential implementation as can be found in 
\cite{CormenLeisersonRivest89}.  The first concurrent implementation
is a simple modification of the sequential implementation by 
representing the red-black tree as a monitor.  The second concurrent
implementation allows for more concurrency by modifying a solution to 
the readers-writers problem \cite{CourtoisHeymansParnas71}.  The
third and final concurrent implementation uses fine grain locking
to allow even more concurrency.  In this implementation, we adapt the 
approach proposed by Ellis \cite{Ellis80} for concurrent AVL trees to 
red-black trees.

\section{Red-Black Trees}
\label{section:red-black-tree}

We assume that the reader is familiar with binary search trees (their 
definition can be found in, for example, 
\cite[Section~13.1]{CormenLeisersonRivest89}).  A red-black tree is a 
binary search tree where each node has a colour.  A node is either 
coloured red or black.  By restricting the way nodes can be coloured, 
the tree becomes approximately balanced.  These trees were first
introduced as symmetric binary B-trees by Bayer \cite{Bayer72}.  
Guibas and Sedgewick \cite{GuibasSedgewick78} characterized these
trees by colouring the nodes red or black, leading to the following
definition.

\begin{definition}
\label{definition:red-black-tree}
A {\sl red-black tree} is a binary search tree where each node is
either coloured red or black and
\begin{itemize}
\item
the root is black,
\item
each leaf is black,
\item
if a node is red, then both its children are black, and
\item
for every node, every path from that node to a leaf contains the same 
number of black nodes.
\end{itemize}
\end{definition}

For example, the binary search tree
$$
\UseComputerModernTips
\xymatrix{
&& *+<2ex>[o][F**:black][white]{3} \ar[dl] \ar[dr]\\
& *+<2ex>[o][F**:red][white]{1} \ar[dl] \ar[dr] && *+<3ex>[o][F**:black]{}\\
*+<3ex>[o][F**:black]{} && *+<3ex>[o][F**:black]{}}
$$
is a red-black tree.  Note that only the internal nodes contain elements.  
Red-black trees have the following key property.

\begin{theorem}
A red-black tree with $n$ internal nodes has height at most
$2 \log_2(n + 1)$.
\end{theorem}

A proof of this result can be found in, for example,
\cite[Section~14.1]{CormenLeisersonRivest89}.  Since a red-black tree is 
approximately balanced, the operations \lstinline{Contains} and 
\lstinline{Add} can be implemented efficiently.  More precisely, both 
\lstinline{Contains} and \lstinline{Add} can be implemented in 
$O(\log_2(n))$, where $n$ is the number of internal nodes of the red-black 
tree.

\section{Sequential Implementation}

The \lstinline{Contains} operation for red-black trees can be implemented 
in exactly the same way as for binary search trees.  Its pseudocode can be 
found in Appendix~\ref{appendix:sequential}.

Also the \lstinline{Add} operation for red-black trees is similar to that 
for binary search trees.  If the element $e$, which is to be added, is not 
already part of the red-black tree, then the appropriate leaf is replaced 
with the tree
$$
\UseComputerModernTips
\xymatrix{
& *+<2ex>[o][F**:red][white]{e} \ar[dl] \ar[dr]\\
*+<3ex>[o][F**:black]{} && *+<3ex>[o][F**:black]{}}
$$
This modification does not violate condition~1, 2 and 4 of 
Definition~\ref{definition:red-black-tree}, but it may violate condition~3. 
To reestablish this condition, the colour of some of the nodes may have to 
be changed and the structure of the tree may have to be modified.  The 
details can be found in Appendix~\ref{appendix:sequential}.  For example, 
if we add the element~2 to the red-black tree depicted in 
Section~\ref{section:red-black-tree}, then we first replace the right child 
of the node containing the element~1 with the tree
$$
\UseComputerModernTips
\xymatrix{
& *+<2ex>[o][F**:red][white]{2} \ar[dl] \ar[dr]\\
*+<3ex>[o][F**:black]{} && *+<3ex>[o][F**:black]{}}
$$
obtaining the tree
$$
\UseComputerModernTips
\xymatrix{
&& *+<2ex>[o][F**:black][white]{3} \ar[dl] \ar[dr]\\
& *+<2ex>[o][F**:red][white]{1} \ar[dl] \ar[dr] && *+<3ex>[o][F**:black]{}\\
*+<3ex>[o][F**:black]{} && *+<2ex>[o][F**:red][white]{2} \ar[dl] \ar[dr]\\
& *+<3ex>[o][F**:black]{} && *+<3ex>[o][F**:black]{}}
$$
Note that this is not a red-black tree, since the red node labelled~1 has a 
red child.  After restructuring the tree, we obtain the following red-black 
tree.
$$
\UseComputerModernTips
\xymatrix{
&&& *+<2ex>[o][F**:black][white]{2} \ar[dll] \ar[drr]\\
& *+<2ex>[o][F**:red][white]{1} \ar[dl] \ar[dr] &&& & *+<2ex>[o][F**:red][white]{3} \ar[dl] \ar[dr]\\
*+<3ex>[o][F**:black]{} && *+<3ex>[o][F**:black]{} && *+<3ex>[o][F**:black]{} && *+<3ex>[o][F**:black]{}}
$$

We believe that multiple threads manipulating a red-black tree concurrently 
using the operations \lstinline{Contains} and \lstinline{Add} may lead to 
counter-intuitive results.  Consider the following concurrent program.
\begin{lstlisting}
Add(3)
Add(1)
(Add(2) $\parallel$ Contains(1))
\end{lstlisting}
Starting from an empty red-black tree, we first add the elements~3 and 1.  
This results in the red-black tree depicted in the previous section.  
Subsequently, one threads adds the element~2 whereas the other thread checks 
if the tree contains the element~1.  One would expect the \lstinline{Contains} 
operation to always return true.  However, we believe that by interleaving 
the elementary operations of the operations \lstinline{Add} and 
\lstinline{Contains} in a particular way, the operation \lstinline{Contains} 
may return false.  When the \lstinline{Add} operation modifies the structure 
of the tree, the \lstinline{Contains} operation may not be able to find the 
element~1.  We plan to confirm this conjecture by our implementation or our 
verification effort.  In the following sections, we present three ways to 
rule out this undesirable behaviour.

\section{The Monitors Approach}
\label{section:monitors}

A simple way to ensure that the \lstinline{Add} operation does not interfere 
with the \lstinline{Contains} operation is to implement the red-black tree as 
a monitor.  Monitors were introduced by Brinch Hansen and Hoare in 
\cite{BrinchHansen73,Hoare74}.  Below we use the syntax as used in \cite{Hoare74}.
\begin{lstlisting}[emph={begin,end,result,monitor,int},emphstyle=\bf]
RedBlackTree : monitor
begin
  root : node
  procedure contains (element : int, result contains : boolean)
  begin
    $\ldots$
  end
  procedure add (element : int, result added : boolean)
  begin
    $\ldots$
  end
  root := black node
end
\end{lstlisting}
Within the body of the procedures \lstinline{Contains} and \lstinline{Add} we 
place the code presented in Appendix~\ref{appendix:sequential}.  Since monitor 
procedures are always mutually exclusive, the \lstinline{Add} procedure never 
interferes with the \lstinline{Contains} procedure.

\section{The Readers-Writers Approach}
\label{section:readers}

The solution presented in the previous section ensures that one operation
at a time is performed on the red-black tree.  However, multiple
\lstinline{Contains} operations can be performed concurrently without giving 
rise to undesirable results.  To accomplish this, we can easily modify a 
solution to the readers-writers problem \cite{CourtoisHeymansParnas71}.  In 
our setting, the threads that perform the \lstinline{Contains} operation are 
the readers and the threads that perform the \lstinline{Add} operation are the
writers.  For a solution to the readers-writers problem in which no reader 
waits because a writer is waiting for other readers to finish, we refer the 
reader to \cite{CourtoisHeymansParnas71}.

\section{Locking Nodes}
\label{section:locking}

In an attempt to increase concurrency even more, we adapt the approach
proposed by Ellis \cite{Ellis80} for concurrent AVL trees to red-black trees.  

The key idea of this implementation is that individual nodes are locked.  A 
node can be locked in three different ways.  A thread that searches for an 
element (by performing the \lstinline{Contains} operation) $\rho$-locks a
node of the tree to ensure that the locked node is not part of a restructuring 
of the tree.  A thread that searches for a leaf to add an element (as part of 
the \lstinline{Add} operation) $\alpha$-locks a node of the tree to prevent 
another thread, which also wants to add an element, access to the subtree 
rooted at the locked node.  Just before a thread restructures the tree (as 
part of the \lstinline{Add} operation), it $\xi$-locks the nodes that are 
part of the restructuring.  This prevents other threads from accessing these
nodes.

Different threads can hold a lock on the same node at the same time.  
However, there are some restrictions.  The following graph \cite{Ellis80}
captures those restrictions.
$$
\UseComputerModernTips
\xymatrix@R=1ex{
*+<3ex>[o][F]{\rho} \ar@{-}@(ul,dl)[] \ar@{-}[rr] && *+<3ex>[o][F]{\alpha}\\
& *+<3ex>[o][F]{\xi}}
$$
If there is an edge between two lock types, then two threads can have
a lock of the given type on a particular node at the same time.  For 
example, multiple threads can $\rho$-lock a node and a single thread can 
$\alpha$-lock that node all at the same time.

\subsection{The \lstinline{Contains} Operation}

While searching for an element in the tree, we $\rho$-lock nodes on the path 
from the root of the tree to either a leaf (if the element is not stored in 
the tree) or the node containing the element.  We start to $\rho$-lock the 
root of the red-black tree.  Assume that, during the search, we have 
$\rho$-locked a particular node.  Before releasing the lock, we first 
$\rho$-lock the left or right child of that node.  This avoid should deadlock.  
We will try to confirm this with our implementation or verification effort.
The details of the implementation of the \lstinline{Contains} operation can be 
found in Section~\ref{section:contains}.

\subsection{The \lstinline{Add} Operation}

The \lstinline{Add} operation consists of two parts.  The first part is very 
similar to the \lstinline{Contains} operation.  In the first part, we locate 
the leaf where the element is to be inserted.  While searching for that leaf,
we $\alpha$-lock nodes on the path from the root to the leaf.  An $\alpha$-lock 
on a node prevents other threads, which also want to add elements to the tree, 
access to the subtree rooted at that node, so that this subtree can be modified.  
We want to keep this subtree as small as possible to allow as much concurrency 
as possible.  Initially, we $\alpha$-lock the root.  If we encounter two 
consecutive black nodes on the path from the root to the leaf, we know that the 
potential restructuring will be limited to the subtree rooted at first black 
node (the one closest to the root).  Hence, we $\alpha$-lock this node and we 
release the lock on the previously $\alpha$-locked node.  In this way, the 
subtree rooted at the $\alpha$-locked node becomes smaller, therefore, allowing 
more concurrency.

After we have inserted the element at a leaf of the tree, we may have to modify 
the structure of the tree and change the colour of some of the nodes.  These 
changes will be limited to the subtree rooted at the $\alpha$-locked node.  
Whenever, we change the structure of the tree, we $\xi$-lock all the nodes 
involved in the restructuring.  We lock them in a top-down fashion to avoid 
deadlock.

The details can be found in Section~\ref{section:add}.

\section{Conclusion}

A lot of work has been done on the concurrent implementation of data structures.  
We refer the reader to, for example, \cite{MoirShavit05} for an overview.  The 
concurrent red-black tree implementation described in Section~\ref{section:locking}
is an adaptation of the concurrent implementation of AVL trees as introduced by 
Ellis in \cite{Ellis80}.  Hanke \cite{Hanke99} also mentions that the implementation 
of Ellis can be adapted to red-black trees.  Nurmi and Soisalon-Soininen
\cite{NurmiSoisalonSoininen96} present a slightly different concurrent implementation 
of red-black trees.  Also their work is based on the original work of Ellis.

We have presented three concurrent implementations of red-black trees.  The 
implementation in Section~\ref{section:readers} allows for more concurrency than 
the one in Section~\ref{section:monitors}.  The implementation in 
Section~\ref{section:locking} gives rise to even more concurrency.  However, as the 
concurrency increases, so does the complexity of the implementation.  

There seem to be opportunities to increase the amount of concurrency of the 
implementation in Section~\ref{section:locking}.  First of all, rather than locking 
nodes, we could lock only ``half a node.''  For example, instead of locking a node, 
we can lock only its left part.  In this way, its right child is still available.
Secondly, there seem opportunities to decrease the lock granularity.  For example, 
line~73--87 of Section~\ref{section:add} can be modified as follows.
\begin{lstlisting}[literate={:=}{{$\gets$}}1,emph={then},emphstyle=\bf]
$\xi$-lock grandparent
$\xi$-lock parent
$\xi$-lock node
Left-Child(node, parent)
Right-Child(node, grandparent)
root := node
$\xi$-unlock node
Left-Child(grandparent, right)
$\xi$-unlock grandparent
Right-Child(parent, left)
$\xi$-unlock parent
\end{lstlisting}
Note that \lstinline{left} and \lstinline{right} are not locked at all.  Also notice 
that \lstinline{grandparent} and \lstinline{node} are locked for a ``smaller amount 
of time.''  Thirdly, we may attempt to avoid using locks completely by using
atomic operations such as ``compare and swap.''

\bibliographystyle{plain}
\bibliography{assignment1}

\appendix

\section{Pseudocode for the Sequential Implementation}
\label{appendix:sequential}

\subsection{Pseudocode for the \lstinline{Contains} Operation} 

The following pseudocode is based on the pseudocode found in
\cite[Section~13.2]{CormenLeisersonRivest89}.

\begin{lstlisting}[literate={:=}{{$\gets$}}1,emph={then},emphstyle=\bf]
Contains(e)
  found := false
  node := root
  while node is not a leaf $\wedge$ $\neg$ found do
    if e = element of node then
      found := true
    else if e < element of node then
      node := left child of node
    else
      node := right child of node
  return found
\end{lstlisting}

\subsection{Pseudocode for the \lstinline{Add} Operation} 

The following pseudocode is based on the pseudocode found in
\cite[Section~14.3]{CormenLeisersonRivest89}.  Before presenting the 
pseudocode for \lstinline{Add}, we first present some simple operations 
that will be used in the pseudocode for \lstinline{Add}.

The operation \lstinline{Left-Child(p, c)} ensures that the 
node~\lstinline{c} becomes the left child of the node~\lstinline{p}.
\begin{lstlisting}[literate={:=}{{$\gets$}}1]
Left-Child(p, c)
  parent of c := p
  left child of p := c
\end{lstlisting}

Similarly, the operation \lstinline{Right-Child(p, c)} ensures that 
the node~\lstinline{c} becomes the right child of the node~\lstinline{p}.
\begin{lstlisting}[literate={:=}{{$\gets$}}1]
Right-Child(p, c)
  parent of c := p
  right child of p := c
\end{lstlisting}

\begin{lstlisting}[literate={:=}{{$\gets$}}1,emph={then},emphstyle=\bf]
Add(e)
  found := false
  node := root
  while node is not a leaf $\wedge$ $\neg$ found do
    if e = element of node then
      found := true
    else if e < element of node then
      node := left child of node
    else
      node := right child of node
  if $\neg$ found then
    colour of node := red
    element of node := e
    left := black node
    right := black node
    Left-Child(node, left)
    Right-Child(node, right)
    while node $\not=$ root $\wedge$ parent of node is red do
      parent := parent of node
      grandparent := parent of parent
      if parent is left child of grandparent then
        aunt := right child of grandparent
        if aunt is red then
          colour of aunt := black
          colour of parent := black
          colour of grandparent := red
          node := grandparent
        else if node is left child of parent then
          colour of parent := black
          colour of grandparent := red
          sister := right child of parent
          Right-Child(parent, grandparent)
          Left-Child(grandparent, sister)
          if grandparent = root then
            root := parent
          else
            grandgrandparent := parent of grandparent
            if grandparent is a left child of grandgrandparent then
              Left-Child(grandgrandparent, parent)
            else
              Right-Child(grandgrandparent, parent)
        else (node is right child of parent)
          colour of node := black
          colour of grandparent := red
          left := left child of node
          right := right child of node
          Left-Child(node, parent)
          Right-Child(node, grandparent)
          Right-Child(parent, left)
          Left-Child(grandparent, right)
          if grandparent = root then
            root := node
          else
            grandgrandparent := parent of grandparent
            if grandparent is a left child of grandgrandparent then
              Left-Child(grandgrandparent, node)
            else
              Right-Child(grandgrandparent, node)
      else (parent is right child of grandparent)
        aunt := left child of grandparent
        if aunt is red then
          colour of aunt := black
          colour of parent := black
          colour of grandparent := red
          node := grandparent
        else if node is right child of parent then
          colour of parent := black
          colour of grandparent := red
          sister :=  left child of parent
          Left-Child(parent, grandparent)
          Right-Child(grandparent, sister)
          if grandparent = root then
            root := parent
          else
            grandgrandparent :=  parent of grandparent
            if grandparent is a left child of grandgrandparent then
              Left-Child(grandgrandparent, parent)
            else
              Right-Child(grandgrandparent, parent)
        else (node is left child of parent)
          colour of node := black
          colour of grandparent := red
          left := left child of node
          right := right child of node
          Right-Child(node, parent)
          Left-Child(node, grandparent)
          Left-Child(parent, right)
          Right-Child(grandparent, left)
          if grandparent = root then
            root := node
          else
            grandgrandparent := parent of grandparent
            if grandparent is a left child of grandgrandparent then
              Left-Child(grandgrandparent, node)
            else
              Right-Child(grandgrandparent, node)
  colour of root := black
  return $\neg$ found
\end{lstlisting}

Note that line~59--96 is the mirror image of line~21--58.

\section{Pseudocode for the Concurrent Implementation}
\label{appendix:concurrent}

We augment the pseudocode of Appendix~\ref{appendix:sequential}
with the locking of nodes.

\subsection{Pseudocode for the \lstinline{Contains} Operation} 
\label{section:contains}

We modify the implementation of the \lstinline{Contains} operation
as follows.
\begin{lstlisting}[literate={:=}{{$\gets$}}1,emph={then},emphstyle=\bf]
Contains(e)
  found := false
  node := root
  $\rho$-lock node
  while node is not a leaf $\wedge$ $\neg$ found do
    parent := node
    if e = element of node then
      found := true
    else if e < element of node then
      node := left child of node
    else
      node := right child of node
    $\rho$-lock node
    $\rho$-unlock parent
  $\rho$-unlock node
  return found
\end{lstlisting}
Note that line~4, 6, 13, 14 and 15 are new.

\subsection{Pseudocode for the \lstinline{Add} Operation} 
\label{section:add}

We modify the implementation of the \lstinline{Add} operation
as follows.
\begin{lstlisting}[literate={:=}{{$\gets$}}1,emph={then},emphstyle=\bf]
Add(e)
  found := false
  node := root
  $\alpha$-lock node
  locked := node
  while node is not a leaf $\wedge$ $\neg$ found do
    parent := node
    if e = element of node then
      found := true
    else if e < element of node then
      node := left child of node
    else
      node := right child of node
    if node and parent are black and parent $\not=$ locked then
      $\alpha$-lock parent
      $\alpha$-unlock locked
      locked := parent
  if $\neg$ found then
    $\xi$-lock node
    colour of node := red
    element of node := e
    left := black node
    right := black node
    Left-Child(node, left)
    Right-Child(node, right)
    $\xi$-unlock node
    while node $\not=$ root $\wedge$ parent of node is red do
      parent := parent of node
      grandparent := parent of parent
      if parent is left child of grandparent then
        aunt := right child of grandparent
        if aunt is red then
          colour of aunt := black
          colour of parent := black
          colour of grandparent := red
          node := grandparent
        else if node is left child of parent then
          colour of parent := black
          colour of grandparent := red
          sister := right child of parent
          if grandparent = root then
            $\xi$-lock grandparent
            $\xi$-lock parent
            $\xi$-lock sister
            root := parent
            Right-Child(parent, grandparent)
            Left-Child(grandparent, sister)
            $\xi$-unlock sister
            $\xi$-unlock parent
            $\xi$-unlock grandparent
          else
            grandgrandparent := parent of grandparent
            $\xi$-lock grandgrandparent
            $\xi$-lock grandparent
            $\xi$-lock parent
            $\xi$-lock sister
            if grandparent is a left child of grandgrandparent then
              Left-Child(grandgrandparent, parent)
            else
              Right-Child(grandgrandparent, parent)
            Right-Child(parent, grandparent)
            Left-Child(grandparent, sister)
            $\xi$-unlock sister
            $\xi$-unlock parent
            $\xi$-unlock grandparent
            $\xi$-unlock grandgrandparent
        else (node is right child of parent)
          colour of node := black
          colour of grandparent := red
          left := left child of node
          right := right child of node
          if grandparent = root then
            $\xi$-lock grandparent
            $\xi$-lock parent
            $\xi$-lock node
            $\xi$-lock left
            $\xi$-lock right
            root := node
            Left-Child(node, parent)
            Right-Child(node, grandparent)
            Right-Child(parent, left)
            Left-Child(grandparent, right)
            $\xi$-unlock right            
            $\xi$-unlock left
            $\xi$-unlock node
            $\xi$-unlock parent
            $\xi$-unlock grandparent
          else
            grandgrandparent := parent of grandparent
            $\xi$-lock grandgrandparent
            $\xi$-lock grandparent
            $\xi$-lock parent
            $\xi$-lock node
            $\xi$-lock left
            $\xi$-lock right
            if grandparent is a left child of grandgrandparent then
              Left-Child(grandgrandparent, node)
            else
              Right-Child(grandgrandparent, node)
            Left-Child(node, parent)
            Right-Child(node, grandparent)
            Right-Child(parent, left)
            Left-Child(grandparent, right)
            $\xi$-unlock right            
            $\xi$-unlock left
            $\xi$-unlock node
            $\xi$-unlock parent
            $\xi$-unlock grandparent
      else (parent is right child of grandparent)
        aunt := left child of grandparent
        if aunt is red then
          colour of aunt := black
          colour of parent := black
          colour of grandparent := red
          node := grandparent
        else if node is right child of parent then
          colour of parent := black
          colour of grandparent := red
          sister :=  left child of parent
          if grandparent = root then
            $\xi$-lock grandparent
            $\xi$-lock parent
            $\xi$-lock sister
            root := parent
            Left-Child(parent, grandparent)
            Right-Child(grandparent, sister)
            $\xi$-unlock sister
            $\xi$-unlock parent
            $\xi$-unlock grandparent
          else
            grandgrandparent := parent of grandparent
            $\xi$-lock grandgrandparent
            $\xi$-lock grandparent
            $\xi$-lock parent
            $\xi$-lock sister
            if grandparent is a left child of grandgrandparent then
              Left-Child(grandgrandparent, parent)
            else
              Right-Child(grandgrandparent, parent)
            Left-Child(parent, grandparent)
            Right-Child(grandparent, sister)
            $\xi$-unlock sister
            $\xi$-unlock parent
            $\xi$-unlock grandparent
            $\xi$-unlock grandgrandparent
        else (node is left child of parent)
          colour of node := black
          colour of grandparent := red
          left := left child of node
          right := right child of node
          if grandparent = root then
            $\xi$-lock grandparent
            $\xi$-lock parent
            $\xi$-lock node
            $\xi$-lock left
            $\xi$-lock right
            root := node
            Right-Child(node, parent)
            Left-Child(node, grandparent)
            Left-Child(parent, right)
            Right-Child(grandparent, left)
            $\xi$-unlock right
            $\xi$-unlock left
            $\xi$-unlock node
            $\xi$-unlock parent
            $\xi$-unlock grandparent
          else
            grandgrandparent := parent of grandparent
            $\xi$-lock grandgrandparent
            $\xi$-lock grandparent
            $\xi$-lock parent
            $\xi$-lock node
            $\xi$-lock left
            $\xi$-lock right
            if grandparent is a left child of grandgrandparent then
              Left-Child(grandgrandparent, node)
            else
              Right-Child(grandgrandparent, node)
            Right-Child(node, parent)
            Left-Child(node, grandparent)
            Left-Child(parent, right)
            Right-Child(grandparent, left)
            $\xi$-unlock right
            $\xi$-unlock left
            $\xi$-unlock node
            $\xi$-unlock parent
            $\xi$-unlock grandparent
            $\xi$-unlock grandgrandparent
  colour of root := black
  $\alpha$-unlocked locked
  return $\neg$ found
\end{lstlisting}

\end{document}
