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.