This is the mail archive of the
mailing list for the glibc project.
Re: Consensus on MT-, AS- and AC-Safety docs.
- From: Torvald Riegel <triegel at redhat dot com>
- To: Alexandre Oliva <aoliva at redhat dot com>
- Cc: "Carlos O'Donell" <carlos at redhat dot com>, GNU C Library <libc-alpha at sourceware dot org>, "Joseph S. Myers" <joseph at codesourcery dot com>, Rich Felker <dalias at aerifal dot cx>
- Date: Mon, 02 Dec 2013 12:42:34 +0100
- Subject: Re: Consensus on MT-, AS- and AC-Safety docs.
- Authentication-results: sourceware.org; auth=none
- References: <528A7C8F dot 8060805 at redhat dot com> <52991C3B dot 9080701 at redhat dot com> <ord2lhjnku dot fsf at livre dot home> <1385921165 dot 3152 dot 11533 dot camel at triegel dot csb> <orvbz7iyqg dot fsf at livre dot home>
On Mon, 2013-12-02 at 03:54 -0200, Alexandre Oliva wrote:
> On Dec 1, 2013, Torvald Riegel <firstname.lastname@example.org> wrote:
> > On Sun, 2013-12-01 at 00:45 -0200, Alexandre Oliva wrote:
> >> On Nov 29, 2013, "Carlos O'Donell" <email@example.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?
Please speak for yourself.
> > 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
Either it takes care by itself of defining the aspects that a memory
model would cover otherwise, or it relies on another memory model.
> , because if it did, we
> couldn't possibly get a portable one:
If the memory model is portable, a definition relying on the model can
> we'd have to have one definition
> for each hardware memory model.
C11's memory model is certainly portable across different HW memory
> Conversely, if an abstracted-out
> least-denominator memory model will do, then why wouldn't the existing
> memory model be enough?
Because it's not a complete definition. And I obviously don't mean here
that it would be lacking atomics or such; it just doesn't define certain
things that need to be defined.
> >> > 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
So how was the "But there is an *exhaustive* list" meant? I read it as
the reason why Carlos' statement would be wrong. Did you mean to write
that as just a statement that there is such a list?
> (but we know you don't like it);
Don't try to put it as if this is all about what I *like* or not.
Obviously, others (such as Carlos) also see a lack of a strict
> examples just illustrate the thread-safety pitfalls that were found and
> >> 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.
I'm saying you can't do without atomicity in the model. I cite the
worst case that's needed to reason here. You say some HW has wider.
Fine. How does that conflict with what I said?
> But.. Are we even speaking the same language? I can't see how your
> response relates to what I wrote.
You said the "end result may not be a perfect match for any of the
transactional consistency models". Given that atomicity is core of many
transactional consistency criteria, I'm saying that you can't avoid the
atomicity aspect anyway. So, that there doesn't need to be a mismatch
> > 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.
That's fine too. If they are unordered, you get a few more options a
certain execution can play out, but once you're reasoning about any of
the parts, you're back to having to reason about sequential specs.
> 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!
Non-determinism is orthogonal to whether it's a sequential specification
(ie, in the form of pre/post condition).
> 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?
Other email thread please. Specifically, per Carlos' request, that
belongs into a thread about a full definition of MT-Safe.
> 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.
So? How does that conflict with the compare functions having a
sequential specification? Even if you add certain additional
constraints to executions, at the base you still have a precondition and
a postcondition for the compare function. The
> 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
You mean parallel, I suppose?
> compliant with the standard, at least as long as they do not call the
> compare function concurrently over the same object.
So? Then you effectively guarantee an unordered sequential execution of
the compare functions. Anyway, this discussion belongs into a separate
> >> 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.
Proof, please. That means you either need to list their definitions of
MT-Safe, and show that those don't conflict with each other, or you need
to look at all their implementations, and show that what those guarantee
doesn't conflict with each other. And that still wouldn't tell us what
users think, unless we have precise definitions.
> 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.
I did. See the email I wrote about choices we have to make, for
> 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.
Oh sure you can. For example, just extend and clarify it until it
answers all my questions. For example, if I ask what does "safe" mean,
add a sentence that says what it means; if I ask about program order,
make sure you take it into account in your definition.
> > 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,
So you don't remember the actual definition, just that it seemed clear
to you at that time?
> 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.
And yet there was a bug in the Java memory model, for example, fixed
years later. Trying to infer that a topic is finished by looking at the
when research on it was started doesn't make sense. For example, why
didn't we get memory models for C/C++ earlier?
> > 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?
In what I'm aware of, "thread-safe" is always used as an informal
notion. In the sense of "this is supposed to make sense even if
executed concurrently", and then an actual detailed definition is used
(eg, linearizability, sequential consistency, some sort of
serializability, ...). There are different reasonable criteria, so
"thread-safe" is used as a loose property.
May I ask whether you are familiar with the C11/C++11 model (including
the way the model itself works, and why certain parts are necessary for
the definitions; e.g., look at the formalization by Batty et al.),
perhaps linearizability, and/or the more formal definitions of