All the videos are available on the IRILL website:
A feedback of the conference has been published on the LLVM blog:
DebConf 11, the annual Debian conference took place in Banja Luka, Republika Srpska, Bosnia and Herzegovina. 56 talks or BoF have been recorded during this event:
DebConf 12 took place in Managua, Nicaragua. 72 talks or BoF have been recorded during this event, including many of them in Spanish.
Compilers sometimes generate correct sequential code but break the concurrency memory model of the programming language: these subtle compiler bugs are observable only when the miscompiled functions interact with concurrent contexts, making them particularly hard to detect. In this work we design a strategy to reduce the hard problem of hunting concurrency compiler bugs to differential testing of sequential code and build a tool that puts this strategy to work. Our first contribution is a theory of sound optimisations in the C11/C++11 memory model, covering most of the optimisations we have observed in real compilers and validating the claim that common compiler optimisations are sound in the C11/C++11 memory model. Our second contribution is to show how, building on this theory, concurrency compiler bugs can be identified by comparing the memory trace of compiled code against a reference memory trace for the source code. Our tool identified several mistaken write introductions and other unexpected behaviours in the latest release of the gcc compiler.
Monday, April 29th
|11:00 - 13:00||Entrance||Registration|
|12:30 - 13:15||ENS restaurant||Lunch|
|13:14 - 13:30||Dussane||Welcome - Day 1|
|13:30 - 14:30||Dussane||Keynote : Optimization in LLVM - Numbers, A Case Study, and Looking Forward|
|14:30 - 15:15||Dussane||Talk : Towards OpenMP Support in LLVM|
|Résistants||Talk : Dagger: decompilation to LLVM IR|
|15:15 - 15:45||Coffee break|
|15:45 - 16:30||Dussane||Talk : LLVM on IBM POWER processors: a progress report|
|Résistants||Talk : Performing Source-to-Source Transformations with Clang|
|16:30 - 17:15||Dussane||Talk : How to implement an LLVM Assembler|
|Résistants||Talk : clang-format - Automatic formatting for C++|
|20:00 - 23:00||Dinner cruise on the Seine river, in Paris, for those who registered to the dinner|
Tuesday, April 30th
|8:45 - 9:00||Dussane||Welcome - Day 2|
|9:00 - 10:00||Dussane||Keynote : How Computers Work|
|10:00 - 10:45||Dussane||Talk : LLVM Interpreter, a key component in validation of OpenCL compilers|
|Résistants||Talk : Run-time tracking of uninitialized data with MemorySanitizer|
|10:45 - 11:05||Coffee break|
|11:05 - 12:05||Dussane||Lightning talks|
|12:05 - 12:35||Résistants||Posters|
|12:35 - 13:35||ENS restaurant||Lunch|
|13:35 - 14:20||Dussane||Talk : lld - Solving the Linking Performance Problem|
|Résistants||Talk : An experimental framework for Pragma Handling in Clang|
|14:20 - 15:05||Dussane||Talk : Debug Info - Status and Directions|
|Résistants||Talk : Implementing Data Layout Optimizations in LLVM Framework|
|15:05 - 16:05||Dussane||Tutorial : The Clang AST - a tutorial|
|16:05 - 16:20||Dussane||Closing word|
The event is sponsored by ARM, Google, IRILL/INRIA, Intel, Parrot, QuIC, Samsung
L'année dernière avait lieu la première session de la journée de conférence et discussion Logiciels libres et enseignement supérieur.
IRILL est heureux de diffuser les 9 présentations qui ont eu lieu lors de cet événement: http://www.irill.org/videos/education-et-FLOSS
From the beginning, the Ada language was designed for critical software. It is still mostly used for the development of such systems. To facilitate the expression of requirements for the verification of programs, the last update of the Ada language includes new capabilities, such as contracts on functions or type invariants. With the increase cost of unit testing, the certification standards are opening to formal methods as a new way to address verification activities. Therefore, more and more users are interested in using formal methods for verifying part of their software.
In this talk, we present the upcoming version of the SPARK subset of Ada. It aims at easily allowing formal analysis on parts of an Ada program. We then give some hints on how formal verification is conducted in this tool. Finally, we explain how formal proof can be used in combination with more traditional testing.
Vous êtes étudiant ? Ingénieur jeune diplômé ? Le développement logiciel open source vous passionne ? Cette année encore, inria vous donne l'opportunité avec le concours Boost Your Code de présenter votre projet à un jury de scientifiques et de professionnels. Et toujours à la clé, un contrat d'un an pour développer votre projet au sein de notre Institut.
Free and Open Source Software (FOSS) has become an important source of components to reuse, in both commercial and non commercial software. While these components are free (i.e. gratis) they are made available with a license that indicates the conditions under which it can be used. As a consequence, the license of a component might restrict how it can be reused. In this talk I'll describe our recent work regarding reuse of FOSS components:
- The problem of provenance discovery in FOSS. Components are frequently distributed in binary form, making it difficult to trace back their origin. In other cases code snippets are copied from one product to another. I'll describe Joa, a system that is capable of finding the provenance of Java classes in both binary and source code form.
- The problem of license compliance and auditing: how to determine if a software system is satisfying all the legal constraints imposed by the components it reuses. I'll describe Ninka, a system for license identification, and a model that puts together Joa and Ninka to do license compliance of Java applications
More: Daniel's blog
The goal is this event is to improve the performances of the various Mozilla software like Firefox or Thunderbird.
The event, internal to the Mozilla community, will take place at IRILL between the March 18 to the 22.