This is the mail archive of the
libc-alpha@sourceware.org
mailing list for the glibc project.
Re: Consensus on MT-, AS- and AC-Safety docs.
- From: Alexandre Oliva <aoliva at redhat dot com>
- To: Torvald Riegel <triegel at redhat dot com>
- Cc: "Joseph S. Myers" <joseph at codesourcery dot com>, "Carlos O'Donell" <carlos at redhat dot com>, GNU C Library <libc-alpha at sourceware dot org>, Rich Felker <dalias at aerifal dot cx>
- Date: Mon, 02 Dec 2013 04:21:57 -0200
- Subject: Re: Consensus on MT-, AS- and AC-Safety docs.
- Authentication-results: sourceware.org; auth=none
- References: <528A7C8F dot 8060805 at redhat dot com> <Pine dot LNX dot 4 dot 64 dot 1311182312130 dot 8831 at digraph dot polyomino dot org dot uk> <orob5fv8nl dot fsf at livre dot home> <Pine dot LNX dot 4 dot 64 dot 1311201555320 dot 28804 at digraph dot polyomino dot org dot uk> <orli0itbm5 dot fsf at livre dot home> <Pine dot LNX dot 4 dot 64 dot 1311211322040 dot 14539 at digraph dot polyomino dot org dot uk> <or4n75t4b7 dot fsf at livre dot home> <Pine dot LNX dot 4 dot 64 dot 1311221324200 dot 5029 at digraph dot polyomino dot org dot uk> <orob5csdvx dot fsf at livre dot home> <Pine dot LNX dot 4 dot 64 dot 1311221535560 dot 8443 at digraph dot polyomino dot org dot uk> <or61rjs2li dot fsf at livre dot home> <orhab3qktz dot fsf at livre dot home> <Pine dot LNX dot 4 dot 64 dot 1311251755140 dot 12149 at digraph dot polyomino dot org dot uk> <orpppop975 dot fsf at livre dot home> <1385414332 dot 3152 dot 3643 dot camel at triegel dot csb> <orhaayoqk8 dot fsf at livre dot home> <1385549084 dot 3152 dot 5896 dot camel at triegel dot csb> <ork3ftmvkj dot fsf at livre dot home> <1385657312 dot 3152 dot 9107 dot camel at triegel dot csb> <or8uw5jmh0 dot fsf at livre dot home> <1385921652 dot 3152 dot 11550 dot camel at triegel dot csb>
On Dec 1, 2013, Torvald Riegel <triegel@redhat.com> wrote:
> In another email, I mentioned a couple of choices that a definition of
> MT-Safe will have to make.
To be blunt, I can't see that your choice of formal-ish modeling
language is sufficiently expressive to capture the kind of abstract
specifications present in POSIX, so I didn't put any time into trying to
translate my internal conceptual framework into what you proposed, or
those choices to my conceptual framework.
Given infinite time, I guess I could try to figure out the way you
reason about and formalize this stuff, but that wouldn't be fair if
you're not willing to meet me half-way. Evidently you're not: I asked
for *concrete* examples of imprecision, and these choices you point out
are not concrete at all. They are problems you perceive in this
meta-model you came up with, that AFAICT can't even represent the whole
of what you're trying to model. Given that, I'm not even convinced the
choices/problems you see aren't artifacts of your model rather than of
the modeled object (namely the POSIX specs).
So, let's try again:
>> I think I have a precise definition. Can you back up your claim by
>> giving a concrete situation in which you believe the definition fails
>> to capture some notion of safety?
Note the âconcreteâ. What I'm looking for is something like âone thread
calls this function specified as MT-Safe while another thread calls this
other function also specified as MT-Safe, but I can't tell what the
expectations are WRT their behavior: it could be X, Y, or Z, and it
ought to be specifiedâ or âI don't see how they could both be MT-Safe,
because X and Y makes that impossibleâ. That would be constructive
proof, rather than hand-wavy assertion, of an insufficiently-precise
definition. âIt's not sequentially consistent, but I expect it to beâ
may very well be a fact or two, but it's no proof of imprecision, it's
just indication of an expectation mismatch.
>> > (2) I believe that something similar to sequential consistency is
>> > easier for our users (and we would follow the choice made by C11 and
>> > C++11).
>> POSIX already specifies interfaces that explicitly permit interleaving
>> of executions, so this boat has already sailed.
> That doesn't conflict with sequential consistency, BTW. You can break
> up a function into several parts, for example, yet those can still be
> sequentially consistent.
I'll believe it when you show me a sequentally-consistent model for the
POSIX abstract specifications (as opposed to for specific
POSIX-compliant implementations) of qsort and bsearch.
--
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