* [9fans] interaction of lnfs and autocompletion
@ 2004-11-16 18:55 Skip Tavakkolian
2004-11-16 19:35 ` rog
0 siblings, 1 reply; 6+ messages in thread
From: Skip Tavakkolian @ 2004-11-16 18:55 UTC (permalink / raw)
To: 9fans
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.
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [9fans] interaction of lnfs and autocompletion
2004-11-16 18:55 [9fans] interaction of lnfs and autocompletion Skip Tavakkolian
@ 2004-11-16 19:35 ` rog
2004-11-16 20:04 ` [9fans] spin models rog
0 siblings, 1 reply; 6+ messages in thread
From: rog @ 2004-11-16 19:35 UTC (permalink / raw)
To: 9fans
> 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
^ permalink raw reply [flat|nested] 6+ messages in thread
* [9fans] spin models
2004-11-16 19:35 ` rog
@ 2004-11-16 20:04 ` rog
2004-11-17 0:07 ` Charles Forsyth
0 siblings, 1 reply; 6+ messages in thread
From: rog @ 2004-11-16 20:04 UTC (permalink / raw)
To: 9fans
[-- 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
}
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [9fans] spin models
2004-11-16 20:04 ` [9fans] spin models rog
@ 2004-11-17 0:07 ` Charles Forsyth
2004-12-01 11:02 ` Axel Belinfante
0 siblings, 1 reply; 6+ messages in thread
From: Charles Forsyth @ 2004-11-17 0:07 UTC (permalink / raw)
To: 9fans
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.
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [9fans] spin models
2004-11-17 0:07 ` Charles Forsyth
@ 2004-12-01 11:02 ` Axel Belinfante
2004-12-02 0:31 ` rog
0 siblings, 1 reply; 6+ messages in thread
From: Axel Belinfante @ 2004-12-01 11:02 UTC (permalink / raw)
To: Fans of the OS Plan 9 from Bell Labs
> 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.
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [9fans] spin models
2004-12-01 11:02 ` Axel Belinfante
@ 2004-12-02 0:31 ` rog
0 siblings, 0 replies; 6+ messages in thread
From: rog @ 2004-12-02 0:31 UTC (permalink / raw)
To: 9fans
> 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.
^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2004-12-02 0:31 UTC | newest]
Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2004-11-16 18:55 [9fans] interaction of lnfs and autocompletion Skip Tavakkolian
2004-11-16 19:35 ` rog
2004-11-16 20:04 ` [9fans] spin models rog
2004-11-17 0:07 ` Charles Forsyth
2004-12-01 11:02 ` Axel Belinfante
2004-12-02 0:31 ` rog
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).