References:
Multiprocessors are now pervasive and concurrent programming is becoming mainstream, but typical multiprocessors (x86, Sparc, Power, ARM, Itanium) and programming languages (C, C++, Java) do not provide the sequentially consistent shared memory that has been assumed by most work on semantics and verification. Instead, they have subtle relaxed (or weak) memory models, exposing behaviour that arises from hardware and compiler optimisations to the programmer. Moreover, these memory models have usually described only in ambiguous (and sometimes flawed) prose, leading to widespread confusion.
This page collects work by a group of people working to develop mathematically rigorous and usable semantics for multiprocessor programs. We are focussing on three processor architectures (x86, Power, and ARM), on the recent revisions of the C++ and C languages (C++11 and C11), and on reasoning and verification using these models.
x86-TSO is sound with respect to actual processor behaviour, matches the current vendor intentions, and is a good model to program above.
The low-level assembly-language implementations of the abstractions that support language-level concurrency, such as locks and concurrent data structures, are particularly interesting and challenging to reason about because they invariably contain data races.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?