SWS   Info

Public Audience

English

60 Minutes

Kaiserslautern

In order to improve performance or conserve energy, modern hardware
implementations have adopted weak memory models; that is, models of
concurrency that allow more outcomes than the classic sequentially
consistent (SC) model of execution. Modern programming languages
similarly provide their own language-level memory models, which strive
to allow all the behaviors allowed by the various hardware-level memory
models, as well as those that can occur as a result of desired compiler
optimizations.

As these weak memory models are often rather intricate, it can be
difficult for programmers to keep track of all the possible behaviors of
their programs. It is therefore very useful to have an abstraction layer
over the model that can be used to ensure program correctness without
reasoning about the underlying memory model. Program logics are a way of
constructing such an abstraction—one can use their syntactic rules to
reason about programs, without needing to understand the messy details
of the memory model for which the logic has been proven sound.

Unfortunately, most of the work on formal verification in general, and
program logics in particular, has so far assumed the SC model of
execution. This means that new logics for weak memory have to be
developed.

This thesis presents two such logics—fenced separation logic (FSL) and
weak separation logic (Weasel)—which are sound for reasoning under two
different weak memory models.

FSL considers the C/C++ concurrency memory model, supporting several of
its advanced features. The soundness of FSL depends crucially on a
specific strengthening of the model which eliminates a certain class of
undesired behaviors (so-called out-of-thin-air behaviors) that
were inadvertently allowed by the original C/C++ model.

Weasel works under weaker assumptions than FSL, considering a model
which takes a more fine-grained approach to the out-of-thin-air problem.
Weasel's focus is on exploring the programming constructs directly
related to out-of-thin-air behaviors, and is therefore significantly
less feature-rich than FSL.

Using FSL and Weasel, the thesis explores the key challenges in
reasoning under weak memory models, and what effect different solutions
to the out-of-thin-air problem have on such reasoning. It explains which
reasoning principles are preserved when moving from a stronger to a
weaker model, and develops novel proof techniques to establish soundness
of logics under weaker models.

Maria-Louise Albrecht

+49 631 9303 9604

--email hidden

passcode not visible

logged in users only