This is the mail archive of the
`libc-alpha@sourceware.org`
mailing list for the glibc project.

Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|

Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |

Other format: | [Raw text] |

*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

**Follow-Ups**:**Re: Consensus on MT-, AS- and AC-Safety docs.***From:*Torvald Riegel

**References**:**Re: Consensus on MT-, AS- and AC-Safety docs.***From:*Alexandre Oliva

**Re: Consensus on MT-, AS- and AC-Safety docs.***From:*Torvald Riegel

Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|

Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |