Campus Event Calendar
Event Entry
What and Who
Relaxed memory concurrency and verified compilation
Viktor Vafeiadis
Max Planck Institut for Software Systems
Joint MPI-INF/MPI-SWS Lecture Series
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 13 June 2012
12:15
60 Minutes
E1 3 - Hörsaal Gebäude
HS 002
Saarbrücken
Abstract
The talk will cover two topics: (1) relaxed memory concurrency
and (2) verified compilation. I will introduce each topic
separately, and answer the questions such as the following:
- What does it mean for a compiler to be correct?
- What are relaxed memory models?
- How do you compile from one memory model to another? (e.g., from C++11 to x86-TSO)
- What compiler optimisations are valid?
- How do you actually prove such a compiler correct?
During the talk, I will refer to CompCertTSO, a verified compiler
from (relaxed memory concurrent) C to x86.
and (2) verified compilation. I will introduce each topic
separately, and answer the questions such as the following:
- What does it mean for a compiler to be correct?
- What are relaxed memory models?
- How do you compile from one memory model to another? (e.g., from C++11 to x86-TSO)
- What compiler optimisations are valid?
- How do you actually prove such a compiler correct?
During the talk, I will refer to CompCertTSO, a verified compiler
from (relaxed memory concurrent) C to x86.
Contact
Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 03/27/2012 11:02 -- Created document.