Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                          Salle Lions 1, bâtiment C
                             Lundi 15 mai, 10h30

                                Clément Allain
                                 Inria Paris

              Verification of the Chase-Lev work-stealing deque

A parallel scheduler is in charge of running the tasks that make up a
parallel computation on a pool of processors. It implements a
scheduling policy that governs how these tasks are divided among the
processors. Work-stealing is a popular scheduling policy in which an
idle processor may steal tasks from others, thereby performing load
balancing. In a typical work-stealing algorithm, each processor owns a
concurrent deque (double-ended queue) storing its ready tasks. This
deque features three operations. The owner may [push] and [pop] at its
end of the deque while the thieves may [steal] at the other end. This
talk will present ongoing work on the verification of the Chase-Lev
work-stealing deque. This data structure is implemented in the
[lockfree] OCaml 5 library and used in the [domainslib] library. We
will give an overview of the proof in Iris, taking advantage of ghost
state and prophecy variables with memory.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                     https://bbb.inria.fr/pot-xb8-cq4-y6w