Date: Sun, 5 Mar 2000 18:05:13 -0800 From: "David O'Brien" <obrien@FreeBSD.ORG> To: Chuck Robey <chuckr@picnic.mat.net> Cc: "Daniel C. Sobral" <dcs@newsguy.com>, ports@FreeBSD.ORG Subject: Re: Spin Message-ID: <20000305180513.A2531@dragon.nuxi.com> In-Reply-To: <Pine.BSF.4.21.0003051847260.301-100000@picnic.mat.net>; from chuckr@picnic.mat.net on Sun, Mar 05, 2000 at 06:51:31PM -0500 References: <20000305153156.C2252@dragon.nuxi.com> <Pine.BSF.4.21.0003051847260.301-100000@picnic.mat.net>
next in thread | previous in thread | raw e-mail | index | archive | help
On Sun, Mar 05, 2000 at 06:51:31PM -0500, Chuck Robey wrote: > > It certainly isn't CAD -- it isn't used in designing stuff. It is a > > model checker and falls close to the field for Formal Methods and proving > > Does stuff in logic like cad/spice does in electronics. I can't quite parse this. But if you are saying is often used for checking models of circuits like SPICE, then I have to disagree. Here is the description of a couple of the included examples: /* * Models the Pathfinder scheduling algorithm and explains the * cause of the recurring reset problem during the mission on Mars * * there is a high priority process, that consumes * data produced by a low priority process. * data consumption and production happens under * the protection of a mutex lock * the mutex lock conflicts with the scheduling priorities * which can deadlock the system if high() starts up * while low() has the lock set * there are 12 reachable states in the full (non-reduced) * state space -- two of which are deadlock states * partial order reduction cannot be used here because of * the 'provided' clause that models the process priorities */ /* Dolev, Klawe & Rodeh for leader election in unidirectional ring * `An O(n log n) unidirectional distributed algorithm for extrema * finding in a circle,' J. of Algs, Vol 3. (1982), pp. 245-260 */ /* Peterson's solution to the mutual exclusion problem - 1981 */ /* Peterson's algorithm for N processes - see Lynch's book, p. 284 */ /* * PROMELA Validation Model * FLOW CONTROL LAYER VALIDATION [for FTP] */ /* * A program to sort concurrently N "random" numbers * The reduced space and time should be linear in the * number of processes, and can be reduced when the length of * the buffer queues is increased. * In full search it should be exponential. */ To Unsubscribe: send mail to majordomo@FreeBSD.org with "unsubscribe freebsd-ports" in the body of the message
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?20000305180513.A2531>