Campus Event Calendar
Event Entry
What and Who
Program Logic for Weak Memory Concurrency
Marko Doko
MMCI
SWS Student Defense Talks - Thesis Proposal
SWS
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 17 November 2017
15:00
-- Not specified --
G26
111
Kaiserslautern
Abstract
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.
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.
Contact
--email hidden
passcode not visible
logged in users only
Maria-Louise Albrecht, 11/16/2017 10:00 -- Created document.