[9fans] spin/trace source for plan9 scheduler

[9fans] spin/trace source for plan9 scheduler

[FODEMESI]

There is a paper called:

Process Sleep and Wakeup on a Shared-memory Multiprocessor
Rob Pike, Dave Presotto, Ken Thompson, and Gerard Holzmann

Is the spin/trace source still available? It would be a great help, I
would need it for a summary on plan9 at the university.

 thank you very much: Gergo

Re: [9fans] spin/trace source for plan9 scheduler

[presotto]

[-- Attachment #1: Type: text/plain, Size: 1345 bytes --]

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.

[-- Attachment #2: Type: message/rfc822, Size: 1524 bytes --]

From: Scott Schwartz <schwartz@bio.cse.psu.edu>
To: 9fans@cse.psu.edu
Subject: Re: [9fans] spin/trace source for plan9 scheduler
Date: Mon, 18 Sep 2000 16:43:43 -0400
Message-ID: <20000918204344.19984.qmail@g.bio.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?

Re: [9fans] spin/trace source for plan9 scheduler

[Scott Schwartz]

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?

re: [9fans] spin/trace source for plan9 scheduler

[Gerard J. Holzmann]

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

----------re:----------------
From: FODEMESI Gergely <fgergo@eik.bme.hu>
To: plan9 mailing list <9fans@cse.psu.edu>
Subject: [9fans] spin/trace source for plan9 scheduler
Sender: 9fans-admin@cse.psu.edu
Errors-To: 9fans-admin@cse.psu.edu
X-BeenThere: 9fans@cse.psu.edu
X-Mailman-Version: 2.0beta4
Reply-To: 9fans@cse.psu.edu
List-Id: Fans of the O/S Plan 9 from Bell Labs <9fans.cse.psu.edu>


There is a paper called:

Process Sleep and Wakeup on a Shared-memory Multiprocessor
Rob Pike, Dave Presotto, Ken Thompson, and Gerard Holzmann

Is the spin/trace source still available? It would be a great help, I
would need it for a summary on plan9 at the university.

 thank you very much: Gergo

Re: [9fans] spin/trace source for plan9 scheduler

[presotto]

[-- Attachment #1: Type: text/plain, Size: 151 bytes --]

Funny you should ask, we're redoing the code and the spin analysis right
now to deal with postnote.  I'll forward you mail to Gerard who's doing it.

[-- Attachment #2: Type: message/rfc822, Size: 3072 bytes --]

From: FODEMESI Gergely <fgergo@eik.bme.hu>
To: plan9 mailing list <9fans@cse.psu.edu>
Subject: [9fans] spin/trace source for plan9 scheduler
Date: Mon, 18 Sep 2000 15:47:44 -0400 (EDT)
Message-ID: <Pine.GSO.4.10.9912131648250.10783-100000@goliat>


There is a paper called:

Process Sleep and Wakeup on a Shared-memory Multiprocessor
Rob Pike, Dave Presotto, Ken Thompson, and Gerard Holzmann 

Is the spin/trace source still available? It would be a great help, I
would need it for a summary on plan9 at the university.

 thank you very much: Gergo

[9fans] spin/trace source for plan9 scheduler

[FODEMESI Gergely]

There is a paper called:

Process Sleep and Wakeup on a Shared-memory Multiprocessor
Rob Pike, Dave Presotto, Ken Thompson, and Gerard Holzmann 

Is the spin/trace source still available? It would be a great help, I
would need it for a summary on plan9 at the university.

 thank you very much: Gergo