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

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                        Amphi Turing du bâtiment 1

                           Lundi 12 avril, 10h30

                               -------------
                               Gustavo Petri
                               -------------

                                   INRIA

              ===============================================
              Operational semantics for relaxed memory models
              ===============================================

The standard approach to describe the semantics of multi-threaded programs is
to consider all possible interleavings of the events generated by sequential
executions of each of its threads. However, in seek for better performance
many current multi-processor computer architectures optimize code in ways that
break the illusion of interleaved executions. These architectures provide, so
called, relaxed memory models.

Most relaxed memory model specifications are rather informal and/or axiomatic,
which makes them hard to understand and use for the programmer. In this talk I
will present two approaches: write buffering & speculation, that help to
overcome this problem, by providing operational semantics that account for
many of the effects introduced by relaxed memory models.