Chase–Lev deque

The Chase–Lev deque is the lock-free double-ended queue at the heart of most work-stealing schedulers. Each worker thread owns one deque of tasks: it pushes and pops tasks at the bottom, and idle workers steal tasks from the top of other workers' deques. The owner's operations use only ordinary reads and writes of two indices except when a single task is left, where the owner and a thief may both want it; both then resolve the race with a compare-and-swap on the top index, so exactly one of them wins. The buffer is a circular array that grows when full. Chase and Lev published it in 2005, as a growable version of the deque of Arora, Blumofe and Plaxton^[1]^[3]. It is used in the schedulers of Cilk-style runtimes, Java's fork/join framework, Rust's Crossbeam and Rayon, and OCaml 5's domainslib.

§ 01

Work stealing

A work-stealing scheduler runs a fork-join program on $P$ worker threads. A worker that spawns a task pushes it onto its own deque and continues; when it needs work, it pops from its own deque, and only when that is empty does it pick another worker at random and steal from the top of that worker's deque. Blumofe and Leiserson proved that for a computation with total work $T_{1}$ and critical-path length $T_{\infty}$ , this takes expected time^[4]:

T_{P} \leq \frac{T _{1}}{P} + O (T_{\infty})

with expected $O (P T_{\infty})$ steal attempts, so steals are rare when there is enough parallelism and almost all deque operations are the owner's own pushes and pops. The data structure is designed around that asymmetry: the owner's operations should cost almost nothing, and thieves may pay for synchronization.

Taking from opposite ends also helps performance. The bottom holds the most recently spawned tasks, whose data is still in the owner's cache; in a divide-and-conquer computation the top holds the oldest and therefore usually the largest pending subproblems, so one steal transfers a large amount of work.

§ 02

The algorithm

The deque has two indices, $top$ and $bottom$ , and a circular array. The elements are those at positions $top, \dots, bottom - 1$ . $top$ only ever increases, and only through compare-and-swap; only the owner writes $bottom$ . The indices are never wrapped; only the array position $i mod size$ is, so an index is never reused, and the compare-and-swap on $top$ cannot suffer from the ABA problem, whereas the fixed-size deque of Arora, Blumofe and Plaxton needed a tag in its top word to avoid it^[3]^[1].

Push writes the element at $bottom$ and then increments $bottom$ . Steal reads $top$ and then $bottom$ , and if the deque is not empty reads the element at $top$ and tries to increment $top$ with a compare-and-swap; if that fails, another thread took the element first. Pop first decrements $bottom$ , reserving the bottom element against thieves, and then reads $top$ . If more than one element remains, no thief can reach the reserved one, and the pop completes without synchronization. If exactly one remains, a thief may be taking it at the same moment, and the owner competes for it with the same compare-and-swap on $top$ that the thief uses.

The deque in OCaml, with a growable buffer, tested with three thieves.

(* The Chase-Lev work-stealing deque. The owner pushes and pops at the
   bottom; thieves steal from the top. top only ever increases. The buffer
   is circular and grows when full; indices are never wrapped, only the
   positions in the buffer are. *)
type 'a t = {
  top : int Atomic.t;
  bottom : int Atomic.t;
  buffer : 'a option array Atomic.t;
}
 
let create () = { top = Atomic.make 0; bottom = Atomic.make 0; buffer = Atomic.make (Array.make 16 None) }
 
let get buf i = buf.(i land (Array.length buf - 1))
let put buf i v = buf.(i land (Array.length buf - 1)) <- v
 
(* Owner only. *)
let push d v =
  let b = Atomic.get d.bottom and t = Atomic.get d.top in
  let buf = Atomic.get d.buffer in
  let buf =
    if b - t >= Array.length buf - 1 then begin
      (* Full: copy the live range into a buffer twice the size. Thieves
         still reading the old one see the same elements at the same
         indices. *)
      let bigger = Array.make (2 * Array.length buf) None in
      for i = t to b - 1 do put bigger i (get buf i) done;
      Atomic.set d.buffer bigger;
      bigger
    end else buf
  in
  put buf b (Some v);
  Atomic.set d.bottom (b + 1)
 
(* Owner only. *)
let pop d =
  let b = Atomic.get d.bottom - 1 in
  let buf = Atomic.get d.buffer in
  Atomic.set d.bottom b;
  let t = Atomic.get d.top in
  if t > b then (Atomic.set d.bottom (b + 1); None)          (* empty *)
  else
    let v = get buf b in
    if t < b then v                                          (* no race possible *)
    else begin
      (* One element left: race the thieves for it. *)
      let won = Atomic.compare_and_set d.top t (t + 1) in
      Atomic.set d.bottom (b + 1);
      if won then v else None
    end
 
(* Any thread. None means empty, or that another thread won the race. *)
let steal d =
  let t = Atomic.get d.top in
  let b = Atomic.get d.bottom in
  if t >= b then None
  else
    let v = get (Atomic.get d.buffer) t in
    if Atomic.compare_and_set d.top t (t + 1) then v else None

One run; the division between owner and thieves varies from run to run. The threads of OCaml 4 interleave but do not run in parallel; under OCaml 5 domains would.

200000 items: popped by the owner 110213, stolen 10703 + 27404 + 51680
every item taken exactly once: true;  final buffer size 128

Growing the buffer

When the array is full, push allocates one twice the size, copies the live elements to the same logical indices, and publishes it. A thief that read the old array still finds the correct element at its index, because the elements it can reach are copied, not moved, and the old array is not reused. In a garbage-collected language the old array is simply dropped when no thief refers to it; in C or C++ its reclamation needs care, and Chase and Lev discuss shrinking the array as well^[1].

§ 03

Checking the races

The difficult cases involve the owner and a thief acting on the last one or two elements at the same time. They can be checked exhaustively by modelling each operation as a sequence of single memory accesses and exploring every interleaving. The model below runs one pop against a thief making two steal attempts, on deques of one and two elements, under sequential consistency. It also runs two broken variants. In one the owner takes the last element without the compare-and-swap; in the other the owner reads $top$ before its write to $bottom$ takes effect:

An exhaustive model check of pop against two steals.

(* Explore every interleaving of the owner's pop with a thief that
   attempts two steals, one shared memory access per step, under
   sequential consistency. The deque starts with k elements; each element
   must end up taken exactly once or still in the deque. *)
type shared = { top : int; bottom : int }
 
(* A process is a program counter and local registers; a step reads or
   writes shared memory once and moves to the next pc. *)
type owner = { opc : int; ob : int; ot : int; oresult : int option option }
type thief = { tpc : int; tt : int; tb : int; tgot : int list; tleft : int }
 
type variant = Correct | No_cas | Reordered
 
let owner_step variant s o =
  match (variant, o.opc) with
  | Reordered, 0 -> (s, { o with opc = 1; ot = s.top })                 (* read top first *)
  | Reordered, 1 -> (s, { o with opc = 2; ob = s.bottom - 1 })
  | Reordered, 2 -> ({ s with bottom = o.ob }, { o with opc = 3 })
  | _, 0 -> (s, { o with opc = 1; ob = s.bottom - 1 })                  (* b = bottom - 1 *)
  | _, 1 -> ({ s with bottom = o.ob }, { o with opc = 2 })              (* bottom <- b *)
  | _, 2 -> (s, { o with opc = 3; ot = s.top })                         (* t = top *)
  | _, 3 ->
      if o.ot > o.ob then ({ s with bottom = o.ob + 1 }, { o with opc = 9; oresult = Some None })
      else if o.ot < o.ob || variant = No_cas then (s, { o with opc = 9; oresult = Some (Some o.ob) })
      else if s.top = o.ot then ({ s with top = o.ot + 1 }, { o with opc = 4; oresult = Some (Some o.ob) })  (* CAS wins *)
      else (s, { o with opc = 4; oresult = Some None })                  (* CAS loses *)
  | _, 4 -> ({ s with bottom = o.ob + 1 }, { o with opc = 9 })
  | _ -> assert false
 
let thief_step s th =
  let next th = if th.tleft > 1 then { th with tpc = 0; tleft = th.tleft - 1 } else { th with tpc = 9 } in
  match th.tpc with
  | 0 -> (s, { th with tpc = 1; tt = s.top })
  | 1 -> (s, { th with tpc = 2; tb = s.bottom })
  | 2 ->
      if th.tt >= th.tb then (s, next th)
      else if s.top = th.tt then ({ s with top = th.tt + 1 }, next { th with tgot = th.tt :: th.tgot })
      else (s, next th)
  | _ -> assert false
 
let owner_label variant pc =
  match (variant, pc) with
  | Reordered, 0 -> "O:t=top" | Reordered, 1 -> "O:b=bottom-1" | Reordered, 2 -> "O:bottom=b"
  | _, 0 -> "O:b=bottom-1" | _, 1 -> "O:bottom=b" | _, 2 -> "O:t=top" | _, 3 -> "O:take" | _ -> "O:bottom=b+1"
let thief_label = function 0 -> "T:t=top" | 1 -> "T:b=bottom" | _ -> "T:cas"
 
(* Depth-first search over all schedules; returns the number of complete
   schedules and the first one that loses or duplicates an element. *)
let explore variant k =
  let count = ref 0 and bad = ref None in
  let rec go s o th trace =
    let odone = o.opc = 9 and tdone = th.tpc = 9 in
    if odone && tdone then begin
      incr count;
      let got = Option.to_list (Option.join o.oresult) @ th.tgot in
      (* Elements still in the deque afterwards are those in [top, bottom). *)
      let remaining = List.init (max 0 (s.bottom - s.top)) (fun i -> s.top + i) in
      let all = List.sort compare (got @ remaining) in
      if all <> List.init k Fun.id && !bad = None then bad := Some (List.rev trace, o, th)
    end else begin
      if not odone then (let s', o' = owner_step variant s o in go s' o' th (owner_label variant o.opc :: trace));
      if not tdone then (let s', th' = thief_step s th in go s' o th' (thief_label th.tpc :: trace))
    end
  in
  go { top = 0; bottom = k } { opc = 0; ob = 0; ot = 0; oresult = None } { tpc = 0; tt = 0; tb = 0; tgot = []; tleft = 2 } [];
  (!count, !bad)

Running it. Each counterexample is a schedule, O for the owner's steps and T for the thief's.

Chase-Lev                              deque of 1: 366 schedules, all correct
Chase-Lev                              deque of 2: 336 schedules, all correct
without the CAS on the last element    deque of 1: 210 schedules, FAILS:
    O:b=bottom-1 T:t=top T:b=bottom O:bottom=b O:t=top O:take T:cas T:t=top T:b=bottom T:cas
    owner got element 0, thief got element 0
without the CAS on the last element    deque of 2: 210 schedules, FAILS:
    O:b=bottom-1 T:t=top T:b=bottom T:cas T:t=top T:b=bottom O:bottom=b O:t=top O:take T:cas
    owner got element 1, thief got element 0 and element 1
owner reads top before writing bottom  deque of 1: 441 schedules, all correct
owner reads top before writing bottom  deque of 2: 231 schedules, FAILS:
    O:t=top O:b=bottom-1 T:t=top T:b=bottom T:cas T:t=top T:b=bottom O:bottom=b O:take T:cas
    owner got element 1, thief got element 0 and element 1

The algorithm is correct on every schedule. Without the compare-and-swap, the owner and the thief can both take the last element. The third variant is the interesting one. The owner's code performs its write to $bottom$ before its read of $top$ , but a processor with a store buffer can let the read overtake the write. The thief then does not see the reservation, and one element is taken twice. This is the store-load reordering that x86 processors perform^[10].

§ 04

Memory models

The algorithm as written assumes sequential consistency. On real hardware, pop needs a full fence between its write of $bottom$ and its read of $top$ , and steal needs its read of $top$ ordered before its read of $bottom$ . On x86, only the fence in pop costs anything. Lê, Pop, Cohen and Zappa Nardelli gave a version for the C11 memory model with the weakest atomic orderings that are correct, proved it correct, and measured it on weakly ordered ARM and POWER processors^[2]. In OCaml 5, operations on Atomic.t are sequentially consistent^[7], so the direct translation above is correct as written, at the price of a fence on every atomic write.

§ 05

Uses

Cilk's runtime used a closely related protocol, THE, in which a thief takes a lock and the owner only synchronizes when the deque may be empty^[5]. Lea's fork/join framework, the basis of Java's ForkJoinPool, uses work-stealing deques of the same design^[6]. Rust's crossbeam-deque, used by the Rayon data-parallelism library, and OCaml 5's domainslib implement the Chase–Lev deque. Hendler, Lev, Moir and Shavit gave a variant that allocates the deque in linked nodes instead of a single array^[9]. Textbook treatments are in Herlihy and Shavit^[8].

§ 06

History

Blumofe and Leiserson established the theory of work stealing in the 1990s^[4], and Arora, Blumofe and Plaxton gave a non-blocking deque with a fixed-size array for it in 1998^[3]. The Cilk-5 runtime of the same year used the THE protocol^[5]. Chase and Lev's 2005 paper made the array circular and growable and removed the need for a tag^[1], and Lê, Pop, Cohen and Zappa Nardelli adapted it to weak memory models in 2013^[2].