From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Mon, 18 Sep 2000 17:07:43 -0400
From: presotto@plan9.bell-labs.com
To: 9fans@cse.psu.edu
Subject: Re: [9fans] spin/trace source for plan9 scheduler
MIME-Version: 1.0
Content-Type: multipart/mixed;
	boundary="upas-mxcqphquupydhfqxpvcqlxrrqz"
Message-Id: <20000918210744.EAFD119A09@mail>
Topicbox-Message-UUID: 092488e6-eac9-11e9-9e20-41e7f4b1d025

This is a multi-part message in MIME format.
--upas-mxcqphquupydhfqxpvcqlxrrqz
Content-Disposition: inline
Content-Type: text/plain; charset="US-ASCII"
Content-Transfer-Encoding: 7bit

No, we're doing that now.  Gerard is currently analysing sleep/wakeup/postnote
using the actual code.  I've taken Richard Miller's solution to sleep/wakeup
to heart and then changed it to make the explanation easier.  His solution is
probably better but I changed it to lock both the rendezvous and process
lock simultaneously in sleep, wakeup, and postnote.  It means that I have to
break the possible lock ordering deadlock in postnote (which I do by releasing
and reacquiring) but it makes explaining that p->r and r->p are consistent a
lot easier, i.e., they're both always changed under both locks.

Of course Gerard found another possible hole that we're going to define
away as not a hole.  To wit:


	p1			p2
	make cond=true
	call wakeup
	.			call sleep
	.			cond == true ?y
	.			cond = false // never mind the sleep
	.			.
	.			.
	.			call sleep
	.			cond == true ?n
	.			goto sleep
	check sleepers
	find p2
	wake him up
				wakes up
				condition == false!

The idea here is that sleep gets called twice before wakeup gets going.
The problem is that p2 is awakened when it shouldn't be.  We define it
away by saying that you aren't guaranteed after the sleep that the
condition is set, you need to check.

When gerard has finished, I'll post the current version of proc.c
and gerard's conclusions.

--upas-mxcqphquupydhfqxpvcqlxrrqz
Content-Type: message/rfc822
Content-Disposition: inline

Received: from plan9.cs.bell-labs.com ([135.104.9.2]) by plan9; Mon Sep 18 16:44:18 EDT 2000
Received: from mail ([130.203.4.6]) by plan9; Mon Sep 18 16:44:18 EDT 2000
Received: from psuvax1.cse.psu.edu (unknown [130.203.30.6])
	by mail (CSE Mail Server) with ESMTP
	id 62E3D19A11; Mon, 18 Sep 2000 16:44:07 -0400 (EDT)
Received: from bio.cse.psu.edu (galapagos.cse.psu.edu [130.203.12.17])
	by mail (CSE Mail Server) with SMTP id 4B3A5199D4
	for <9fans@cse.psu.edu>; Mon, 18 Sep 2000 16:43:44 -0400 (EDT)
Received: (qmail 19986 invoked by uid 991); 18 Sep 2000 20:43:44 -0000
Message-ID: <20000918204344.19984.qmail@g.bio.cse.psu.edu>
To: 9fans@cse.psu.edu
Subject: Re: [9fans] spin/trace source for plan9 scheduler 
In-Reply-To: Message from "Gerard J. Holzmann" <gerard@research.bell-labs.com> 
   of "Mon, 18 Sep 2000 16:16:35 EDT." <200009182018.QAA65558638@nslocum.cs.bell-labs.com> 
Date: Mon, 18 Sep 2000 16:43:43 -0400
From: Scott Schwartz <schwartz@bio.cse.psu.edu>
Sender: 9fans-admin@cse.psu.edu
Errors-To: 9fans-admin@cse.psu.edu
X-BeenThere: 9fans@cse.psu.edu
X-Mailman-Version: 2.0beta4
Precedence: bulk
Reply-To: 9fans@cse.psu.edu
List-Id: Fans of the O/S Plan 9 from Bell Labs <9fans.cse.psu.edu>

Gerard:
| the final spin model mentioned in the paper (with
| the correction for the flaws discussed then) can be
| retrieved from:
| 	ftp://cm.bell-labs.com/cm/cs/who/gerard/sleep_wakeup

Does that include a discussion of the fixes that were required
for the third edition?


--upas-mxcqphquupydhfqxpvcqlxrrqz--