To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Moscova - 01/06/06 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
             http://pauillac.inria.fr/seminaires/subscribe.html

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                     Salle de conférences du bâtiment 7

			    Jeudi 1er juin, 10h30

                               --------------
                               Matt Parkinson
                               --------------

                          University of Cambridge

         ==========================================================
         Concurrent Separation Logic: a message from the front line
         ==========================================================

In this talk I will present two areas that I have been extending  
separation logic in: (1) using * to separate stack variables; and (2)  
verifying non-blocking algorithms.

(1) Normally in separation logic * separates the heap, and we inherit  
the side-conditions of standard Hoare logic to deal with the program  
variables. However, in the concurrent setting these side-conditions  
are overly restrictive and  prevent us verifying many safe programs.  
By extending the logic to use * to separate variables, we can soundly  
remove the side-conditions and verify a wider class of programs.

(2) O'Hearn has shown concurrent separation logic can reason  
elegantly about blocking concurrency. I will show how this same  
reasoning can be applied to non-blocking concurrency, and discuss two  
examples Simpson's 4-slot algorithm for implementing a wait-free  
register, and Maged Michael's non-blocking stack using Hazard pointers.