[9fans] interaction of lnfs and autocompletion

[9fans] interaction of lnfs and autocompletion

[Skip Tavakkolian]

Interaction of lnfs and Control-F autocompletion is interesting:

cpu% touch a_very_long_file_name_with_an_unusual_extension.rob
cpu% ls -l
--rw-rw-r-- M 10426 fst fst 0 Nov 16 10:44 a_very_long_file_name_with_an_unusual_extension.rob
[no matches in 6ek8trxtbrhgd93fnaj6n2bg9w]
cpu% cat a_ver

BTW, for me the only reason to develop on Plan9 is Glenda.

Re: [9fans] interaction of lnfs and autocompletion

[rog]

> Interaction of lnfs and Control-F autocompletion is interesting:

it's not just lnfs. any local modifications of a window's namespace
will have the same effect.

try:
	bind /usr /tmp
	cd /tmp
	^F

[9fans] spin models

[rog]

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

i've always thought the spin(1) protocol analyser was
a perfect match for the concurrency primitives found in
plan 9 and in Limbo.

i've just had to think again.

these concurrency primitives allow for dynamic creation of processes
and channels.  in particular, a fairly common idiom is (using Limbo
syntax for brevity):

	c := chan of int;
	spawn someproc(c);
	<-c;

where someproc() does something, sends on the channel c,
and continues on its way.

this idiom translates quite naturally into Promela:

	chan c = [0] of {bit};
	run someproc(c);
	c?0

the problem is that promela allows only a static number
of channels, and it doesn't garbage-collect old channels, so
that, for instance, this Promela program:

	active proctype x()
	{
		do
		:: _nr_pr == 1 ->
			run f()
		od
	}
	
	proctype f()
	{
		chan sync = [0] of {bit};
	}

dies very quickly, saying "too many queues".  (the _nr_pr condition is
necessary to prevent exiting processes from building up).

this is a pity, especially given that the spin manual itself suggests
replacing function calls with process invocations - the "factorial"
example given there dies if n > 257.

i imagine there are a few spin users out there.  is there a neat
general solution to this problem (for instance, an automatic
transformation).

or should i just give up on making a spin model of my system?

i've attached a copy of the model.

  cheers,
    rog.

[-- Attachment #2.1: Type: text/plain, Size: 335 bytes --]

from postmaster@ethel:
The following attachment had content that we can't
prove to be harmless.  To avoid possible automatic
execution, we changed the content headers.
The original header was:

	Content-Disposition: attachment; filename=slave2.spin
	Content-Type: text/plain; charset="US-ASCII"
	Content-Transfer-Encoding: 7bit

[-- Attachment #2.2: slave2.spin.suspect --]
[-- Type: application/octet-stream, Size: 1967 bytes --]

#define Nproc 1

chan worktoken = [Nproc] of {bit};
chan newtask = [0] of {bit};
chan tasklock = [1] of {bit};
chan down = [0] of {int};

int nexcl = 0;
int nproc = 0;

#define EXCLUSIVE 2
#define EXISTS 1

active proctype mount()
{
	int t;
	do
	:: down?t ->
		_nr_pr < Nproc*2 + 4 ->
		run processor(t)
	od
}

proctype processor(int t)
{
	chan sync= [0] of {bit};
	chan treply = [0] of {int};
	/*
	 * resubmit old task
	 */
	if
	:: t & EXISTS ->
		if
		:: skip ->
			down!t ->
			goto exit
		:: skip ->
			run taskfinish(sync, t);
			sync?0
		fi
	:: else ->
		skip
	fi;

	do
	:: run runtask(treply) ->
		treply?t;
		if
		:: skip ->
			down!t;
			goto exit
		:: skip ->
			if
			:: t&EXISTS ->
				run taskfinish(sync, t);
				sync?0
			:: else
			fi
		fi
	od;

exit:
	skip
}

proctype runtask(chan treply)
{
	int t, i;
	chan sync = [0] of {bit};
	tasklock!0;
	newtask?0;
	
	if
	:: skip ->
		tasklock?0;
		treply!0;
		goto exit
	:: skip
	fi;

	/*
	 * getworktoken
	 */
	if
	:: skip ->	/* exclusive */
		t = EXCLUSIVE|EXISTS;
		i = 0;
		do
		:: i == Nproc ->
			break
		:: i < Nproc ->
			worktoken?0;
			i = i + 1
		od
	:: skip ->
		t = EXISTS;
		tasklock?0;
		worktoken?0
	fi;

	/*
	 * runtask2
	 */
	if
	:: skip ->		/* submit failed */
		treply!t;
		goto exit
	:: skip
	fi;

	run taskfinish(sync, t);
	sync?0;
	treply!0;
exit:
	skip
}

proctype taskfinish(chan sync; int t)
{
	int i;
	if
	:: t & EXCLUSIVE ->
		i = 0;
		do
		:: i == Nproc ->
			break
		:: i < Nproc ->
			worktoken!0;
			i = i + 1
		od;
		tasklock?0
	:: (t & EXCLUSIVE) == 0 ->
		worktoken!0
	:: else ->
		printf("shouldn't happen (t is %d)\n", t);
	fi;
	sync!0
}

active proctype taskgen()
{
progress: do
	:: newtask!0
	od
}

init
{
	int i;
	i = 0;
	do
	:: i == Nproc ->
		break;
	:: i < Nproc ->
		worktoken!0;
		down!0;
		i = i + 1
	od
}

Re: [9fans] spin models

[Charles Forsyth]

i think a version of spin newer than that in plan 9 (ca. 2000)
supports channel passing and dynamic processes.
a glance at spinroot.com suggests that might be right.

Re: [9fans] spin models

[Axel Belinfante]

> i think a version of spin newer than that in plan 9 (ca. 2000)
> supports channel passing and dynamic processes.
> a glance at spinroot.com suggests that might be right.

not that I'm much of a spin expert (we have one/some here,
don't know if he/they will be available during twente9con), but
running xspin (4.2.0) in simulation and/or verification mode
on slave2.spin brings me further than rog suggested in his mail.

wr.r.t. automatic transformation: (disclaimer as above)
there has been work on extracting promela models from C code,
http://spinroot.com/spin/News/news36.html
so maybe doing something from limbo could be interesting/possible too.

Axel.

Re: [9fans] spin models

[rog]

> not that I'm much of a spin expert (we have one/some here,
> don't know if he/they will be available during twente9con), but
> running xspin (4.2.0) in simulation and/or verification mode
> on slave2.spin brings me further than rog suggested in his mail.

i tried it on what i believe to be to the latest version (4.2.1),
and the main problem (fixed limit on number of channels created)
still seems to be there.

i don't think it was envisaged that channels might be used in this
way.