# HG changeset patch
# User Ian Jackson <Ian.Jackson@eu.citrix.com>
# Date 1341488425 -3600
# Node ID 497e2fe4945594cd2846f0302bef5e5dafa1c2c6
# Parent  ad08cd8e7097ec6da6526cf8ac26f0fa72cd1e01
hotplug/Linux: do not leak lockfiles

25590:bb250383a4f5 introduced a new locking scheme.  Unfortunately it
leaves behind files in /var/run/xen-hotplug.  These are spotted as
regressions by the autotester.

Fix this.  This involves changing the locking protocol to allow
lockfiles to be deleted (as removing lockfiles is unsafe with a naive
flock-based algorithm).

Signed-off-by: Ian Jackson <ian.jackson@eu.citrix.com>
Committed-by: Ian Jackson <ian.jackson@eu.citrix.com>

diff -r ad08cd8e7097 -r 497e2fe49455 tools/hotplug/Linux/locking.sh
--- a/tools/hotplug/Linux/locking.sh	Thu Jul 05 11:00:28 2012 +0100
+++ b/tools/hotplug/Linux/locking.sh	Thu Jul 05 12:40:25 2012 +0100
@@ -30,6 +30,7 @@ LOCK_BASEDIR=/var/run/xen-hotplug
     done
     _lockdict[$i]="$1"
     let _lockfd=200+i
+    _lockfile="$LOCK_BASEDIR/$1"
 }
 
 
@@ -37,13 +38,92 @@ claim_lock()
 {
     mkdir -p "$LOCK_BASEDIR"
     _setlockfd $1
-    eval "exec $_lockfd>>$LOCK_BASEDIR/$1"
-    flock -x $_lockfd
+    # The locking strategy is identical to that from with-lock-ex(1)
+    # from chiark-utils, except using flock.  It has the benefit of
+    # it being possible to safely remove the lockfile when done.
+    # See below for a correctness proof.
+    local rightfile
+    while true; do
+        eval "exec $_lockfd>>$_lockfile"
+        flock -x $_lockfd || return $?
+        # 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 '
+            open STDIN, "<&'$_lockfd'" or die $!;
+            my $fd_inum = (stat STDIN)[1]; die $! unless defined $fd_inum;
+            my $file_inum = (stat $ARGV[0])[1];
+            print "y\n" if $fd_inum eq $file_inum;
+                             ' "$_lockfile" )
+        if [ x$rightfile = xy ]; then break; fi
+    done
 }
 
 
 release_lock()
 {
     _setlockfd $1
-    flock -u $_lockfd
+    rm "$_lockfile"
 }
+
+# Protocol and correctness proof:
+#
+# * 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 have open
+#     - stat the lockfile path
+#     - 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 at that point you were the
+#             lockholder (by definition).
+#
+# * 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; so
+#       it will continue to refer to that file.
+#   That's both the conditions for being the lockholder.
+#
+#   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).
