Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Program Logic for Weak Memory Concurrency
Speaker:Marko Doko
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:SWS Student Defense Talks - Thesis Proposal
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Friday, 17 November 2017
Duration:-- Not specified --
Most of the verification techniques for concurrency assume the sequentially
consistent memory model, i.e., the executions of a concurrent program consist of
all the possible interleavings of the instructions of its threads. On the other
hand, in order to improve performance or conserve energy, modern hardware
implementations give us what is known as weak memory models; that is, models of
concurrency that allow some executions which cannot be explained by sequential
consistency. Moreover, modern programming languages provide their own
language-level memory models which strive to allow all the behaviors allowed by
the various hardware-level memory models and, additionally, to allow some
behaviors that can occur as a result of desired compiler optimizations.

These weak memory models are often quite intricate, and it can be quite
difficult for programmers to be aware of all the possible behaviors of their
programs. For this reason, it is very useful to have an abstraction layer over
the model, so that we can make sure our programs are correct without
understanding all the messy details of the underlying memory model. Program
logics are one way of constructing such an abstraction—they can present us with
clean and simple syntactical rules that we can use to reason about our programs,
while not requiring any understanding of the memory model for which the logic
has been proven sound.

In this thesis I develop FSL, a logic for reasoning about programs under the
memory model introduced by the 2011 standards for C and C++ programming
languages. FSL provides a set of clean and simple rules that abstract the
intricacies of the underlying model, while still being powerful enough to reason
about algorithms that appear in practice.

The main novelty of FSL is the ability to reason about synchronization via
memory fences, an advanced synchronization feature of the C11 memory model that
was not supported by any prior logic.
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
Maria-Louise Albrecht/MPI-KLSB, 11/16/2017 09:56 AM
Last modified:
Maria-Louise Albrecht/MPI-KLSB, 11/16/2017 10:00 AM
  • Maria-Louise Albrecht, 11/16/2017 10:00 AM -- Created document.