lkml.org 
[lkml]   [2014]   [Feb]   [6]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [RFC][PATCH 0/5] arch: atomic rework
On Thu, 6 Feb 2014, Torvald Riegel wrote:

> > It seems that nobody really
> > agrees on exactly how the C11 atomics map to real architectural
> > instructions on anything but the trivial architectures.
>
> There's certainly different ways to implement the memory model and those
> have to be specified elsewhere, but I don't see how this differs much
> from other things specified in the ABI(s) for each architecture.

It is not clear to me that there is any good consensus understanding of
how to specify this in an ABI, or how, given an ABI, to determine whether
an implementation is valid.

For ABIs not considering atomics / concurrency, it's well understood, for
example, that the ABI specifies observable conditions at function call
boundaries ("these arguments are in these registers", "the stack pointer
has this alignment", "on return from the function, the values of these
registers are unchanged from the values they had on entry"). It may
sometimes specify things at other times (e.g. presence or absence of a red
zone - whether memory beyond the stack pointer may be overwritten on an
interrupt). But if it gives a code sequence, it's clear this is just an
example rather than a requirement for particular code to be generated -
any code sequence suffices if it meets the observable conditions at the
points where code generated by one implementation may pass control to code
generated by another implementation.

When atomics are involved, you no longer have a limited set of
well-defined points where control may pass from code generated by one
implementation to code generated by another - the code generated by the
two may be running concurrently.

We know of certain cases
<http://www.cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html> where there are
choices of the mapping of atomic operations to particular instructions.
But I'm not sure there's much evidence that these are the only ABI issues
arising from concurrency - that there aren't any other ways in which an
implementation may transform code, consistent with the as-if rule of ISO
C, that may run into incompatibilities of different choices. And even if
those are the only issues, it's not clear there are well-understood ways
to define the mapping from the C11 memory model to the architecture's
model, which provide a good way to reason about whether a particular
choice of instructions is valid according to the mapping.

> Are you familiar with the formalization of the C11/C++11 model by Batty
> et al.?
> http://www.cl.cam.ac.uk/~mjb220/popl085ap-sewell.pdf
> http://www.cl.cam.ac.uk/~mjb220/n3132.pdf

These discuss, as well as the model itself, proving the validity of a
particular choice of x86 instructions. I imagine that might be a starting
point towards an understanding of how to describe the relevant issues in
an ABI, and how to determine whether a choice of instructions is
consistent with what an ABI says. But I don't get the impression this is
yet at the level where people not doing research in the area can routinely
read and write such ABIs and work out whether a code sequence is
consistent with them.

(If an ABI says "use instruction X", then you can't use a more efficient
X' added by a new version of the instruction set. But it can't
necessarily be as loose as saying "use X and Y, or other instructions that
achieve semantics when the other thread is using X or Y", because it might
be the case that Y' interoperates with X, X' interoperates with Y, but X'
and Y' don't interoperate with each other. I'd envisage something more
like mapping not to instructions, but to concepts within the
architecture's own memory model - but that requires the architecture's
memory model to be as well defined, and probably formalized, as the C11
one.)

--
Joseph S. Myers
joseph@codesourcery.com


\
 
 \ /
  Last update: 2014-02-07 00:21    [W:0.143 / U:0.268 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site