Re: [Xen-devel] [xen-unstable test] 13461: regressions - FAIL

[Ian Jackson <Ian.Jackson@xxxxxxxxxxxxx>]

Ian Campbell writes ("Re: [Xen-devel] [xen-unstable test] 13461: regressions - 
FAIL"):
> > +    while true; do
> > +        eval "exec $_lockfd>>$lockfile"
> 
> you mean $_lockfile here I think.

Heh.  Yes.

> > +        flock -x $_lockfd
> > +        # We can't just stat /dev/stdin or /proc/self/fd/$_lockfd or
> > +        # use bash's test -ef because those all go through what is
> > +        # actually a synthetic symlink in /proc and we aren't
> > +        # guaranteed that our stat(2) won't lose the race with an
> > +        # rm(1) between reading the synthetic link and traversing the
> > +        # file system to find the inum.  Perl is very fast so use that.
> > +        rightfile=$( perl -e '
> 
> Won't this need to become $(PERL) (or @PERL@ and some seddery at install
> time) for the benefit of BSD?

This is in tools/hotplug/Linux.  AFAICT at least some of the BSDs have
an fstat(1).

> Does stating $_lockfile before and after the flock, in addition to
> comparing both with $_lockfd, close the race you are worried about?

The correct answer to this question is to present a proof that what
I'm doing is correct.  So:

  * The lock is owned not by a process but by an open-file (informally
    an fd).  Any process with an fd onto this open-file is a
    lockholder and may perform the various operations; such a process
    should only do so when its co-lockholder processes expect.  Ie, we
    will treat all processes holding fds onto the open-file as acting
    in concert and not distinguish between them.

  * You are a lockholder if
      - You have an fd onto an open-file which
      - currently holds an exclusive flock lock on its inum
      - and that inum is currently linked at the lockfile path

  * The rules are:
      - No-one but a lockholder may unlink the lockfile path
        (or otherwise cause it to stop referring to a file it
        refers to).
      - Anyone may open the lockfile with O_CREAT

  * The protocol for locking is:
      - Open the file (O_CREAT)
      - flock it
      - fstat the fd you got
      - stat the lockfile
      - if both are equal you have the lock, otherwise try again.

  * Informal proof of exclusivity:
      - No two open-files can hold an fcntl lock onto the same file
        at the same time
      - No two files can have the same name at the same time

  * Informal proof of correctness of locking protocol:
      - After you call flock successfully no-one other than you
        (someone with the same open-file) can stop you having
        that flock lock.
      - Obviously the inum you get from the fstat is fixed
      - At the point where you call stat there are two
        possibilities:
          (i) the lockfile path referred to some other inum
              in which case you have failed
          (ii) the lockfile path referred to the same file
              in which case you had (by definition) at that
              point the file locked.

  * Informal proof that no-one else can steal the lock:
      - After you call flock successfully no-one other than you
        can stop you having that flock lock
      - No-one other than the lockholder is permitted to stop
        the path referring to a particular inum.  So if you
        hold the lock then only you are allowed to stop the
        path referring to the file whose flock you hold
    Thus once you hold the lock at any instant, you will
    continue to do so until you voluntarily stop doing so
    (eg by unlinking the lockfile or closing the fd).

This demonstrates, I think, that the design is correct.  I will do
some testing on the implementation to try to check that it implements
the design.

> I suppose there is no point in unlocking too?

See my reply to Daniel.

Ian.

_______________________________________________
Xen-devel mailing list
Xen-devel@xxxxxxxxxxxxx
http://lists.xen.org/xen-devel