pangen5.c

这是一个同样来自贝尔实验室的和UNIX有着渊源的操作系统, 其简洁的设计和实现易于我们学习和理解

/***** spin: pangen5.c *****/

/* Copyright (c) 1999-2003 by Lucent Technologies, Bell Laboratories.     */
/* All Rights Reserved.  This software is for educational purposes only.  */
/* No guarantee whatsoever is expressed or implied by the distribution of */
/* this code.  Permission is given to distribute this code provided that  */
/* this introductory message is not removed and no monies are exchanged.  */
/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
/*             http://spinroot.com/                                       */
/* Send all bug-reports and/or questions to: [e-mail]            */

#include "spin.h"
#ifdef PC
#include "y_tab.h"
#else
#include "y.tab.h"
#endif

typedef struct BuildStack {
	FSM_trans *t;
	struct BuildStack *nxt;
} BuildStack;

extern ProcList	*rdy;
extern int verbose, eventmapnr, claimnr, rvopt, export_ast, u_sync;
extern Element *Al_El;

static FSM_state *fsm_free;
static FSM_trans *trans_free;
static BuildStack *bs, *bf;
static int max_st_id;
static int cur_st_id;
int o_max;
FSM_state *fsm;
FSM_state **fsm_tbl;
FSM_use   *use_free;

static void ana_seq(Sequence *);
static void ana_stmnt(FSM_trans *, Lextok *, int);

extern void AST_slice(void);
extern void AST_store(ProcList *, int);
extern int  has_global(Lextok *);
extern void exit(int);

static void
fsm_table(void)
{	FSM_state *f;
	max_st_id += 2;
	/* fprintf(stderr, "omax %d, max=%d\n", o_max, max_st_id); */
	if (o_max < max_st_id)
	{	o_max = max_st_id;
		fsm_tbl = (FSM_state **) emalloc(max_st_id * sizeof(FSM_state *));
	} else
		memset((char *)fsm_tbl, 0, max_st_id * sizeof(FSM_state *));
	cur_st_id = max_st_id;
	max_st_id = 0;

	for (f = fsm; f; f = f->nxt)
		fsm_tbl[f->from] = f;
}

static int
FSM_DFS(int from, FSM_use *u)
{	FSM_state *f;
	FSM_trans *t;
	FSM_use *v;
	int n;

	if (from == 0)
		return 1;

	f = fsm_tbl[from];

	if (!f)
	{	printf("cannot find state %d\n", from);
		fatal("fsm_dfs: cannot happen\n", (char *) 0);
	}

	if (f->seen)
		return 1;
	f->seen = 1;

	for (t = f->t; t; t = t->nxt)
	{
		for (n = 0; n < 2; n++)
		for (v = t->Val[n]; v; v = v->nxt)
			if (u->var == v->var)
				return n;	/* a read or write */

		if (!FSM_DFS(t->to, u))
			return 0;
	}
	return 1;
}

static void
new_dfs(void)
{	int i;

	for (i = 0; i < cur_st_id; i++)
		if (fsm_tbl[i])
			fsm_tbl[i]->seen = 0;
}

static int
good_dead(Element *e, FSM_use *u)
{
	switch (u->special) {
	case 2:	/* ok if it's a receive */
		if (e->n->ntyp == ASGN
		&&  e->n->rgt->ntyp == CONST
		&&  e->n->rgt->val == 0)
			return 0;
		break;
	case 1:	/* must be able to use oval */
		if (e->n->ntyp != 'c'
		&&  e->n->ntyp != 'r')
			return 0;	/* can't really happen */
		break;
	}
	return 1;
}

#if 0
static int howdeep = 0;
#endif

static int
eligible(FSM_trans *v)
{	Element	*el = ZE;
	Lextok	*lt = ZN;

	if (v) el = v->step;
	if (el) lt = v->step->n;

	if (!lt				/* dead end */
	||  v->nxt			/* has alternatives */
	||  el->esc			/* has an escape */
	||  (el->status&CHECK2)		/* remotely referenced */
	||  lt->ntyp == ATOMIC
	||  lt->ntyp == NON_ATOMIC	/* used for inlines -- should be able to handle this */
	||  lt->ntyp == IF
	||  lt->ntyp == C_CODE
	||  lt->ntyp == C_EXPR
	||  has_lab(el, 0)		/* any label at all */

	||  lt->ntyp == DO
	||  lt->ntyp == UNLESS
	||  lt->ntyp == D_STEP
	||  lt->ntyp == ELSE
	||  lt->ntyp == '@'
	||  lt->ntyp == 'c'
	||  lt->ntyp == 'r'
	||  lt->ntyp == 's')
		return 0;

	if (!(el->status&(2|4)))	/* not atomic */
	{	int unsafe = (el->status&I_GLOB)?1:has_global(el->n);
		if (unsafe)
			return 0;
	}

	return 1;
}

static int
canfill_in(FSM_trans *v)
{	Element	*el = v->step;
	Lextok	*lt = v->step->n;

	if (!lt				/* dead end */
	||  v->nxt			/* has alternatives */
	||  el->esc			/* has an escape */
	||  (el->status&CHECK2))	/* remotely referenced */
		return 0;

	if (!(el->status&(2|4))		/* not atomic */
	&&  ((el->status&I_GLOB)
	||   has_global(el->n)))	/* and not safe */
		return 0;

	return 1;
}

static int
pushbuild(FSM_trans *v)
{	BuildStack *b;

	for (b = bs; b; b = b->nxt)
		if (b->t == v)
			return 0;
	if (bf)
	{	b = bf;
		bf = bf->nxt;
	} else
		b = (BuildStack *) emalloc(sizeof(BuildStack));
	b->t = v;
	b->nxt = bs;
	bs = b;
	return 1;
}

static void
popbuild(void)
{	BuildStack *f;
	if (!bs)
		fatal("cannot happen, popbuild", (char *) 0);
	f = bs;
	bs = bs->nxt;
	f->nxt = bf;
	bf = f;				/* freelist */
}

static int
build_step(FSM_trans *v)
{	FSM_state *f;
	Element	*el = v->step;
#if 0
	Lextok	*lt = ZN;
#endif
	int	st  = v->to;
	int	r;

	if (!el) return -1;

	if (v->step->merge)
		return v->step->merge;	/* already done */

	if (!eligible(v))		/* non-blocking */
		return -1;

	if (!pushbuild(v))		/* cycle detected */
		return -1;		/* break cycle */

	f = fsm_tbl[st];
#if 0
	lt = v->step->n;
	if (verbose&32)
	{	if (++howdeep == 1)
			printf("spin: %s, line %3d, merge:\n",
				lt->fn->name,
				lt->ln);
		printf("\t[%d] <seqno %d>\t", howdeep, el->seqno);
		comment(stdout, lt, 0);
		printf(";\n");
	}
#endif
	r = build_step(f->t);
	v->step->merge = (r == -1) ? st : r;
#if 0
	if (verbose&32)
	{	printf("	merge value: %d (st=%d,r=%d, line %d)\n",
			v->step->merge, st, r, el->n->ln);
		howdeep--;
	}
#endif
	popbuild();

	return v->step->merge;
}

static void
FSM_MERGER(char *pname_unused)	/* find candidates for safely merging steps */
{	FSM_state *f, *g;
	FSM_trans *t;
	Lextok	*lt;

	for (f = fsm; f; f = f->nxt)		/* all states */
	for (t = f->t; t; t = t->nxt)		/* all edges */
	{	if (!t->step) continue;		/* happens with 'unless' */

		t->step->merge_in = f->in;	/* ?? */

		if (t->step->merge)
			continue;
		lt = t->step->n;

		if (lt->ntyp == 'c'
		||  lt->ntyp == 'r'
		||  lt->ntyp == 's')	/* blocking stmnts */
			continue;	/* handled in 2nd scan */

		if (!eligible(t))
			continue;

		g = fsm_tbl[t->to];
		if (!eligible(g->t))
		{
#define SINGLES
#ifdef SINGLES
			t->step->merge_single = t->to;
#if 0
			if ((verbose&32))
			{	printf("spin: %s, line %3d, merge_single:\n\t<seqno %d>\t",
					t->step->n->fn->name,
					t->step->n->ln,
					t->step->seqno);
				comment(stdout, t->step->n, 0);
				printf(";\n");
			}
#endif
#endif
			/* t is an isolated eligible step:
			 *
			 * a merge_start can connect to a proper
			 * merge chain or to a merge_single
			 * a merge chain can be preceded by
			 * a merge_start, but not by a merge_single
			 */

			continue;
		}

		(void) build_step(t);
	}

	/* 2nd scan -- find possible merge_starts */

	for (f = fsm; f; f = f->nxt)		/* all states */
	for (t = f->t; t; t = t->nxt)		/* all edges */
	{	if (!t->step || t->step->merge)
			continue;

		lt = t->step->n;
#if 0
	4.1.3:
	an rv send operation inside an atomic, *loses* atomicity
	when executed
	and should therefore never be merged with a subsequent
	statement within the atomic sequence
	the same is not true for non-rv send operations
#endif

		if (lt->ntyp == 'c'	/* potentially blocking stmnts */
		||  lt->ntyp == 'r'
		||  (lt->ntyp == 's' && u_sync == 0))	/* added !u_sync in 4.1.3 */
		{	if (!canfill_in(t))		/* atomic, non-global, etc. */
				continue;

			g = fsm_tbl[t->to];
			if (!g || !g->t || !g->t->step)
				continue;
			if (g->t->step->merge)
				t->step->merge_start = g->t->step->merge;
#ifdef SINGLES
			else if (g->t->step->merge_single)
				t->step->merge_start = g->t->step->merge_single;
#endif
#if 0
			if ((verbose&32)
			&& t->step->merge_start)
			{	printf("spin: %s, line %3d, merge_START:\n\t<seqno %d>\t",
						lt->fn->name,
						lt->ln,
						t->step->seqno);
				comment(stdout, lt, 0);
				printf(";\n");
			}
#endif
		}
	}
}

static void
FSM_ANA(void)
{	FSM_state *f;
	FSM_trans *t;
	FSM_use *u, *v, *w;
	int n;

	for (f = fsm; f; f = f->nxt)		/* all states */
	for (t = f->t; t; t = t->nxt)		/* all edges */
	for (n = 0; n < 2; n++)			/* reads and writes */
	for (u = t->Val[n]; u; u = u->nxt)
	{	if (!u->var->context	/* global */
		||   u->var->type == CHAN
		||   u->var->type == STRUCT)
			continue;
		new_dfs();
		if (FSM_DFS(t->to, u))	/* cannot hit read before hitting write */
			u->special = n+1;	/* means, reset to 0 after use */
	}

	if (!export_ast)
	for (f = fsm; f; f = f->nxt)
	for (t = f->t; t; t = t->nxt)
	for (n = 0; n < 2; n++)
	for (u = t->Val[n], w = (FSM_use *) 0; u; )
	{	if (u->special)
		{	v = u->nxt;
			if (!w)			/* remove from list */
				t->Val[n] = v;
			else
				w->nxt = v;
#if q
			if (verbose&32)
			{	printf("%s : %3d:  %d -> %d \t",
					t->step->n->fn->name,
					t->step->n->ln,
					f->from,
					t->to);
				comment(stdout, t->step->n, 0);
				printf("\t%c%d: %s\n", n==0?'R':'L',
					u->special, u->var->name);
			}
#endif
			if (good_dead(t->step, u))
			{	u->nxt = t->step->dead;	/* insert into dead */
				t->step->dead = u;
			}
			u = v;
		} else
		{	w = u;
			u = u->nxt;
	}	}
}

void
rel_use(FSM_use *u)
{
	if (!u) return;
	rel_use(u->nxt);
	u->var = (Symbol *) 0;
	u->special = 0;
	u->nxt = use_free;
	use_free = u;
}

static void
rel_trans(FSM_trans *t)