From owner-freebsd-hackers@FreeBSD.ORG  Wed Aug  6 16:22:32 2003
Return-Path: <owner-freebsd-hackers@FreeBSD.ORG>
Delivered-To: freebsd-hackers@freebsd.org
Received: from mx1.FreeBSD.org (mx1.freebsd.org [216.136.204.125])
	by hub.freebsd.org (Postfix) with ESMTP id E680D37B401
	for <freebsd-hackers@freebsd.org>;
	Wed,  6 Aug 2003 16:22:32 -0700 (PDT)
Received: from ebb.errno.com (ebb.errno.com [66.127.85.87])
	by mx1.FreeBSD.org (Postfix) with ESMTP id 3FD7C43F75
	for <freebsd-hackers@freebsd.org>;
	Wed,  6 Aug 2003 16:22:32 -0700 (PDT)	(envelope-from sam@errno.com)
Received: from melange.errno.com (melange.errno.com [66.127.85.82])
	(authenticated bits=0)
	by ebb.errno.com (8.12.9/8.12.9) with ESMTP id h76NMU7N034286
	(version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=NO);
	Wed, 6 Aug 2003 16:22:31 -0700 (PDT)
	(envelope-from sam@errno.com)
Date: Wed, 06 Aug 2003 16:22:30 -0700
From: Sam Leffler <sam@errno.com>
To: Ted Unangst <tedu@stanford.edu>, freebsd-hackers@freebsd.org
Message-ID: <1650093869.1060186950@melange.errno.com>
In-Reply-To: <Pine.GSO.4.44.0308061506120.29218-100000@saga0.Stanford.EDU>
References: <Pine.GSO.4.44.0308061506120.29218-100000@saga0.Stanford.EDU>
X-Mailer: Mulberry/3.0.3 (Win32)
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
Subject: Re: possible deadlocks?
X-BeenThere: freebsd-hackers@freebsd.org
X-Mailman-Version: 2.1.1
Precedence: list
List-Id: Technical Discussions relating to FreeBSD
	<freebsd-hackers.freebsd.org>
List-Unsubscribe: <http://lists.freebsd.org/mailman/listinfo/freebsd-hackers>,
	<mailto:freebsd-hackers-request@freebsd.org?subject=unsubscribe>
List-Archive: <http://lists.freebsd.org/pipermail/freebsd-hackers>
List-Post: <mailto:freebsd-hackers@freebsd.org>
List-Help: <mailto:freebsd-hackers-request@freebsd.org?subject=help>
List-Subscribe: <http://lists.freebsd.org/mailman/listinfo/freebsd-hackers>,
	<mailto:freebsd-hackers-request@freebsd.org?subject=subscribe>
X-List-Received-Date: Wed, 06 Aug 2003 23:22:33 -0000

> My advisor Dawson Engler has written a deadlock detector, and we'd like
> some verification. They look like bugs, unless there is some other reason
> why two call chains cannot happen at the same time.
>

Dawson?  Hey Dawson!

> second one in bpf, between bpfif_lock and bpfd_lock.
>
> thread 1:
> bpf_tap() /* or bpf_mtap */
>   BPFIF_LOCK(bp); /* gets this lock */
>   for (d = bp->bif_dlist; d != 0; d = d->bd_next) {
> 	BPFD_LOCK(d); /* waits for thread 2 */
>
> thread 2:
> bpf_setdlt()
>   BPFD_LOCK(d); /* gets lock */
>   bpf_detachd(d); /* or bpf_attachd */
>     BPFIF_LOCK(bp); /* waits for thread 1 */

Yeah, this is my bad.  Will have to look if it's possible.

Does this mean you're going to prove -current is "lockably corrrect"? :)

	Sam