Re: [RFC][PATCH 0/5] arch: atomic rework

[Joseph S. Myers]

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@xxxxxxxxxxxxxxxx
--
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/