From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by sympa.inria.fr (Postfix) with ESMTPS id 091A87EE20 for ; Wed, 14 Nov 2012 17:24:19 +0100 (CET) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of filippo.bonchi@ens-lyon.fr) identity=pra; client-ip=140.77.51.2; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="filippo.bonchi@ens-lyon.fr"; x-sender="filippo.bonchi@ens-lyon.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of filippo.bonchi@ens-lyon.fr designates 140.77.51.2 as permitted sender) identity=mailfrom; client-ip=140.77.51.2; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="filippo.bonchi@ens-lyon.fr"; x-sender="filippo.bonchi@ens-lyon.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@jabiru.ens-lyon.fr) identity=helo; client-ip=140.77.51.2; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="filippo.bonchi@ens-lyon.fr"; x-sender="postmaster@jabiru.ens-lyon.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgUIANPEo1CMTTMCf2dsb2JhbABEsUABkXUIIwEBCwsKCBQngz0HXRIBBQGIPwuZbIJvnlmMRYYUA5V8jmIWKYQS X-IronPort-AV: E=Sophos;i="4.83,251,1352070000"; d="scan'208";a="162470110" Received: from jabiru.ens-lyon.fr ([140.77.51.2]) by mail4-smtp-sop.national.inria.fr with ESMTP; 14 Nov 2012 17:24:18 +0100 Received: from localhost (localhost [127.0.0.1]) by jabiru.ens-lyon.fr (Postfix) with ESMTP id 765F71EB315 for ; Wed, 14 Nov 2012 17:24:18 +0100 (CET) X-Virus-Scanned: by amavisd-new-2.6.4 (20090625) (Debian) at ens-lyon.fr Received: from jabiru.ens-lyon.fr ([127.0.0.1]) by localhost (jabiru.ens-lyon.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id RWX9zGuhvEsd for ; Wed, 14 Nov 2012 17:24:18 +0100 (CET) Received: from mail-lb0-f182.google.com (mail-lb0-f182.google.com [209.85.217.182]) (using TLSv1 with cipher RC4-SHA (128/128 bits)) (Client CN "smtp.gmail.com", Issuer "Google Internet Authority" (verified OK)) by jabiru.ens-lyon.fr (Postfix) with ESMTPSA id DD5A41EB293 for ; Wed, 14 Nov 2012 17:24:17 +0100 (CET) Received: by mail-lb0-f182.google.com with SMTP id gg13so953506lbb.27 for ; Wed, 14 Nov 2012 08:24:17 -0800 (PST) MIME-Version: 1.0 Received: by 10.112.9.199 with SMTP id c7mr10941072lbb.70.1352910257080; Wed, 14 Nov 2012 08:24:17 -0800 (PST) Received: by 10.114.37.67 with HTTP; Wed, 14 Nov 2012 08:24:17 -0800 (PST) Date: Wed, 14 Nov 2012 17:24:17 +0100 Message-ID: From: Filippo Bonchi To: caml-list@inria.fr Content-Type: multipart/alternative; boundary=e0cb4efe2f16494bd204ce76f756 Subject: [Caml-list] Research School on "Semantics and tools for low-level programming" --e0cb4efe2f16494bd204ce76f756 Content-Type: text/plain; charset=ISO-8859-1 ************************************************************************ Research School on "Semantics and tools for low-level programming" January 14-18, 2013, ENS Lyon ************************************************************************ Speakers: Francesco Zappa Nardelli (INRIA), Mark Batty (University of Cambridge), Alastair Donaldson(Imperial College London) and Martin Vechev (ETH Zurich) Webpage: http://www.ens-lyon.fr/DI/?p=2803&lang=en Local Contact: Filippo Bonchi The registration is free and closes Monday 8th of January. Abstract: Optimisations performed by the hardware or by high-level language compilers can reorder memory accesses in various subtle ways. These reorderings can sometimes be observed by concurrent programs, exacerbating the usual problems of concurrent programming. The situation is even worse when we abandon traditional shared memory concurrency in favor of graphics processing units (GPUs) or exotic hardware. In these lectures we will cover recent progress in understanding and specifying the behaviour of some major processor architectures and the impact of optimisations performed by high-level programming language compilers, stablishing a solid basis for shared memory programming. We will then explore techniques which can help programmers develop reliable concurrent software by automatically discovering the necessary synchronization. We will also discuss techniques for verification of multicore software, including GPU kernels. --e0cb4efe2f16494bd204ce76f756 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable ************************************************************************Research School on "Semantics and tools for low-level programming&quo= t;
January 14-18, 2013, ENS Lyon
************************************= ************************************

Speakers: Francesco Zappa Nardelli (INRIA), Mark Batty (University of C= ambridge), Alastair Donaldson(Imperial College London) and Martin Vechev (E= TH Zurich)

Webpage: http://www.ens-lyon.fr/DI/?p=3D2803&lang=3Den
Local Contact: Filippo Bonchi
The registration is free and closes Monday= 8th of January.

Abstract:
Optimisations performed by the hardwar= e or by high-level language compilers can reorder memory accesses in variou= s subtle ways. These reorderings can sometimes be observed by concurrent pr= ograms, exacerbating the usual problems of concurrent programming. The situ= ation is even worse when we abandon traditional shared memory concurrency i= n favor of graphics processing units (GPUs) or exotic hardware. In these le= ctures we will cover recent progress in understanding and specifying the be= haviour of some major processor architectures and the impact of optimisatio= ns performed by high-level programming language compilers, stablishing a so= lid basis for shared memory programming. We will then explore techniques wh= ich can help programmers develop reliable concurrent software by automatica= lly discovering the necessary synchronization. We will also discuss techniq= ues for verification of multicore software, including GPU kernels.

--e0cb4efe2f16494bd204ce76f756--