From mboxrd@z Thu Jan  1 00:00:00 1970
Message-ID: <f76b49d1af064e30d5d7138d78191b32@vitanuova.com>
To: 9fans@cse.psu.edu
Date: Tue, 16 Nov 2004 20:04:17 +0000
From: rog@vitanuova.com
In-Reply-To: <2bb671db109de535914062d5cec26e36@vitanuova.com>
MIME-Version: 1.0
Content-Type: multipart/mixed;
	boundary="upas-xqwmhzdgayiclcrhkochywmpfb"
Subject: [9fans] spin models
Topicbox-Message-UUID: 03772f98-eace-11e9-9e20-41e7f4b1d025

This is a multi-part message in MIME format.
--upas-xqwmhzdgayiclcrhkochywmpfb
Content-Disposition: inline
Content-Type: text/plain; charset="US-ASCII"
Content-Transfer-Encoding: 7bit

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.

--upas-xqwmhzdgayiclcrhkochywmpfb
Content-Type: multipart/mixed;
	boundary="upas-jxfurlwnehaijnxhitpjrgoxox"
Content-Disposition: inline

This is a multi-part message in MIME format.
--upas-jxfurlwnehaijnxhitpjrgoxox
Content-Disposition: inline
Content-Type: text/plain; charset="US-ASCII"
Content-Transfer-Encoding: 7bit

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
--upas-jxfurlwnehaijnxhitpjrgoxox
Content-Type: application/octet-stream
Content-Disposition: attachment; filename="slave2.spin.suspect"

#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
}
--upas-jxfurlwnehaijnxhitpjrgoxox--
--upas-xqwmhzdgayiclcrhkochywmpfb--