Campus Event Calendar
Event Entry
What and Who
Formal Reasoning about Relaxed Concurrency
Viktor Vafeiadis
Max Planck Institute for Software Systems
Joint Lecture Series of MPI-INF, MPI-SWS and MMCI
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, 5 March 2014
12:15
60 Minutes
E1 5
002
Saarbrücken
Abstract
Despite what most reasoning techniques assume, concurrent programs
do run under sequentially consistency, but rather under a relaxed
memory model, such as the recent C/C++ model. There has been a lot
of work on specifying such relaxed models, but very little yet on
reasoning about programs under relaxed concurrency semantics.
Recently, at MPI-SWS, we have tackled this problem and developed
a bunch of relaxed program logics that encompass sound reasoning
principles for concurrent programs running under the C/C++ relaxed
memory model. The talk will provide a gentle introduction to
the C/C++ memory model and our newly developed reasoning principles.
do run under sequentially consistency, but rather under a relaxed
memory model, such as the recent C/C++ model. There has been a lot
of work on specifying such relaxed models, but very little yet on
reasoning about programs under relaxed concurrency semantics.
Recently, at MPI-SWS, we have tackled this problem and developed
a bunch of relaxed program logics that encompass sound reasoning
principles for concurrent programs running under the C/C++ relaxed
memory model. The talk will provide a gentle introduction to
the C/C++ memory model and our newly developed reasoning principles.
Contact
Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only
Kamila Kolesniczenko, 11/04/2013 14:32 -- Created document.