* [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).