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

[Alexandre Oliva]

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