Re: ARC model specified in spinroot/promela
- Reply: Mathew\, Cherry G.*: "Re: ARC model specified in spinroot/promela"
- In reply to: Mathew\, Cherry G.*: "Re: ARC model specified in spinroot/promela"
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Wed, 06 Sep 2023 11:58:49 UTC
>>>>> Mathew, Cherry G * <c@bow.st> 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.
Meanwhile, please feel free to comment on this approach at Design Driven
Development (D3) if you have any.
--
~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-06 11:18:57.502125698 +0000
@@ -0,0 +1,173 @@
+/* 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"
+
+void arc_list_init(struct arc_list *_arc_list)
+{
+ TAILQ_INIT(&_arc_list->qhead);
+ _arc_list->qcount = 0;
+
+ for(int 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-04 10:32:34.042373574 +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"
+
+#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 byte _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.h arc/arc.h
--- arc.null/arc.h 1970-01-01 00:00:00.000000000 +0000
+++ arc/arc.h 2023-09-06 11:27:01.777533992 +0000
@@ -0,0 +1,166 @@
+/*
+ * 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;
+ for (int 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);
+}
+
+inline static struct arc_item *
+findmember(struct arc_list *_arc_list, struct arc_item *aikey)
+{
+ assert(_arc_list != NULL && aikey != NULL);
+ 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 */);
+
+#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-05 19:11:38.075381290 +0000
@@ -0,0 +1,54 @@
+/* Spin process model for Adaptive Replacement Cache algorithm. Written by cherry */
+
+#ifndef _ARC_INC
+#define _ARC_INC
+
+/* XXX: Move these into a set of library includes ? */
+/* XXX: Equivalence verification */
+/* Note: CAS implemented in an atomic {} block */
+#define mutex_enter(_mutex) \
+ atomic { \
+ (_mutex == 0) -> _mutex = 1; \
+ }
+
+#define mutex_exit(_mutex) \
+ atomic { \
+ assert(_mutex == 1); \
+ (_mutex == 1) -> _mutex = 0; \
+ }
+
+bit sc_lock;
+
+#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) \
+ d_step { \
+ _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-04 10:15:53.767411900 +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"
+
+#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)))
+ ->
+ d_step {
+ readLRU(T1, LRUitem);
+ delLRU(T1);
+ cacheremove(LRUitem);
+ addMRU(B1, LRUitem);
+ }
+
+ ::
+ else
+ ->
+ d_step {
+ readLRU(T2, LRUitem);
+ delLRU(T2);
+ cacheremove(LRUitem);
+ addMRU(B2, LRUitem);
+ }
+ fi
+}
+
+inline ARC(/* arc_item */ x_t)
+{
+ if
+ :: /* Case I */
+ memberof(T1, x_t)
+ ->
+ d_step {
+ delitem(T1, x_t);
+ addMRU(T2, x_t);
+ }
+ :: /* Case I */
+ memberof(T2, x_t)
+ ->
+ d_step {
+ 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);
+ d_step {
+ 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);
+ d_step {
+ 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);
+ d_step {
+ 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/Makefile arc/Makefile
--- arc.null/Makefile 1970-01-01 00:00:00.000000000 +0000
+++ arc/Makefile 2023-09-06 11:37:35.438225102 +0000
@@ -0,0 +1,78 @@
+# This set of spinroot related files were written by cherry
+# <c@bow.st> 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 model > spinmodel.pml;cat arc.drv >> spinmodel.pml;cat arc.inv >> spinmodel.pml;
+ spin -am spinmodel.pml
+
+spin-build: spin-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 -o arc.o -c arc.c
+
+# Housekeeping
+prog-clean:
+ rm -f arc.o
+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: 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_ */