tech-kern archive

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]

Re: ARC model specified in spinroot/promela



>>>>> Mathew, Cherry G * <c%bow.st@localhost> writes:

>>>>> Mathew, Cherry G * <c%bow.st@localhost> writes:
    > [...]


    >> The next step is to write the equivalent C code, compile it with
    >> a simple test "driver" (ideally ATF, but since this is standalone
    >> for the moment, I'll use something simpler, just to illustrate
    >> the concept), and then hook it into spin's "modex" tool, to
    >> extract the implicit model. Once this is done, we'll have a full
    >> cycle of
    design-> implement->verify and this will demonstrate the DDD (Design
    >> Driven Development) methodology I'd love to hear your thoughts
    >> about.

    > I'm attaching below patch (with the usual instructions) to give a
    > sense of direction. At this point, the C code is purely manually
    > crafted. The next step (modex extraction) ties the original model
    > (arc.pml and friends) to the extracted code (arc.c and friends). I
    > am working on that next, and will post later in the week when
    > that's done.

Follow up as promised. Please see below patch with the usual
instructions. There's a slight complication though, in that the modex
tool isn't packaged for most OSs. It's fairly straightforward to compile
it on a posix-y build environment though.  You can grab the sources
here:
https://github.com/nimble-code/Modex

I think at this stage a few comments on the model extraction are
important: 

1) The usual pattern for spin modex is to convert the source code into C
code "snippets" that sit within the extracted promela source. What then
happens is that, subsets of the code's data state space are exported to
the model, which can then be subject to the usual LTL invariance checks.

I've taken a different approach here - slightly abusing the extractor
framework, I have basically "converted" the C source code back as close
to the original model as possible.

In order to see this in action, do the following:

$ make clean modex-gen
$ cp spinmodel.pml /tmp/spinmodel-modex.pml
$ make clean spin-gen
$ diff -u spinmodel /tmp/spinmodel-modex.pml

When you make the comparison, you will see that the extraction attempts
a source model level retrieval. I ran this by the author of spin
(Dr. Gerard Holzmann) and he said the approach looked interesting. The
problem is that the "harness language" used to drive the extraction is
very brittle and has terrible syntax IMHO (whoever thought up <TAB> as
token separator ?!!!). See arc.prx for this in action.

The advantage of this approach is that you can virtually assume that if
the model passes verification, then any logical bugs lie elsewhere.

Interestingly, I now have a good challenge, as the queue.h manipulation
I have done via arc.h does crash (at delLRU() ). So this will be a good
test of my theory. At the very least, the model extraction process is a
far more rigourous process of code review - where questions about logic
can be asked formally via the LTL constraints.

2) The modex data object export support is terrible - it only supports
basic data types, and the source parser is unable to automatically
export expressions. As you probably noticed in the arc.prx file, I've
kludged around this by doing effectively a sed s// over all expressions
in the source code. This shortcoming can be addressed by improving the
modex parser code. I have applied for a research grant in this regard,
and if it comes through, then I am committed to fixing it (in
consultation with the primary author, of course).

3) The gap between extracted code, and the "glue" that allows it to be
driven both as a final compiled program, and as a module under test can
be addressed by setting up infrastructure that I'm calling "Equivalence
Verification/Testing". For eg: the semantics of readLRU()/delLRU() are
implemented using spin "channel"s in the model, and a simple queue(3)
mechanism in the C implementation. Equivalence will guarantee that they
implement the intended semantics accurately.

I believe that the *BSD OSs have a firm USP, if we can implement modular
verification as part of the CI infrastructure - having a mirror
"Equivalence" infrastructure will make this process much easier for new
modules, as well as ingesting existing ones.

With that thought, I take leave for the weekend, and hope to put my
money where my mouth is, by debugging the current C implementation using
ideas described above.

$ make prog
$ ./arc

should give you a crash dump for gdb, which, I'm getting a SEG fault at
delLRU() well into the caching input trace (T1 has 59 out of 64 entries
filled!)

Finally, if you know anyone contracting or hiring software Engineers or
Leads, where an intersect between concurret programming and modelling is
interesting, please signpost me (offlist of course).

Have a great weekend!

-- 
~cherry

diff -urN arc.null/arc.c arc/arc.c
--- arc.null/arc.c	1970-01-01 00:00:00.000000000 +0000
+++ arc/arc.c	2023-09-07 07:56:40.245824950 +0000
@@ -0,0 +1,174 @@
+/* C Implementation of the Adaptive Replacement Cache algorithm. Written by cherry */
+
+/*
+ * We implement the following algorithm from page 10, Figure 4.
+ * https://www.usenix.org/legacy/events/fast03/tech/full_papers/megiddo/megiddo.pdf
+ *
+ *
+ *  ARC(c)
+ *  
+ *  INPUT: The request stream x1,x2,....,xt,....
+ *  INITIALIZATION: Set p = 0 and set the LRU lists T1, B1, T2, and B2 to empty.
+ *  
+ *  For every t>=1 and any xt, one and only one of the following four cases must occur.
+ *  Case I: xt is in T1 or T2. A cache hit has occurred in ARC(c) and DBL(2c).
+ *       Move xt to MRU position in T2.
+ *  
+ *  Case II: xt is in B1. A cache miss (resp. hit) has occurred in ARC(c) (resp. DBL(2c)).
+ *       	 ADAPTATION: Update p = min { p + d1,c }
+ *  	 	     where d1 = { 1 if |B1| >= |B2|, |B2|/|B1| otherwise
+ *  
+ *       REPLACE(xt, p). Move xt from B1 to the MRU position in T2 (also fetch xt to the cache).
+ *  
+ *  Case III: xt is in B2. A cache miss (resp. hit) has occurred in ARC(c) (resp. DBL(2c)).
+ *       	 ADAPTATION: Update p = max { p - d2,0 }
+ *  	 	     where d2 = { 1 if |B2| >= |B1|, |B1|/|B2| otherwise
+ *  
+ *       REPLACE(xt, p). Move xt from B2 to the MRU position in T2 (also fetch xt to the cache).
+ *       
+ *  Case IV: xt is not in T1 U B1 U T2 U B2. A cache miss has occurred in ARC(c) and DBL(2c).
+ *       Case A: L1 = T1 U B1 has exactly c pages.
+ *       	  If (|T1| < c)
+ *  	     	     	Delete LRU page in B1. REPLACE(xt,p).
+ *  	  	  else
+ *			Here B1 is empty. Delete LRU page in T1 (also remove it from the cache).
+ *  	  	  endif
+ *       Case B: L1 = T1 U B1 has less than c pages.
+ *       	  If (|T1| + |T2| + |B1| + |B2| >= c)
+ *  	             Delete LRU page in B2, if (|T1| + |T2| + |B1| + |B2| = 2c).
+ *  		     REPLACE(xt, p).
+ *  	  	  endif
+ *  
+ *       Finally, fetch xt to the cache and move it to MRU position in T1.
+ *  
+ *  Subroutine REPLACE(xt,p)
+ *       If ( (|T1| is not empty) and ((|T1| exceeds the target p) or (xt is in B2 and |T1| = p)) )
+ *       	  Delete the LRU page in T1 (also remove it from the cache), and move it to MRU position in B1.
+ *       else
+ *		  Delete the LRU page in T2 (also remove it from the cache), and move it to MRU position in B2.
+ *       endif
+ */
+ 
+#include "arc.h"
+
+static void arc_list_init(struct arc_list *_arc_list)
+{
+	TAILQ_INIT(&_arc_list->qhead);
+	_arc_list->qcount = 0;
+	
+	int i;
+	for(i = 0; i < ARCLEN; i++) {
+		init_arc_item(&_arc_list->item_list[i], IID_INVAL, false);
+	};
+}
+
+int p, d1, d2;
+struct arc_list _B1, *B1 = &_B1, _B2, *B2 = &_B2, _T1, *T1 = &_T1, _T2, *T2 = &_T2;
+
+void arc_init(void)
+{
+	p = d1 = d2 = 0;
+
+	arc_list_init(B1);
+	arc_list_init(B2);
+	arc_list_init(T1);
+	arc_list_init(T2);
+}
+
+struct arc_item _LRUitem, *LRUitem = &_LRUitem;
+
+static void
+REPLACE(struct arc_item *x_t, int p)
+{
+
+
+	init_arc_item(LRUitem, IID_INVAL, false);
+
+	if ((lengthof(T1) != 0) &&
+	    ((lengthof(T1) >  p) ||
+	     (memberof(B2, x_t) && (lengthof(T1) == p)))) {
+		/* XXX: d_step { ? */
+		readLRU(T1, LRUitem);
+		delLRU(T1);
+		cacheremove(LRUitem);
+		addMRU(B1, LRUitem);
+	} else {
+		readLRU(T2, LRUitem);
+		delLRU(T2);
+		cacheremove(LRUitem);
+		addMRU(B2, LRUitem);
+	}
+}
+
+void
+ARC(struct arc_item *x_t)
+{
+	if (memberof(T1, x_t)) { /* Case I */
+		delitem(T1, x_t);
+		addMRU(T2, x_t);
+	}
+
+	if (memberof(T2, x_t)) { /* Case I */
+		delitem(T2, x_t);
+		addMRU(T2, x_t);
+	}
+
+	if (memberof(B1, x_t)) { /* Case II */
+		d1 = ((lengthof(B1) >= lengthof(B2)) ? 1 : (lengthof(B2)/lengthof(B1)));
+		p = min((p + d1), C);
+
+		REPLACE(x_t, p);
+
+		delitem(B1, x_t);
+		addMRU(T2, x_t);
+		cachefetch(x_t);
+	}
+
+	if (memberof(B2, x_t)) { /* Case III */
+		d2 = ((lengthof(B2) >= lengthof(B1)) ? 1 : (lengthof(B1)/lengthof(B2)));
+		p = max((p - d2), 0);
+
+		REPLACE(x_t, p);
+
+		delitem(B2, x_t);
+		addMRU(T2, x_t);
+		cachefetch(x_t);
+	}
+
+	if (!(memberof(T1, x_t) ||
+	      memberof(B1, x_t) ||
+	      memberof(T2, x_t) ||
+	      memberof(B2, x_t))) { /* Case IV */
+
+		if ((lengthof(T1) + lengthof(B1)) == C) { /* Case A */
+			if (lengthof(T1) < C) {
+				delLRU(B1);
+				REPLACE(x_t, p);
+			} else {
+				assert(lengthof(B1) == 0);
+				readLRU(T1, LRUitem);
+				delLRU(T1);
+				cacheremove(LRUitem);
+			}
+		}
+
+		if ((lengthof(T1) + lengthof(B1)) < C) {
+			if ((lengthof(T1) +
+			     lengthof(T2) +
+			     lengthof(B1) +
+			     lengthof(B2)) >= C) {
+				if ((lengthof(T1) +
+				     lengthof(T2) +
+				     lengthof(B1) +
+				     lengthof(B2)) == (2 * C)) {
+
+					delLRU(B2);
+				}
+				
+				REPLACE(x_t, p);
+			}
+		}
+		cachefetch(x_t);
+		addMRU(T1, x_t);
+	}
+}
diff -urN arc.null/arc.drv arc/arc.drv
--- arc.null/arc.drv	1970-01-01 00:00:00.000000000 +0000
+++ arc/arc.drv	2023-09-07 16:43:18.906339006 +0000
@@ -0,0 +1,52 @@
+/* Spin process model for Adaptive Replacement Cache algorithm. Written by cherry */
+
+/* Note: What we're attempting in this driver file, is to generate an
+ * input trace that would exercise all code-paths of the model specified
+ * in arc.pml
+ *
+ * Feeding a static trace to the algorithm in array _x[N_ITEMS] is a
+ * acceptable alternative.
+ */
+/* #include "arc.pmh" See Makefile , spinmodel.pml */
+
+#define N_ITEMS (2 * C) /* Number of distinct cache items to test with */
+#define ITEM_REPS (C / 4) /* Max repeat item requests */
+#define N_ITERATIONS 3
+
+hidden arc_item _x[N_ITEMS]; /* Input state is irrelevant from a verification PoV */
+hidden int _x_iid = 0;
+hidden int _item_rep = 0;
+hidden int _iterations = 0;
+
+/* Drive the procs */
+init {
+
+	atomic {
+	       do
+	       ::
+	       _iterations < N_ITERATIONS ->
+	       
+			_x_iid = 0;
+			do
+			:: _x_iid < N_ITEMS ->
+			   	   init_arc_item(_x[_x_iid], _x_iid, false);
+				   _item_rep = 0;
+				   do
+				   :: _item_rep < (_x_iid % ITEM_REPS) ->
+				      		ARC(_x[_x_iid]);
+						_item_rep++;
+				   :: _item_rep >= (_x_iid % ITEM_REPS) ->
+				      		break;
+				   od
+				   _x_iid++;
+			:: _x_iid >= N_ITEMS ->
+				break;
+			od
+			_iterations++;
+		::
+		_iterations >= N_ITERATIONS ->
+			    break;
+		od
+	}
+
+}
diff -urN arc.null/arc_drv.c arc/arc_drv.c
--- arc.null/arc_drv.c	1970-01-01 00:00:00.000000000 +0000
+++ arc/arc_drv.c	2023-09-06 14:25:07.045001611 +0000
@@ -0,0 +1,33 @@
+#include "arc.h"
+
+#define N_ITEMS (2 * C) /* Number of distinct cache items to test with */
+#define ITEM_REPS (C / 4) /* Max repeat item requests */
+#define N_ITERATIONS 3
+
+static struct arc_item _x[N_ITEMS]; /* Input state is irrelevant from a verification PoV */
+static int _x_iid = 0;
+static int _item_rep = 0;
+static int _iterations = 0;
+
+/* Drive ARC() with a preset input trace */
+
+void
+main(void)
+{
+	arc_init(); /* Init module state */
+
+	while (_iterations < N_ITERATIONS) {
+		_x_iid = 0;
+		while (_x_iid < N_ITEMS) {
+			init_arc_item(&_x[_x_iid], _x_iid, false);
+			_item_rep = 0;
+			while(_item_rep < (_x_iid % ITEM_REPS) ) {
+				ARC(&_x[_x_iid]);
+				_item_rep++;
+			} 
+			_x_iid++;
+		}
+		_iterations++;
+	}
+}
+
diff -urN arc.null/arc.h arc/arc.h
--- arc.null/arc.h	1970-01-01 00:00:00.000000000 +0000
+++ arc/arc.h	2023-09-08 10:09:17.217694851 +0000
@@ -0,0 +1,169 @@
+/*
+ * The objective of the header here is to provide a set of macros that
+ * reflect the interfaces designed in arc.pmh
+ */
+
+#ifndef _ARC_H_
+#define _ARC_H_
+
+#ifdef __NetBSD__
+/* TODO: */
+#else
+/* Defaults to POSIX */
+#include <assert.h>
+#include <stddef.h>
+#include <stdbool.h>
+#endif
+
+#include "queue.h" /* We use the NetBSD version as it has no
+		    * dependencies (except for -DNULL) . */
+
+#define C 64
+
+#define ARCLEN (2 * C) /* c.f ghost cache directory length constraints in arc.inv */
+
+#define IID_INVAL -1
+
+struct arc_item {
+	TAILQ_ENTRY(arc_item) qlink;	
+	int iid;	/* Unique identifier for item */
+	bool cached;
+};
+
+struct arc_list {
+	TAILQ_HEAD(arc_qhead, arc_item) qhead;
+	int qcount;
+	struct arc_item item_list[ARCLEN]; /* We use static memory for demo purposes */
+};
+
+inline static struct arc_item * allocmember(struct arc_list *);
+inline static void freemember(struct arc_item *);
+inline static struct arc_item * findmember(struct arc_list *, struct arc_item *);
+
+#define init_arc_item(/* &struct arc_item [] */ _arc_item_addr,			\
+		      /* int */_iid, /*bool*/_cached)	do {			\
+		struct arc_item *_arc_item = _arc_item_addr;			\
+		assert(_arc_item != NULL);				\
+		_arc_item->iid = _iid;						\
+		_arc_item->cached = _cached;					\
+	} while (/*CONSTCOND*/0)
+
+#define lengthof(/* struct arc_list* */_arc_list) (_arc_list->qcount)
+#define memberof(/* struct arc_list* */_arc_list,				\
+		 /* struct arc_item* */_arc_item)				\
+	((findmember(_arc_list,							\
+		     _arc_item) != TAILQ_END(&_arc_list->qhead)) ?		\
+	 true : false)
+
+/*
+ * We follow spin's channel rx/tx semantics here: "send" means
+ * duplicate onto queue ("_arc_list.item_list!_arc_item.iid"), and
+ * recieve means "duplicate" from queue but leave the data source on
+ * queue  ("_arc_list.item_list?<_arc_item.iid>").
+ *
+ * It is an error to addMRU() on a full queue. Likewise, it is an
+ * error to readLRU() on an empty queue. The verifier is expected to
+ * have covered any case where these happen. We use assert()s to
+ * indicate the error.
+ *
+ * Note: We use spin's channel mechanism in our design, only because
+ * it's the easiest. We could have chosen another
+ * mechanism/implementation, if the semantics were specified
+ * differently due to, for eg: convention, architectural or efficiency
+ * reasons.
+ */
+#define addMRU(/* struct arc_list* */_arc_list,					\
+	       /* struct arc_item* */_arc_item) do {				\
+		_arc_list->qcount++; assert(_arc_list->qcount < ARCLEN);	\
+		struct arc_item *aitmp = allocmember(_arc_list);		\
+		assert(aitmp != NULL);						\
+		*aitmp = *_arc_item;						\
+		TAILQ_INSERT_TAIL(&_arc_list->qhead, aitmp, qlink);	\
+	} while (/*CONSTCOND*/0)
+
+#define readLRU(/* struct arc_list* */_arc_list,				\
+		/* struct arc_item* */_arc_item) do {				\
+		assert(!TAILQ_EMPTY(&_arc_list->qhead));			\
+		assert(_arc_item != NULL);					\
+		*_arc_item = *(struct arc_item *)TAILQ_FIRST(&_arc_list->qhead);\
+	} while (/*CONSTCOND*/0)
+		
+#define delLRU(/* struct arc_list* */_arc_list)					\
+	if (!TAILQ_EMPTY(&_arc_list->qhead)) {					\
+		struct arc_item *aitmp = TAILQ_FIRST(&_arc_list->qhead);	\
+		TAILQ_REMOVE(&_arc_list->qhead, aitmp, qlink);			\
+		freemember(aitmp);						\
+		_arc_list->qcount--; assert(_arc_list->qcount >= 0);		\
+	} else assert(false)
+
+#define delitem(/* struct arc_list* */_arc_list,				\
+		/* struct arc_item* */_arc_item) do {				\
+	struct arc_item *aitmp;							\
+	aitmp = findmember(_arc_list, _arc_item);				\
+	if (aitmp != TAILQ_END(&_arc_list->qhead)) {				\
+		TAILQ_REMOVE(&_arc_list->qhead, aitmp, qlink);		\
+		freemember(aitmp);						\
+		_arc_list->qcount--; assert(_arc_list->qcount >= 0);		\
+	}									\
+	} while (/*CONSTCOND*/0)
+
+#define cachefetch(/* struct arc_item* */_arc_item) do {			\
+		_arc_item->cached = true; /* XXX:TODO */			\
+	} while (/*CONSTCOND*/0)
+
+#define cacheremove(/* struct arc_item* */_arc_item)  do {			\
+		_arc_item->cached = false;	/* XXX:TODO */			\
+	} while (/*CONSTCOND*/0)
+
+#define min(a, b) ((a < b) ? a : b)
+#define max(a, b) ((a > b) ? a : b)
+	
+/* These routines deal with our home-rolled mem management for the
+ * ghost cache directory memory embedded within statically defined
+ * struct arc_list buffers.
+ * Note that any pointers emerging from these should be treated as
+ * "opaque"/cookies - ie; they should not be assumed by other routines
+ * to have any specific properties (such as being part of any specific
+ * array etc.) They are solely for the consumption of these
+ * routines. Their contents however may be freely copied/written to.
+ */
+inline static struct arc_item *
+allocmember(struct arc_list *_arc_list)
+{
+	/* Search for the first unallocated item in given list */
+	struct arc_item *aitmp = NULL;
+	int i;
+	for (i = 0; i < ARCLEN; i++) {
+		if (_arc_list->item_list[i].iid == IID_INVAL) {
+			assert(_arc_list->item_list[i].cached == false);
+			aitmp = &_arc_list->item_list[i];
+		}
+	}
+	return aitmp;
+			
+}
+	
+inline static void
+freemember(struct arc_item *_arc_item)
+{
+	init_arc_item(_arc_item, IID_INVAL, false);
+}	
+
+static inline struct arc_item *
+findmember(struct arc_list *_arc_list, struct arc_item *aikey)
+{
+	assert(_arc_list != NULL && aikey != NULL);
+	assert(aikey->iid != IID_INVAL);
+	struct arc_item *aitmp;
+	TAILQ_FOREACH(aitmp, &_arc_list->qhead, qlink) {
+			if (aitmp->iid == aikey->iid) {
+				return aitmp;
+			}
+	}
+	return aitmp; /* returns TAILQ_END() on non-membership */
+}
+
+void ARC(struct arc_item * /* x_t */);
+void arc_init(void);
+
+#endif /* _ARC_H_ */
diff -urN arc.null/arc.inv arc/arc.inv
--- arc.null/arc.inv	1970-01-01 00:00:00.000000000 +0000
+++ arc/arc.inv	2023-09-04 09:20:20.224107390 +0000
@@ -0,0 +1,59 @@
+/* $NetBSD$ */
+
+/* These are Linear Temporal Logic invariants (and constraints)
+ * applied over the statespace created by the promela
+ * specification. Correctness is implied by Logical consistency.
+ */
+ltl 
+{
+	/* Liveness - all threads, except control must finally exit */
+	eventually always (_nr_pr == 1) &&
+	/* c.f Section I. B, on page 3 of paper */
+	always ((lengthof(T1) +
+	         lengthof(B1) +
+	         lengthof(T2) +
+	         lengthof(B2)) <= (2 * C)) &&
+
+	/* Reading together Section III. A., on page 7, and
+	 * Section III. B., on pages  7,8
+	 */
+	always ((lengthof(T1) + lengthof(B1)) <= C) &&
+	always ((lengthof(T2) + lengthof(B2)) < (2 * C)) &&
+
+	/* Section III. B, Remark III.1	*/
+	always ((lengthof(T1) + lengthof(T2)) <= C) &&
+
+	/* TODO: III B, A.1 */
+
+	/* III B, A.2 */
+	always (((lengthof(T1) +
+	          lengthof(B1) +
+	          lengthof(T2) +
+	          lengthof(B2)) < C)
+		 implies ((lengthof(B1) == 0) &&
+			   lengthof(B2) == 0)) &&
+
+	/* III B, A.3 */
+	always (((lengthof(T1) +
+	          lengthof(B1) +
+	          lengthof(T2) +
+	          lengthof(B2)) >= C)
+		 implies ((lengthof(T1) +
+		 	   lengthof(T2) == C))) &&
+
+	/* TODO: III B, A.4 */
+
+	/* TODO: III B, A.5 */
+
+	/* IV A. */
+	always (p <= C) &&
+
+	/* Not strictly true, but these force us to generate a "good"
+	 * input trace via arc.drv
+	 */
+
+	eventually /* always ? */ ((lengthof(T1) == p) && lengthof(T2) == (C - p)) &&
+
+	eventually (p > 0)
+		
+}
diff -urN arc.null/arc.pmh arc/arc.pmh
--- arc.null/arc.pmh	1970-01-01 00:00:00.000000000 +0000
+++ arc/arc.pmh	2023-09-08 10:36:52.827695101 +0000
@@ -0,0 +1,38 @@
+/* Spin process model for Adaptive Replacement Cache algorithm. Written by cherry */
+
+#ifndef _ARC_INC
+#define _ARC_INC
+
+#define C 64 /* Cache size - use judiciously - adds to statespace */
+
+typedef arc_item {
+	int iid;    /* Unique identifier for item */
+	bool cached;
+};
+
+/* Note that we use the arc_item.iid as the member lookup handle to reduce state space */
+typedef arc_list {
+	chan item_list  = [ 2 * C ] of { int }; /* A list of page items */
+};
+
+
+#define init_arc_item(_arc_item, _iid, _cached)		\
+	{		       			\
+		_arc_item.iid = _iid;	       		\
+		_arc_item.cached = _cached;		\
+	}
+
+#define lengthof(_arc_list) len(_arc_list.item_list)
+#define memberof(_arc_list, _arc_item) _arc_list.item_list??[eval(_arc_item.iid)]
+#define addMRU(_arc_list, _arc_item) _arc_list.item_list!_arc_item.iid
+#define readLRU(_arc_list, _arc_item) _arc_list.item_list?<_arc_item.iid>
+#define delLRU(_arc_list) _arc_list.item_list?_
+#define delitem(_arc_list, _arc_item) _arc_list.item_list??eval(_arc_item.iid)
+
+#define cachefetch(_arc_item) _arc_item.cached = true
+#define cacheremove(_arc_item) _arc_item.cached = false
+
+#define min(a, b) ((a < b) -> a : b)
+#define max(a, b) ((a > b) -> a : b)
+	
+#endif /* _ARC_INC_ */
\ No newline at end of file
diff -urN arc.null/arc.pml arc/arc.pml
--- arc.null/arc.pml	1970-01-01 00:00:00.000000000 +0000
+++ arc/arc.pml	2023-09-08 10:34:47.759024169 +0000
@@ -0,0 +1,216 @@
+/* Spin process model for Adaptive Replacement Cache algorithm. Written by cherry */
+
+/*
+ * We implement the following algorithm from page 10, Figure 4.
+ * https://www.usenix.org/legacy/events/fast03/tech/full_papers/megiddo/megiddo.pdf
+ *
+ *
+ *  ARC(c)
+ *  
+ *  INPUT: The request stream x1,x2,....,xt,....
+ *  INITIALIZATION: Set p = 0 and set the LRU lists T1, B1, T2, and B2 to empty.
+ *  
+ *  For every t>=1 and any xt, one and only one of the following four cases must occur.
+ *  Case I: xt is in T1 or T2. A cache hit has occurred in ARC(c) and DBL(2c).
+ *       Move xt to MRU position in T2.
+ *  
+ *  Case II: xt is in B1. A cache miss (resp. hit) has occurred in ARC(c) (resp. DBL(2c)).
+ *       	 ADAPTATION: Update p = min { p + d1,c }
+ *  	 	     where d1 = { 1 if |B1| >= |B2|, |B2|/|B1| otherwise
+ *  
+ *       REPLACE(xt, p). Move xt from B1 to the MRU position in T2 (also fetch xt to the cache).
+ *  
+ *  Case III: xt is in B2. A cache miss (resp. hit) has occurred in ARC(c) (resp. DBL(2c)).
+ *       	 ADAPTATION: Update p = max { p - d2,0 }
+ *  	 	     where d2 = { 1 if |B2| >= |B1|, |B1|/|B2| otherwise
+ *  
+ *       REPLACE(xt, p). Move xt from B2 to the MRU position in T2 (also fetch xt to the cache).
+ *       
+ *  Case IV: xt is not in T1 U B1 U T2 U B2. A cache miss has occurred in ARC(c) and DBL(2c).
+ *       Case A: L1 = T1 U B1 has exactly c pages.
+ *       	  If (|T1| < c)
+ *  	     	     	Delete LRU page in B1. REPLACE(xt,p).
+ *  	  	  else
+ *			Here B1 is empty. Delete LRU page in T1 (also remove it from the cache).
+ *  	  	  endif
+ *       Case B: L1 = T1 U B1 has less than c pages.
+ *       	  If (|T1| + |T2| + |B1| + |B2| >= c)
+ *  	             Delete LRU page in B2, if (|T1| + |T2| + |B1| + |B2| = 2c).
+ *  		     REPLACE(xt, p).
+ *  	  	  endif
+ *  
+ *       Finally, fetch xt to the cache and move it to MRU position in T1.
+ *  
+ *  Subroutine REPLACE(xt,p)
+ *       If ( (|T1| is not empty) and ((|T1| exceeds the target p) or (xt is in B2 and |T1| = p)) )
+ *       	  Delete the LRU page in T1 (also remove it from the cache), and move it to MRU position in B1.
+ *       else
+ *		  Delete the LRU page in T2 (also remove it from the cache), and move it to MRU position in B2.
+ *       endif
+ */
+ 
+/* #include "arc.pmh" See Makefile */
+
+#define IID_INVAL -1 /* XXX: move to header ? */
+
+/* Temp variable to hold LRU item */
+hidden arc_item LRUitem;
+
+/* Adaptation "delta" variables */
+int d1, d2;
+int p = 0;
+
+/* Declare arc lists - "shadow/ghost cache directories" */
+arc_list B1, B2, T1, T2;
+
+inline REPLACE(/* arc_item */ x_t, /* int */ p)
+{
+	/*
+	 * Since LRUitem is declared in scope p_ARC, we expect it to be only accessible from there and REPLACE()
+	 * as REPLACE() is only expected to be called from p_ARC.
+	 * XXX: May need to revisit due to Modex related limitations.
+	 */
+	init_arc_item(LRUitem, IID_INVAL, false);
+	
+	if
+		::
+		(lengthof(T1) != 0) &&
+		((lengthof(T1) > p) || (memberof(B2, x_t) && (lengthof(T1) == p)))
+		->
+		{
+		       readLRU(T1, LRUitem);
+		       delLRU(T1);
+		       cacheremove(LRUitem);
+		       addMRU(B1, LRUitem);
+		}
+
+		::
+		else
+		->
+		{
+		       readLRU(T2, LRUitem);
+		       delLRU(T2);
+		       cacheremove(LRUitem);
+		       addMRU(B2, LRUitem);
+		}
+	fi
+}
+
+inline ARC(/* arc_item */ x_t)
+{
+	if
+		:: /* Case I */
+		memberof(T1, x_t)
+		->
+		{
+		       delitem(T1, x_t);
+		       addMRU(T2, x_t);
+		}
+		:: /* Case I */
+		memberof(T2, x_t)
+		->
+		{
+		       delitem(T2, x_t);
+		       addMRU(T2, x_t);
+		}
+		:: /* Case II */
+		memberof(B1, x_t)
+		->
+		d1 = ((lengthof(B1) >= lengthof(B2)) -> 1 : (lengthof(B2)/lengthof(B1)));
+		p = min((p + d1), C);
+
+		REPLACE(x_t, p);
+		{
+		       delitem(B1, x_t);
+		       addMRU(T2, x_t);
+		       cachefetch(x_t);
+		}
+		:: /* Case III */
+		memberof(B2, x_t)
+		->
+		d2 = ((lengthof(B2) >= lengthof(B1)) -> 1 : (lengthof(B1)/lengthof(B2)));
+		p = max(p - d2, 0);
+		
+		REPLACE(x_t, p);
+		{
+		       delitem(B2, x_t);
+		       addMRU(T2, x_t);
+		       cachefetch(x_t);
+		}
+		:: /* Case IV */
+		!(memberof(T1, x_t) ||
+		  memberof(B1, x_t) ||
+		  memberof(T2, x_t) ||
+		  memberof(B2, x_t))
+		->
+		if
+			:: /* Case A */
+			((lengthof(T1) + lengthof(B1)) == C)
+			->
+			if
+				::
+				(lengthof(T1) < C)
+				->
+				delLRU(B1);
+				REPLACE(x_t, p);
+				::
+				else
+				->
+				assert(lengthof(B1) == 0);
+				{
+				       readLRU(T1, LRUitem);
+				       delLRU(T1);
+				       cacheremove(LRUitem);
+				}
+			fi
+			:: /* Case B */
+			((lengthof(T1) + lengthof(B1)) < C)
+			->
+			if
+				::
+				((lengthof(T1) +
+				  lengthof(T2) +
+				  lengthof(B1) +
+				  lengthof(B2)) >= C)
+				->
+				if
+					::
+					((lengthof(T1) +
+				  	  lengthof(T2) +
+				  	  lengthof(B1) +
+				  	  lengthof(B2)) == (2 * C))
+					->
+					delLRU(B2);
+					::
+					else
+					->
+					skip;
+				fi
+				REPLACE(x_t, p);
+				::
+				else
+				->
+				skip;
+			fi
+			::
+			else
+			->
+			skip;
+		fi
+		cachefetch(x_t);
+		addMRU(T1, x_t);
+	fi
+
+}
+
+#if 0 /* Resolve this after modex extract foo */
+proctype p_arc(arc_item x_t)
+{
+	/* Serialise entry */	
+	mutex_enter(sc_lock);
+
+	ARC(x_t);
+
+	mutex_exit(sc_lock);
+}
+#endif
diff -urN arc.null/arc.prx arc/arc.prx
--- arc.null/arc.prx	1970-01-01 00:00:00.000000000 +0000
+++ arc/arc.prx	2023-09-07 17:35:35.607923403 +0000
@@ -0,0 +1,81 @@
+// Spin model extractor harness written by cherry
+//
+%F arc.c
+%X -n REPLACE
+%X -n ARC
+%H
+// Disable effects of all included files and try to implement a subset of the APIs they provide.
+#define _ARC_H_
+%%
+//%C  // c_code {}
+//%%
+//%D // c_cdecl {}
+//%%
+%L
+// We use spin primitives and data objects.
+// See %P Below
+NonState	hidden	_LRUitem
+NonState	hidden	LRUitem
+NonState	hidden	_B2
+NonState	hidden	B2
+NonState	hidden	_B1
+NonState	hidden	B1
+NonState	hidden	_T2
+NonState	hidden	T2
+NonState	hidden	_T1
+NonState	hidden	T1
+NonState	hidden	x_t
+
+
+
+assert(...		keep
+REPLACE(...		keep
+init_arc_item(...	keep
+lengthof(...		keep
+memberof(...		keep
+addMRU(...		keep
+readLRU(...		keep
+delLRU(...		keep
+delitem(...		keep
+cacheremove(...		keep
+cachefetch(...		keep
+
+
+Substitute		c_expr { ((lengthof(T1)!=0)&&((lengthof(T1)>now.p)||(memberof(B2,x_t)&&(lengthof(T1)==now.p)))) }	(lengthof(T1) != 0) && ((lengthof(T1) > p) || (memberof(B2, x_t) && (lengthof(T1) == p)))
+Substitute		c_code { now.d1=((lengthof(B1)>=lengthof(B2)) ? Int 1\n : (lengthof(B2)/lengthof(B1))); }	d1 = ((lengthof(B1) >= lengthof(B2)) -> 1 : (lengthof(B2)/lengthof(B1)))
+Substitute		c_code { now.p=min((now.p+now.d1),C); }	 p = min((p + d1), C)
+
+Substitute		c_code { now.d2=((lengthof(B2)>=lengthof(B1)) ? Int 1\n : (lengthof(B1)/lengthof(B2))); }	d2 = ((lengthof(B2) >= lengthof(B1)) -> 1 : (lengthof(B1)/lengthof(B2)));
+Substitute		c_code { now.p=max((now.p-now.d2),0); }		      	  p = max(p - d2, 0);
+Substitute		c_expr { (!(((memberof(T1,x_t)||memberof(B1,x_t))||memberof(T2,x_t))||memberof(B2,x_t))) }			!(memberof(T1, x_t) || memberof(B1, x_t) || memberof(T2, x_t) ||  memberof(B2, x_t))
+Substitute		c_expr { ((lengthof(T1)+lengthof(B1))==C) }	((lengthof(T1) + lengthof(B1)) == C)
+Substitute		c_expr { (lengthof(T1)<C) }	(lengthof(T1) < C)
+Substitute		c_expr { ((lengthof(T1)+lengthof(B1))<C) }	((lengthof(T1) + lengthof(B1)) < C)
+Substitute		c_expr { ((((lengthof(T1)+lengthof(T2))+lengthof(B1))+lengthof(B2))>=C) }	((lengthof(T1) + lengthof(T2) + lengthof(B1) + lengthof(B2)) >= C)
+Substitute		c_expr { ((((lengthof(T1)+lengthof(T2))+lengthof(B1))+lengthof(B2))==(2*C)) }	((lengthof(T1) + lengthof(T2) + lengthof(B1) + lengthof(B2)) == (2 * C))
+%%
+
+%P
+#define IID_INVAL -1 /* XXX: move to header ? */
+
+/* Temp variable to hold LRU item */
+hidden arc_item LRUitem;
+
+arc_list B1, B2, T1, T2;
+
+#define p_REPLACE(_arg1, _arg2) REPLACE(_arg1, _arg2) /* Demo arbitrary Cfunc->PMLproc transformation */
+inline p_REPLACE(/* arc_item */ x_t, /* int */ p)
+{
+
+#include "_modex_REPLACE.pml"
+
+}
+
+#define p_ARC(_arg1) ARC(_arg1)
+inline p_ARC(/* arc_item */ x_t)
+{
+
+#include "_modex_ARC.pml"
+
+}
+%%
\ No newline at end of file
diff -urN arc.null/Makefile arc/Makefile
--- arc.null/Makefile	1970-01-01 00:00:00.000000000 +0000
+++ arc/Makefile	2023-09-08 10:32:11.650504807 +0000
@@ -0,0 +1,93 @@
+# This set of spinroot related files were written by cherry
+# <c%bow.st@localhost> in the Gregorian Calendar year AD.2023, in the month
+# of February that year.
+#
+# We have two specification files and a properties file
+#
+# The properties file contains "constraint" sections
+# such as ltl or never claims (either or, not both).
+# The specification is divided into two files:
+# the file with suffix '.drv' is a "driver" which
+# instantiates processes that will ultimately "drive" the
+# models under test.
+# The file with the suffix '.pml' contains the process
+# model code, which, is intended to be the formal specification
+# for the code we are interested in writing in C.
+#
+# We process these files in slightly different ways during
+# the dev cycle, but broadly speaking, the idea is to create
+# a file called 'spinmodel.pml' which contains the final
+# model file that is fed to spin.
+#
+# Note that when we use the model extractor tool "modex" to
+# extract the 'specification' from C code written to implement
+# the model defined above. We use a 'harness' file (see file with
+# suffix '.prx' below.
+#
+# Once the harness has been run, spinmodel.pml should be
+# synthesised and processed as usual.
+# 
+# The broad idea is that software dev starts by writing the spec
+# first, validating the model, and then implementing the model in
+# C, after which we come back to extract the model from the C file
+# and cross check our implementation using spin.
+#
+# If things go well, the constraints specified in the '.ltl' file
+# should hold exactly for both the handwritten model, and the
+# extracted one.
+
+spin-gen: arc.pml arc.drv arc.inv
+	cp arc.pml model #mimic modex
+	cat arc.pmh model > spinmodel.pml;cat arc.drv >> spinmodel.pml;cat arc.inv >> spinmodel.pml;
+	spin -am spinmodel.pml
+
+spin-build: #Could be spin-gen or modex-gen
+	cc -DVECTORSZ=65536 -o pan pan.c
+
+all: spin-gen spin-build prog
+
+# Verification related targets.
+spin-run: spin-build
+	./pan -a #Generate arc.pml.trail	on error
+
+# You run the trace only if the spin run above failed and created a trail
+spin-trace: spinmodel.pml.trail
+	spin -t spinmodel.pml -p -g #  -p (statements) -g (globals) -l (locals) -s (send) -r (recv)
+	./pan -r spinmodel.pml.trail -g
+
+# Build the implementation
+prog: arc.c arc.h
+	cc -g -o arc arc_drv.c arc.c
+
+# Modex Extracts from C code to 'model' - see arc.prx
+# Unfortunately there doesn't seem to be a way to specify a filename to generate
+modex-gen: arc.prx arc.c
+	modex -v -w arc.prx
+	cat arc.pmh model > spinmodel.pml;cat arc.drv >> spinmodel.pml;cat arc.inv >> spinmodel.pml;
+	spin -a spinmodel.pml #Sanity check
+
+# Housekeeping
+modex-gen-clean:
+	rm -f spinmodel.pml # Our consolidated model file
+	rm -f _spin_nvr.tmp # Never claim file
+	rm -f model # modex generated intermediate "model" file
+	rm -f pan.* # Spin generated source files
+	rm -f _modex* # modex generated script files
+	rm -f  *.I *.M
+
+prog-clean:
+	rm -f arc
+spin-run-clean:
+	rm -f spinmodel.pml.trail
+
+spin-build-clean:
+	rm -f pan
+
+spin-gen-clean:
+	rm -f spinmodel.pml # Our consolidated model file
+	rm -f _spin_nvr.tmp # Never claim file
+	rm -f model # Intermediate "model" file
+	rm -f pan.* # Spin generated source files
+
+clean: modex-gen-clean spin-gen-clean spin-build-clean spin-run-clean prog-clean
+	rm -f *~
diff -urN arc.null/queue.h arc/queue.h
--- arc.null/queue.h	1970-01-01 00:00:00.000000000 +0000
+++ arc/queue.h	2021-01-16 23:51:51.000000000 +0000
@@ -0,0 +1,655 @@
+/*	$NetBSD: queue.h,v 1.76 2021/01/16 23:51:51 chs Exp $	*/
+
+/*
+ * Copyright (c) 1991, 1993
+ *	The Regents of the University of California.  All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the distribution.
+ * 3. Neither the name of the University nor the names of its contributors
+ *    may be used to endorse or promote products derived from this software
+ *    without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND
+ * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED.  IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+ * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+ * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+ * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+ * SUCH DAMAGE.
+ *
+ *	@(#)queue.h	8.5 (Berkeley) 8/20/94
+ */
+
+#ifndef	_SYS_QUEUE_H_
+#define	_SYS_QUEUE_H_
+
+/*
+ * This file defines five types of data structures: singly-linked lists,
+ * lists, simple queues, tail queues, and circular queues.
+ *
+ * A singly-linked list is headed by a single forward pointer. The
+ * elements are singly linked for minimum space and pointer manipulation
+ * overhead at the expense of O(n) removal for arbitrary elements. New
+ * elements can be added to the list after an existing element or at the
+ * head of the list.  Elements being removed from the head of the list
+ * should use the explicit macro for this purpose for optimum
+ * efficiency. A singly-linked list may only be traversed in the forward
+ * direction.  Singly-linked lists are ideal for applications with large
+ * datasets and few or no removals or for implementing a LIFO queue.
+ *
+ * A list is headed by a single forward pointer (or an array of forward
+ * pointers for a hash table header). The elements are doubly linked
+ * so that an arbitrary element can be removed without a need to
+ * traverse the list. New elements can be added to the list before
+ * or after an existing element or at the head of the list. A list
+ * may only be traversed in the forward direction.
+ *
+ * A simple queue is headed by a pair of pointers, one the head of the
+ * list and the other to the tail of the list. The elements are singly
+ * linked to save space, so elements can only be removed from the
+ * head of the list. New elements can be added to the list after
+ * an existing element, at the head of the list, or at the end of the
+ * list. A simple queue may only be traversed in the forward direction.
+ *
+ * A tail queue is headed by a pair of pointers, one to the head of the
+ * list and the other to the tail of the list. The elements are doubly
+ * linked so that an arbitrary element can be removed without a need to
+ * traverse the list. New elements can be added to the list before or
+ * after an existing element, at the head of the list, or at the end of
+ * the list. A tail queue may be traversed in either direction.
+ *
+ * For details on the use of these macros, see the queue(3) manual page.
+ */
+
+/*
+ * Include the definition of NULL only on NetBSD because sys/null.h
+ * is not available elsewhere.  This conditional makes the header
+ * portable and it can simply be dropped verbatim into any system.
+ * The caveat is that on other systems some other header
+ * must provide NULL before the macros can be used.
+ */
+#ifdef __NetBSD__
+#include <sys/null.h>
+#endif
+
+#if defined(_KERNEL) && defined(DIAGNOSTIC)
+#define QUEUEDEBUG	1
+#endif
+
+#if defined(QUEUEDEBUG)
+# if defined(_KERNEL)
+#  define QUEUEDEBUG_ABORT(...) panic(__VA_ARGS__)
+# else
+#  include <err.h>
+#  define QUEUEDEBUG_ABORT(...) err(1, __VA_ARGS__)
+# endif
+#endif
+
+/*
+ * Singly-linked List definitions.
+ */
+#define	SLIST_HEAD(name, type)						\
+struct name {								\
+	struct type *slh_first;	/* first element */			\
+}
+
+#define	SLIST_HEAD_INITIALIZER(head)					\
+	{ NULL }
+
+#define	SLIST_ENTRY(type)						\
+struct {								\
+	struct type *sle_next;	/* next element */			\
+}
+
+/*
+ * Singly-linked List access methods.
+ */
+#define	SLIST_FIRST(head)	((head)->slh_first)
+#define	SLIST_END(head)		NULL
+#define	SLIST_EMPTY(head)	((head)->slh_first == NULL)
+#define	SLIST_NEXT(elm, field)	((elm)->field.sle_next)
+
+#define	SLIST_FOREACH(var, head, field)					\
+	for((var) = (head)->slh_first;					\
+	    (var) != SLIST_END(head);					\
+	    (var) = (var)->field.sle_next)
+
+#define	SLIST_FOREACH_SAFE(var, head, field, tvar)			\
+	for ((var) = SLIST_FIRST((head));				\
+	    (var) != SLIST_END(head) &&					\
+	    ((tvar) = SLIST_NEXT((var), field), 1);			\
+	    (var) = (tvar))
+
+/*
+ * Singly-linked List functions.
+ */
+#define	SLIST_INIT(head) do {						\
+	(head)->slh_first = SLIST_END(head);				\
+} while (/*CONSTCOND*/0)
+
+#define	SLIST_INSERT_AFTER(slistelm, elm, field) do {			\
+	(elm)->field.sle_next = (slistelm)->field.sle_next;		\
+	(slistelm)->field.sle_next = (elm);				\
+} while (/*CONSTCOND*/0)
+
+#define	SLIST_INSERT_HEAD(head, elm, field) do {			\
+	(elm)->field.sle_next = (head)->slh_first;			\
+	(head)->slh_first = (elm);					\
+} while (/*CONSTCOND*/0)
+
+#define	SLIST_REMOVE_AFTER(slistelm, field) do {			\
+	(slistelm)->field.sle_next =					\
+	    SLIST_NEXT(SLIST_NEXT((slistelm), field), field);		\
+} while (/*CONSTCOND*/0)
+
+#define	SLIST_REMOVE_HEAD(head, field) do {				\
+	(head)->slh_first = (head)->slh_first->field.sle_next;		\
+} while (/*CONSTCOND*/0)
+
+#define	SLIST_REMOVE(head, elm, type, field) do {			\
+	if ((head)->slh_first == (elm)) {				\
+		SLIST_REMOVE_HEAD((head), field);			\
+	}								\
+	else {								\
+		struct type *curelm = (head)->slh_first;		\
+		while(curelm->field.sle_next != (elm))			\
+			curelm = curelm->field.sle_next;		\
+		curelm->field.sle_next =				\
+		    curelm->field.sle_next->field.sle_next;		\
+	}								\
+} while (/*CONSTCOND*/0)
+
+
+/*
+ * List definitions.
+ */
+#define	LIST_HEAD(name, type)						\
+struct name {								\
+	struct type *lh_first;	/* first element */			\
+}
+
+#define	LIST_HEAD_INITIALIZER(head)					\
+	{ NULL }
+
+#define	LIST_ENTRY(type)						\
+struct {								\
+	struct type *le_next;	/* next element */			\
+	struct type **le_prev;	/* address of previous next element */	\
+}
+
+/*
+ * List access methods.
+ */
+#define	LIST_FIRST(head)		((head)->lh_first)
+#define	LIST_END(head)			NULL
+#define	LIST_EMPTY(head)		((head)->lh_first == LIST_END(head))
+#define	LIST_NEXT(elm, field)		((elm)->field.le_next)
+
+#define	LIST_FOREACH(var, head, field)					\
+	for ((var) = ((head)->lh_first);				\
+	    (var) != LIST_END(head);					\
+	    (var) = ((var)->field.le_next))
+
+#define	LIST_FOREACH_SAFE(var, head, field, tvar)			\
+	for ((var) = LIST_FIRST((head));				\
+	    (var) != LIST_END(head) &&					\
+	    ((tvar) = LIST_NEXT((var), field), 1);			\
+	    (var) = (tvar))
+
+#define	LIST_MOVE(head1, head2, field) do {				\
+	LIST_INIT((head2));						\
+	if (!LIST_EMPTY((head1))) {					\
+		(head2)->lh_first = (head1)->lh_first;			\
+		(head2)->lh_first->field.le_prev = &(head2)->lh_first;	\
+		LIST_INIT((head1));					\
+	}								\
+} while (/*CONSTCOND*/0)
+
+/*
+ * List functions.
+ */
+#if defined(QUEUEDEBUG)
+#define	QUEUEDEBUG_LIST_INSERT_HEAD(head, elm, field)			\
+	if ((head)->lh_first &&						\
+	    (head)->lh_first->field.le_prev != &(head)->lh_first)	\
+		QUEUEDEBUG_ABORT("LIST_INSERT_HEAD %p %s:%d", (head),	\
+		    __FILE__, __LINE__);
+#define	QUEUEDEBUG_LIST_OP(elm, field)					\
+	if ((elm)->field.le_next &&					\
+	    (elm)->field.le_next->field.le_prev !=			\
+	    &(elm)->field.le_next)					\
+		QUEUEDEBUG_ABORT("LIST_* forw %p %s:%d", (elm),		\
+		    __FILE__, __LINE__);				\
+	if (*(elm)->field.le_prev != (elm))				\
+		QUEUEDEBUG_ABORT("LIST_* back %p %s:%d", (elm),		\
+		    __FILE__, __LINE__);
+#define	QUEUEDEBUG_LIST_POSTREMOVE(elm, field)				\
+	(elm)->field.le_next = (void *)1L;				\
+	(elm)->field.le_prev = (void *)1L;
+#else
+#define	QUEUEDEBUG_LIST_INSERT_HEAD(head, elm, field)
+#define	QUEUEDEBUG_LIST_OP(elm, field)
+#define	QUEUEDEBUG_LIST_POSTREMOVE(elm, field)
+#endif
+
+#define	LIST_INIT(head) do {						\
+	(head)->lh_first = LIST_END(head);				\
+} while (/*CONSTCOND*/0)
+
+#define	LIST_INSERT_AFTER(listelm, elm, field) do {			\
+	QUEUEDEBUG_LIST_OP((listelm), field)				\
+	if (((elm)->field.le_next = (listelm)->field.le_next) != 	\
+	    LIST_END(head))						\
+		(listelm)->field.le_next->field.le_prev =		\
+		    &(elm)->field.le_next;				\
+	(listelm)->field.le_next = (elm);				\
+	(elm)->field.le_prev = &(listelm)->field.le_next;		\
+} while (/*CONSTCOND*/0)
+
+#define	LIST_INSERT_BEFORE(listelm, elm, field) do {			\
+	QUEUEDEBUG_LIST_OP((listelm), field)				\
+	(elm)->field.le_prev = (listelm)->field.le_prev;		\
+	(elm)->field.le_next = (listelm);				\
+	*(listelm)->field.le_prev = (elm);				\
+	(listelm)->field.le_prev = &(elm)->field.le_next;		\
+} while (/*CONSTCOND*/0)
+
+#define	LIST_INSERT_HEAD(head, elm, field) do {				\
+	QUEUEDEBUG_LIST_INSERT_HEAD((head), (elm), field)		\
+	if (((elm)->field.le_next = (head)->lh_first) != LIST_END(head))\
+		(head)->lh_first->field.le_prev = &(elm)->field.le_next;\
+	(head)->lh_first = (elm);					\
+	(elm)->field.le_prev = &(head)->lh_first;			\
+} while (/*CONSTCOND*/0)
+
+#define	LIST_REMOVE(elm, field) do {					\
+	QUEUEDEBUG_LIST_OP((elm), field)				\
+	if ((elm)->field.le_next != NULL)				\
+		(elm)->field.le_next->field.le_prev = 			\
+		    (elm)->field.le_prev;				\
+	*(elm)->field.le_prev = (elm)->field.le_next;			\
+	QUEUEDEBUG_LIST_POSTREMOVE((elm), field)			\
+} while (/*CONSTCOND*/0)
+
+#define LIST_REPLACE(elm, elm2, field) do {				\
+	if (((elm2)->field.le_next = (elm)->field.le_next) != NULL)	\
+		(elm2)->field.le_next->field.le_prev =			\
+		    &(elm2)->field.le_next;				\
+	(elm2)->field.le_prev = (elm)->field.le_prev;			\
+	*(elm2)->field.le_prev = (elm2);				\
+	QUEUEDEBUG_LIST_POSTREMOVE((elm), field)			\
+} while (/*CONSTCOND*/0)
+
+/*
+ * Simple queue definitions.
+ */
+#define	SIMPLEQ_HEAD(name, type)					\
+struct name {								\
+	struct type *sqh_first;	/* first element */			\
+	struct type **sqh_last;	/* addr of last next element */		\
+}
+
+#define	SIMPLEQ_HEAD_INITIALIZER(head)					\
+	{ NULL, &(head).sqh_first }
+
+#define	SIMPLEQ_ENTRY(type)						\
+struct {								\
+	struct type *sqe_next;	/* next element */			\
+}
+
+/*
+ * Simple queue access methods.
+ */
+#define	SIMPLEQ_FIRST(head)		((head)->sqh_first)
+#define	SIMPLEQ_END(head)		NULL
+#define	SIMPLEQ_EMPTY(head)		((head)->sqh_first == SIMPLEQ_END(head))
+#define	SIMPLEQ_NEXT(elm, field)	((elm)->field.sqe_next)
+
+#define	SIMPLEQ_FOREACH(var, head, field)				\
+	for ((var) = ((head)->sqh_first);				\
+	    (var) != SIMPLEQ_END(head);					\
+	    (var) = ((var)->field.sqe_next))
+
+#define	SIMPLEQ_FOREACH_SAFE(var, head, field, next)			\
+	for ((var) = ((head)->sqh_first);				\
+	    (var) != SIMPLEQ_END(head) &&				\
+	    ((next = ((var)->field.sqe_next)), 1);			\
+	    (var) = (next))
+
+/*
+ * Simple queue functions.
+ */
+#define	SIMPLEQ_INIT(head) do {						\
+	(head)->sqh_first = NULL;					\
+	(head)->sqh_last = &(head)->sqh_first;				\
+} while (/*CONSTCOND*/0)
+
+#define	SIMPLEQ_INSERT_HEAD(head, elm, field) do {			\
+	if (((elm)->field.sqe_next = (head)->sqh_first) == NULL)	\
+		(head)->sqh_last = &(elm)->field.sqe_next;		\
+	(head)->sqh_first = (elm);					\
+} while (/*CONSTCOND*/0)
+
+#define	SIMPLEQ_INSERT_TAIL(head, elm, field) do {			\
+	(elm)->field.sqe_next = NULL;					\
+	*(head)->sqh_last = (elm);					\
+	(head)->sqh_last = &(elm)->field.sqe_next;			\
+} while (/*CONSTCOND*/0)
+
+#define	SIMPLEQ_INSERT_AFTER(head, listelm, elm, field) do {		\
+	if (((elm)->field.sqe_next = (listelm)->field.sqe_next) == NULL)\
+		(head)->sqh_last = &(elm)->field.sqe_next;		\
+	(listelm)->field.sqe_next = (elm);				\
+} while (/*CONSTCOND*/0)
+
+#define	SIMPLEQ_REMOVE_HEAD(head, field) do {				\
+	if (((head)->sqh_first = (head)->sqh_first->field.sqe_next) == NULL) \
+		(head)->sqh_last = &(head)->sqh_first;			\
+} while (/*CONSTCOND*/0)
+
+#define SIMPLEQ_REMOVE_AFTER(head, elm, field) do {			\
+	if (((elm)->field.sqe_next = (elm)->field.sqe_next->field.sqe_next) \
+	    == NULL)							\
+		(head)->sqh_last = &(elm)->field.sqe_next;		\
+} while (/*CONSTCOND*/0)
+
+#define	SIMPLEQ_REMOVE(head, elm, type, field) do {			\
+	if ((head)->sqh_first == (elm)) {				\
+		SIMPLEQ_REMOVE_HEAD((head), field);			\
+	} else {							\
+		struct type *curelm = (head)->sqh_first;		\
+		while (curelm->field.sqe_next != (elm))			\
+			curelm = curelm->field.sqe_next;		\
+		if ((curelm->field.sqe_next =				\
+			curelm->field.sqe_next->field.sqe_next) == NULL) \
+			    (head)->sqh_last = &(curelm)->field.sqe_next; \
+	}								\
+} while (/*CONSTCOND*/0)
+
+#define	SIMPLEQ_CONCAT(head1, head2) do {				\
+	if (!SIMPLEQ_EMPTY((head2))) {					\
+		*(head1)->sqh_last = (head2)->sqh_first;		\
+		(head1)->sqh_last = (head2)->sqh_last;		\
+		SIMPLEQ_INIT((head2));					\
+	}								\
+} while (/*CONSTCOND*/0)
+
+#define	SIMPLEQ_LAST(head, type, field)					\
+	(SIMPLEQ_EMPTY((head)) ?						\
+		NULL :							\
+	        ((struct type *)(void *)				\
+		((char *)((head)->sqh_last) - offsetof(struct type, field))))
+
+/*
+ * Tail queue definitions.
+ */
+#define	_TAILQ_HEAD(name, type, qual)					\
+struct name {								\
+	qual type *tqh_first;		/* first element */		\
+	qual type *qual *tqh_last;	/* addr of last next element */	\
+}
+#define TAILQ_HEAD(name, type)	_TAILQ_HEAD(name, struct type,)
+
+#define	TAILQ_HEAD_INITIALIZER(head)					\
+	{ TAILQ_END(head), &(head).tqh_first }
+
+#define	_TAILQ_ENTRY(type, qual)					\
+struct {								\
+	qual type *tqe_next;		/* next element */		\
+	qual type *qual *tqe_prev;	/* address of previous next element */\
+}
+#define TAILQ_ENTRY(type)	_TAILQ_ENTRY(struct type,)
+
+/*
+ * Tail queue access methods.
+ */
+#define	TAILQ_FIRST(head)		((head)->tqh_first)
+#define	TAILQ_END(head)			(NULL)
+#define	TAILQ_NEXT(elm, field)		((elm)->field.tqe_next)
+#define	TAILQ_LAST(head, headname) \
+	(*(((struct headname *)(void *)((head)->tqh_last))->tqh_last))
+#define	TAILQ_PREV(elm, headname, field) \
+	(*(((struct headname *)(void *)((elm)->field.tqe_prev))->tqh_last))
+#define	TAILQ_EMPTY(head)		(TAILQ_FIRST(head) == TAILQ_END(head))
+
+
+#define	TAILQ_FOREACH(var, head, field)					\
+	for ((var) = ((head)->tqh_first);				\
+	    (var) != TAILQ_END(head);					\
+	    (var) = ((var)->field.tqe_next))
+
+#define	TAILQ_FOREACH_SAFE(var, head, field, next)			\
+	for ((var) = ((head)->tqh_first);				\
+	    (var) != TAILQ_END(head) &&					\
+	    ((next) = TAILQ_NEXT(var, field), 1); (var) = (next))
+
+#define	TAILQ_FOREACH_REVERSE(var, head, headname, field)		\
+	for ((var) = TAILQ_LAST((head), headname);			\
+	    (var) != TAILQ_END(head);					\
+	    (var) = TAILQ_PREV((var), headname, field))
+
+#define	TAILQ_FOREACH_REVERSE_SAFE(var, head, headname, field, prev)	\
+	for ((var) = TAILQ_LAST((head), headname);			\
+	    (var) != TAILQ_END(head) && 				\
+	    ((prev) = TAILQ_PREV((var), headname, field), 1); (var) = (prev))
+
+/*
+ * Tail queue functions.
+ */
+#if defined(QUEUEDEBUG)
+#define	QUEUEDEBUG_TAILQ_INSERT_HEAD(head, elm, field)			\
+	if ((head)->tqh_first &&					\
+	    (head)->tqh_first->field.tqe_prev != &(head)->tqh_first)	\
+		QUEUEDEBUG_ABORT("TAILQ_INSERT_HEAD %p %s:%d", (head),	\
+		    __FILE__, __LINE__);
+#define	QUEUEDEBUG_TAILQ_INSERT_TAIL(head, elm, field)			\
+	if (*(head)->tqh_last != NULL)					\
+		QUEUEDEBUG_ABORT("TAILQ_INSERT_TAIL %p %s:%d", (head),	\
+		    __FILE__, __LINE__);
+#define	QUEUEDEBUG_TAILQ_OP(elm, field)					\
+	if ((elm)->field.tqe_next &&					\
+	    (elm)->field.tqe_next->field.tqe_prev !=			\
+	    &(elm)->field.tqe_next)					\
+		QUEUEDEBUG_ABORT("TAILQ_* forw %p %s:%d", (elm),	\
+		    __FILE__, __LINE__);				\
+	if (*(elm)->field.tqe_prev != (elm))				\
+		QUEUEDEBUG_ABORT("TAILQ_* back %p %s:%d", (elm),	\
+		    __FILE__, __LINE__);
+#define	QUEUEDEBUG_TAILQ_PREREMOVE(head, elm, field)			\
+	if ((elm)->field.tqe_next == NULL &&				\
+	    (head)->tqh_last != &(elm)->field.tqe_next)			\
+		QUEUEDEBUG_ABORT("TAILQ_PREREMOVE head %p elm %p %s:%d",\
+		    (head), (elm), __FILE__, __LINE__);
+#define	QUEUEDEBUG_TAILQ_POSTREMOVE(elm, field)				\
+	(elm)->field.tqe_next = (void *)1L;				\
+	(elm)->field.tqe_prev = (void *)1L;
+#else
+#define	QUEUEDEBUG_TAILQ_INSERT_HEAD(head, elm, field)
+#define	QUEUEDEBUG_TAILQ_INSERT_TAIL(head, elm, field)
+#define	QUEUEDEBUG_TAILQ_OP(elm, field)
+#define	QUEUEDEBUG_TAILQ_PREREMOVE(head, elm, field)
+#define	QUEUEDEBUG_TAILQ_POSTREMOVE(elm, field)
+#endif
+
+#define	TAILQ_INIT(head) do {						\
+	(head)->tqh_first = TAILQ_END(head);				\
+	(head)->tqh_last = &(head)->tqh_first;				\
+} while (/*CONSTCOND*/0)
+
+#define	TAILQ_INSERT_HEAD(head, elm, field) do {			\
+	QUEUEDEBUG_TAILQ_INSERT_HEAD((head), (elm), field)		\
+	if (((elm)->field.tqe_next = (head)->tqh_first) != TAILQ_END(head))\
+		(head)->tqh_first->field.tqe_prev =			\
+		    &(elm)->field.tqe_next;				\
+	else								\
+		(head)->tqh_last = &(elm)->field.tqe_next;		\
+	(head)->tqh_first = (elm);					\
+	(elm)->field.tqe_prev = &(head)->tqh_first;			\
+} while (/*CONSTCOND*/0)
+
+#define	TAILQ_INSERT_TAIL(head, elm, field) do {			\
+	QUEUEDEBUG_TAILQ_INSERT_TAIL((head), (elm), field)		\
+	(elm)->field.tqe_next = TAILQ_END(head);			\
+	(elm)->field.tqe_prev = (head)->tqh_last;			\
+	*(head)->tqh_last = (elm);					\
+	(head)->tqh_last = &(elm)->field.tqe_next;			\
+} while (/*CONSTCOND*/0)
+
+#define	TAILQ_INSERT_AFTER(head, listelm, elm, field) do {		\
+	QUEUEDEBUG_TAILQ_OP((listelm), field)				\
+	if (((elm)->field.tqe_next = (listelm)->field.tqe_next) != 	\
+	    TAILQ_END(head))						\
+		(elm)->field.tqe_next->field.tqe_prev = 		\
+		    &(elm)->field.tqe_next;				\
+	else								\
+		(head)->tqh_last = &(elm)->field.tqe_next;		\
+	(listelm)->field.tqe_next = (elm);				\
+	(elm)->field.tqe_prev = &(listelm)->field.tqe_next;		\
+} while (/*CONSTCOND*/0)
+
+#define	TAILQ_INSERT_BEFORE(listelm, elm, field) do {			\
+	QUEUEDEBUG_TAILQ_OP((listelm), field)				\
+	(elm)->field.tqe_prev = (listelm)->field.tqe_prev;		\
+	(elm)->field.tqe_next = (listelm);				\
+	*(listelm)->field.tqe_prev = (elm);				\
+	(listelm)->field.tqe_prev = &(elm)->field.tqe_next;		\
+} while (/*CONSTCOND*/0)
+
+#define	TAILQ_REMOVE(head, elm, field) do {				\
+	QUEUEDEBUG_TAILQ_PREREMOVE((head), (elm), field)		\
+	QUEUEDEBUG_TAILQ_OP((elm), field)				\
+	if (((elm)->field.tqe_next) != TAILQ_END(head))			\
+		(elm)->field.tqe_next->field.tqe_prev = 		\
+		    (elm)->field.tqe_prev;				\
+	else								\
+		(head)->tqh_last = (elm)->field.tqe_prev;		\
+	*(elm)->field.tqe_prev = (elm)->field.tqe_next;			\
+	QUEUEDEBUG_TAILQ_POSTREMOVE((elm), field);			\
+} while (/*CONSTCOND*/0)
+
+#define TAILQ_REPLACE(head, elm, elm2, field) do {			\
+        if (((elm2)->field.tqe_next = (elm)->field.tqe_next) != 	\
+	    TAILQ_END(head))   						\
+                (elm2)->field.tqe_next->field.tqe_prev =		\
+                    &(elm2)->field.tqe_next;				\
+        else								\
+                (head)->tqh_last = &(elm2)->field.tqe_next;		\
+        (elm2)->field.tqe_prev = (elm)->field.tqe_prev;			\
+        *(elm2)->field.tqe_prev = (elm2);				\
+	QUEUEDEBUG_TAILQ_POSTREMOVE((elm), field);			\
+} while (/*CONSTCOND*/0)
+
+#define	TAILQ_CONCAT(head1, head2, field) do {				\
+	if (!TAILQ_EMPTY(head2)) {					\
+		*(head1)->tqh_last = (head2)->tqh_first;		\
+		(head2)->tqh_first->field.tqe_prev = (head1)->tqh_last;	\
+		(head1)->tqh_last = (head2)->tqh_last;			\
+		TAILQ_INIT((head2));					\
+	}								\
+} while (/*CONSTCOND*/0)
+
+/*
+ * Singly-linked Tail queue declarations.
+ */
+#define	STAILQ_HEAD(name, type)						\
+struct name {								\
+	struct type *stqh_first;	/* first element */		\
+	struct type **stqh_last;	/* addr of last next element */	\
+}
+
+#define	STAILQ_HEAD_INITIALIZER(head)					\
+	{ NULL, &(head).stqh_first }
+
+#define	STAILQ_ENTRY(type)						\
+struct {								\
+	struct type *stqe_next;	/* next element */			\
+}
+
+/*
+ * Singly-linked Tail queue access methods.
+ */
+#define	STAILQ_FIRST(head)	((head)->stqh_first)
+#define	STAILQ_END(head)	NULL
+#define	STAILQ_NEXT(elm, field)	((elm)->field.stqe_next)
+#define	STAILQ_EMPTY(head)	(STAILQ_FIRST(head) == STAILQ_END(head))
+
+/*
+ * Singly-linked Tail queue functions.
+ */
+#define	STAILQ_INIT(head) do {						\
+	(head)->stqh_first = NULL;					\
+	(head)->stqh_last = &(head)->stqh_first;				\
+} while (/*CONSTCOND*/0)
+
+#define	STAILQ_INSERT_HEAD(head, elm, field) do {			\
+	if (((elm)->field.stqe_next = (head)->stqh_first) == NULL)	\
+		(head)->stqh_last = &(elm)->field.stqe_next;		\
+	(head)->stqh_first = (elm);					\
+} while (/*CONSTCOND*/0)
+
+#define	STAILQ_INSERT_TAIL(head, elm, field) do {			\
+	(elm)->field.stqe_next = NULL;					\
+	*(head)->stqh_last = (elm);					\
+	(head)->stqh_last = &(elm)->field.stqe_next;			\
+} while (/*CONSTCOND*/0)
+
+#define	STAILQ_INSERT_AFTER(head, listelm, elm, field) do {		\
+	if (((elm)->field.stqe_next = (listelm)->field.stqe_next) == NULL)\
+		(head)->stqh_last = &(elm)->field.stqe_next;		\
+	(listelm)->field.stqe_next = (elm);				\
+} while (/*CONSTCOND*/0)
+
+#define	STAILQ_REMOVE_HEAD(head, field) do {				\
+	if (((head)->stqh_first = (head)->stqh_first->field.stqe_next) == NULL) \
+		(head)->stqh_last = &(head)->stqh_first;			\
+} while (/*CONSTCOND*/0)
+
+#define	STAILQ_REMOVE(head, elm, type, field) do {			\
+	if ((head)->stqh_first == (elm)) {				\
+		STAILQ_REMOVE_HEAD((head), field);			\
+	} else {							\
+		struct type *curelm = (head)->stqh_first;		\
+		while (curelm->field.stqe_next != (elm))			\
+			curelm = curelm->field.stqe_next;		\
+		if ((curelm->field.stqe_next =				\
+			curelm->field.stqe_next->field.stqe_next) == NULL) \
+			    (head)->stqh_last = &(curelm)->field.stqe_next; \
+	}								\
+} while (/*CONSTCOND*/0)
+
+#define	STAILQ_FOREACH(var, head, field)				\
+	for ((var) = ((head)->stqh_first);				\
+		(var);							\
+		(var) = ((var)->field.stqe_next))
+
+#define	STAILQ_FOREACH_SAFE(var, head, field, tvar)			\
+	for ((var) = STAILQ_FIRST((head));				\
+	    (var) && ((tvar) = STAILQ_NEXT((var), field), 1);		\
+	    (var) = (tvar))
+
+#define	STAILQ_CONCAT(head1, head2) do {				\
+	if (!STAILQ_EMPTY((head2))) {					\
+		*(head1)->stqh_last = (head2)->stqh_first;		\
+		(head1)->stqh_last = (head2)->stqh_last;		\
+		STAILQ_INIT((head2));					\
+	}								\
+} while (/*CONSTCOND*/0)
+
+#define	STAILQ_LAST(head, type, field)					\
+	(STAILQ_EMPTY((head)) ?						\
+		NULL :							\
+	        ((struct type *)(void *)				\
+		((char *)((head)->stqh_last) - offsetof(struct type, field))))
+
+#endif	/* !_SYS_QUEUE_H_ */



Home | Main Index | Thread Index | Old Index