Re: Consensus on MT-, AS- and AC-Safety docs.

[Alexandre Oliva <aoliva at redhat dot com>]

On Dec  1, 2013, Torvald Riegel <triegel@redhat.com> wrote:

> On Sun, 2013-12-01 at 00:45 -0200, Alexandre Oliva wrote:
>> On Nov 29, 2013, "Carlos O'Donell" <carlos@redhat.com> wrote:
>> 
>> > At present POSIX has no memory model,
>> 
>> It does.  In F2F conversation, Torvald retracted that assertion.

> Speak for yourself, or at least be precise when summarizing what someone
> else said.

I didn't try to summarize, just to highlight one point of the
conversation.  You said very explicitly that you didn't really mean that
POSIX had no memory model when you wrote that, you meant something else
and used this phrase as a shorthand.  Didn't you?

> I don't know who you think suggested to make the MT-Safe parametrized on
> the HW memory model,

Nobody did, and I didn't write anything even close to that.

I merely disputed the assertion that the MT-Safety definition had to
depend on the definition of another memory model, because if it did, we
couldn't possibly get a portable one: we'd have to have one definition
for each hardware memory model.  Conversely, if an abstracted-out
least-denominator memory model will do, then why wouldn't the existing
memory model be enough?

>> > and no strict definition of safe.

>> But there is an *exhaustive* list of all interfaces that are not
>> MT-Safe, and a rationale for this qualification.

> Are you saying that a list of cases that conflict with a certain
> criterium (e.g., MT-Safe) including some rationale why there is deemed
> to be a conflict equates a strict definition?

No.  The strict definition is there (but we know you don't like it); the
examples just illustrate the thread-safety pitfalls that were found and
addressed.

>> This, and the various
>> other requirements imposed to various functions throughout the standard,
>> makes the situations that raise safety issues and what POSIX expects
>> implementations to do to avoid them very clear.  The end result may not
>> be a perfect match for any of the transactional consistency models,

> You can't do without atomic entities at some level of the model.  In the
> worst case, 1-bit-wide accesses to memory will be atomic.

In hardware, the atomic access unit is a word, whose width C standards
define as the width of an int.

But..  Are we even speaking the same language?  I can't see how your
response relates to what I wrote.

> That doesn't conflict at all with having to reason about the parts
> that the functions are broken up into using atomicity and/or
> sequential specifications.

Unless there's no sequential specification as to the order of the parts
in which the execution is broken up.  They're specifically unordered and
may or may not be there.  Different implementation choices may very well
get not only a different number of parts, and different ordering between
them, but different intermediate and final states!

How about you show us how you'd model the POSIX-specified bsearch's or
qsort's alleged sequential specifications in your sequential-oriented
modeling language?

Take into account that the standard doesn't prohibit the compare
functions from keeping a counter of the number of times they're called,
and it doesn't mandate any specific order or algorithm.

Also take into account that, since the objects being compared are
expected to be read during the function execution, they must not be
modified concurrently (that would be a data race -> undefined behavior).
Therefore, they must remain constant throughout the execution of the
entire operation (except in case they are modified by the compare
function itself), which makes concurrent implementations perfectly
compliant with the standard, at least as long as they do not call the
compare function concurrently over the same object.

>> People have been able to make perfect sense of the MT-Safety notion
>> for at least 2 decades.

> Second, define "perfect sense" and prove your claim.

Several different operating systems, besides POSIX specifiers, all agree
on what it means.  Surely my claim is not to be mistaken for âeveryoneâ
has been able to make perfect sense of it.  We have a living
counter-example in this thread ;-)

> Then I guess you should have no problem giving us a proper
> definition :) 

I have.  You don't find it proper, but you won't show any concrete case
that casts any doubt on the meaning of the definition.  What can I do?
It makes perfect sense to me, and I can't read your mind to see what you
perceive as missing, so I can't possibly help improve it so as to cover
the issues you have doubts about.

> Or maybe you could give us a list of these other definitions

I don't think I still have access to any of the Solaris systems where I
first read it (I very much doubt they still exist :-) but if you have
access to any Solaris machines, you should be able to look up the
corresponding man page.  As clear as it was to me, I doubt it would
contain the provisions that would make it acceptable to you, for it
wouldn't imply what you seem to expect MT-Safe to imply.

Should you find it, please do NOT post it here unless its license would
permit us to adapt it for our own manual.  It might induce us to
involuntary copyright infringement.

> Also, why are you mentioning the years?

Because these concepts have been settled for a very long time.  I'd
think if there was such a major problem in them, someone at least as
smart as you would have already noticed it and fixed it.

> Memory models are discussed at least since the 70s, serializability is
> even older I believe, and linearizability is used since the early 90s.

Maybe you can point out how the literature you're familiar with defines
MT-Safe or Thread-Safe and how it relates with these other issues?
Maybe then we'll find out there is a difference in the meaning of terms
between different fields of research; we've already found some in our
earlier attempt to sort this out, but it had never occurred to me that
your research field might have defined Thread-Safety in a way that is
quite different, and even incompatible with the way operating systems
and POSIX use it.

-- 
Alexandre Oliva, freedom fighter    http://FSFLA.org/~lxoliva/
You must be the change you wish to see in the world. -- Gandhi
Be Free! -- http://FSFLA.org/   FSF Latin America board member
Free Software Evangelist      Red Hat Brazil Compiler Engineer