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

[Torvald Riegel <triegel at redhat dot com>]

On Mon, 2013-12-02 at 04:21 -0200, Alexandre Oliva wrote:
> 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.

A formal(-ish) way of expression is just a way to clearly define what
one actually means.  It doesn't limit expressiveness in any way.  You
wouldn't say that mathematics aren't sufficient to describe what
computers are supposed to do, would you?

> 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.

What I'm trying to reach is a common denominator.  IOW, we need to
define everything we don't seem to agree on (or define the base of what
we disagree on, so we can actually discuss the possible solutions).
Thus, I am meeting you half-way, in a way.  Given that we also need to
have a definition that is clear for everyone of our users, we need to
define everything that anyone might disagree on, or have a different
initial assumption about.  Thus, a formalish, detailed approach is the
way to solve this.
(BTW, it's not the case that I would have a personal obsession with
formal methods or such; but a formal(-ish) approach is simply a tool you
can't avoid for certain problems.)

> Evidently you're not: I asked
> for *concrete* examples of imprecision, and these choices you point out
> are not concrete at all.

On the model's level, they are.  Because we want to have a
self-contained definition, that matters.  So if a user can be left with
a question like "so, does it mean X or Y" after reading the definition,
we need to clarify this.

> 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).

The modeled object is *not* the POSIX specs.  Instead, the POSIX specs
are trying to define which behavior is allowed under concurrent
execution.  Thus, the POSIX specs should *contain* (or be) a model, but
the model itself would represent the allowed behavior/outcomes of a
certain program.  And the latter is exactly what I was speaking about,
guided by how one reasons about programs.

You could say that the model has to also represent the intent of the
POSIX specs.  But it's not *modeling* the POSIX specs themselves -- that
would be a metamodel.

> 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â

(1) Initially, flockfile(file1) and flockfile(file2) both happened
before the following:

Thread 1:
funlockfile(file1);
r1 = ftrylockfile(file2);

Thread 2:
funlockfile(file2);
r2 = ftrylockfile(file1);

Can both r1 and r2 be nonzero?  If yes/no, how can this be inferred from
the MT-Safe definition?


(2) A coherency example:

Thread1:
setsid();
r = getsid(0);

Thread 2:
setsid();

Can r equal -1?  If not, how does the definition prevent that?  (Note
that saying that this wouldn't be "safe" doesn't cut it, unless there is
actually a definition of safe; neither does "behaves as specified",
because there's no concurrent specification (it can be concurrent with
the other thread's call) of getsid AFAICT.)


(3) Another example:

Thread 1:
setsid();
flockfile(file1);

Thread 2:
if (ftrylockfile(file1) != 0)
  r = getsid(0);

Can r return -1?  If yes/no, how can this be inferred from the MT-Safe
definition?

> 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.

Again, don't try to put it as if I didn't distinguish between both.

> 
> >> > (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.

Can you please rephrase the question so that it makes sense?  Do you
want a specification of a sequential-consistency guarantee for those
functions that doesn't conflict with the current specifications (ie,
don't want a model for the spec but compatible with the spec)?  Modeling
the specification itself is probably not what you want...