PERFORCE change 222990 for review
Jonathan Anderson
jonathan at FreeBSD.org
Sun Mar 17 23:41:30 UTC 2013
http://p4web.freebsd.org/@@222990?ac=10
Change 222990 by jonathan at jonathan-on-joe on 2013/03/17 23:41:17
Pull latest libtesla code from GitHub (commit d829c559).
Submitted by: Robert Watson <rwatson at FreeBSD.org>
Reviewed by: Jonathan Anderson <jonathan at FreeBSD.org>
Affected files ...
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/debug.c#3 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/key.c#2 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/libtesla.h#3 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/state-perthread.c#3 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/state.c#3 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/store.c#3 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_internal.h#3 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/update.c#4 edit
Differences ...
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/debug.c#3 (text+ko) ====
@@ -32,7 +32,10 @@
*/
#include "tesla_internal.h"
+
+#ifndef _KERNEL
#include <stdlib.h>
+#endif
#define SAFE_SPRINTF(dest, end, ...) \
dest += snprintf(dest, end - dest, __VA_ARGS__); \
@@ -42,9 +45,9 @@
char*
transition_matrix(const struct tesla_transitions *trans)
{
- static const char EACH[] = "(%d:0x%tx -> %d%s) ";
+ static const char EACH[] = "(%d:0x%tx -> %d%s%s%s) ";
- size_t needed = trans->length * (sizeof(EACH) + 4) + 4;
+ size_t needed = trans->length * (sizeof(EACH) + 12) + 4;
char *buffer = tesla_malloc(needed);
char *c = buffer;
@@ -53,7 +56,10 @@
for (size_t i = 0; i < trans->length; i++) {
const tesla_transition *t = trans->transitions + i;
c += sprintf(c, EACH, t->from, t->mask, t->to,
- t->fork ? " <fork>" : "");
+ (t->flags & TESLA_TRANS_FORK ? " <fork>" : ""),
+ (t->flags & TESLA_TRANS_INIT ? " <init>" : ""),
+ (t->flags & TESLA_TRANS_CLEANUP ? " <clean>" : "")
+ );
}
c += sprintf(c, "]");
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/key.c#2 (text+ko) ====
@@ -32,8 +32,10 @@
#include "tesla_internal.h"
+#ifndef _KERNEL
#include <inttypes.h>
#include <stdio.h>
+#endif
#define IS_SET(mask, index) (mask & (1 << index))
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/libtesla.h#3 (text+ko) ====
@@ -34,7 +34,11 @@
#ifndef _TESLA_STATE
#define _TESLA_STATE
+#ifdef _KERNEL
+#include <sys/types.h>
+#else
#include <stdint.h> /* int32_t, uint32_t */
+#endif
/*
* libtesla functions mostly return error values, and therefore return
@@ -61,15 +65,15 @@
/** The state we are moving to. */
uint32_t to;
- /**
- * Explicit declaration that libtesla should fork on this transition.
- *
- * This is useful for e.g. TELSA "or" expressions, when we need to
- * allow either or both paths to be followed.
- */
- int fork;
+ /** Things we may need to do on this transition. */
+ int flags;
};
+#define TESLA_TRANS_FORK 0x01 /* Always fork on this transition. */
+#define TESLA_TRANS_INIT 0x02 /* May need to initialise the class. */
+#define TESLA_TRANS_CLEANUP 0x04 /* Clean up the class now. */
+
+
/**
* A set of permissible state transitions for an automata instance.
*
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/state-perthread.c#3 (text+ko) ====
@@ -1,5 +1,5 @@
/*-
- * Copyright (c) 2011 Robert N. M. Watson
+ * Copyright (c) 2011, 2013 Robert N. M. Watson
* Copyright (c) 2012-2013 Jonathan Anderson
* All rights reserved.
*
@@ -49,259 +49,50 @@
#ifdef _KERNEL
/*
- * Global state used to manage per-thread storage slots for TESLA per-thread
- * assertions. tspd_tesla_classp is non-NULL when a slot has been allocated.
- */
-static struct tesla_class_perthread_desc {
- struct tesla_class *tspd_tesla_classp;
- size_t tspd_len;
-} tesla_class_perthread_desc[TESLA_PERTHREAD_MAX];
-static struct sx tesla_class_perthread_sx;
-
-/*
* Registration state for per-thread storage.
*/
-static eventhandler_tag tesla_class_perthread_ctor_tag;
-static eventhandler_tag tesla_class_perthread_dtor_tag;
+static eventhandler_tag tesla_perthread_ctor_tag;
+static eventhandler_tag tesla_perthread_dtor_tag;
static void
-tesla_class_perthread_ctor(__unused void *arg, struct thread *td)
+tesla_perthread_ctor(__unused void *arg, struct thread *td)
{
- struct tesla_class_perthread_desc *tspdp;
- struct tesla_class *tsp;
- struct tesla_table *ttp;
- u_int index;
+ struct tesla_store *store;
+ uint32_t error;
- sx_slock(&tesla_class_perthread_sx);
- for (index = 0; index < TESLA_PERTHREAD_MAX; index++) {
- tspdp = &tesla_class_perthread_desc[index];
- tsp = tspdp->tspd_tesla_classp;
- if (tsp == NULL) {
- td->td_tesla[index] = NULL;
- continue;
- }
- ttp = malloc(tspdp->tspd_len, M_TESLA, M_WAITOK | M_ZERO);
- ttp->tt_length = tsp->ts_limit;
- ttp->tt_free = tsp->ts_limit;
- td->td_tesla[index] = ttp;
- }
- sx_sunlock(&tesla_class_perthread_sx);
+ store = tesla_malloc(sizeof(*store));
+ error = tesla_store_init(store, TESLA_SCOPE_PERTHREAD,
+ TESLA_MAX_CLASSES, TESLA_MAX_INSTANCES);
+ tesla_assert(error == TESLA_SUCCESS, ("tesla_store_init failed"));
+ td->td_tesla = store;
}
static void
-tesla_class_perthread_dtor_locked(struct thread *td)
+tesla_perthread_dtor(struct thread *td)
{
- u_int index;
+ struct tesla_store *store;
- sx_assert(&tesla_class_perthread_sx, SX_LOCKED);
- for (index = 0; index < TESLA_PERTHREAD_MAX; index++) {
- if (td->td_tesla[index] == NULL)
- continue;
- free(M_TESLA, td->td_tesla[index]);
- td->td_tesla[index] = NULL;
- }
+ store = td->td_tesla;
+ td->td_tesla = NULL;
+ tesla_store_free(store);
+ tesla_free(store);
}
static void
-tesla_class_perthread_dtor(__unused void *arg, struct thread *td)
+tesla_perthread_sysinit(__unused void *arg)
{
- sx_slock(&tesla_class_perthread_sx);
- tesla_class_perthread_dtor_locked(td);
- sx_sunlock(&tesla_class_perthread_sx);
+ tesla_perthread_ctor_tag = EVENTHANDLER_REGISTER(thread_ctor,
+ tesla_perthread_ctor, NULL, EVENTHANDLER_PRI_ANY);
+ tesla_perthread_dtor_tag = EVENTHANDLER_REGISTER(thread_dtor,
+ tesla_perthread_dtor, NULL, EVENTHANDLER_PRI_ANY);
}
+SYSINIT(tesla_perthread, SI_SUB_TESLA, SI_ORDER_FIRST,
+ tesla_perthread_sysinit, NULL);
-static void
-tesla_class_perthread_sysinit(__unused void *arg)
-{
+#endif /* !_KERNEL */
- sx_init(&tesla_class_perthread_sx, "tesla_class_perthread_sx");
- tesla_class_perthread_ctor_tag = EVENTHANDLER_REGISTER(thread_ctor,
- tesla_class_perthread_ctor, NULL, EVENTHANDLER_PRI_ANY);
- tesla_class_perthread_dtor_tag = EVENTHANDLER_REGISTER(thread_dtor,
- tesla_class_perthread_dtor, NULL, EVENTHANDLER_PRI_ANY);
-}
-SYSINIT(tesla_class_perthread, SI_SUB_TESLA, SI_ORDER_FIRST,
- tesla_class_perthread_sysinit, NULL);
-
-static void
-tesla_class_perthread_sysuninit(__unused void *arg)
-{
- struct proc *p;
- struct thread *td;
-
- /*
- * XXXRW: Possibility of a race for in-flight handlers and
- * instrumentation?
- */
- EVENTHANDLER_DEREGISTER(tesla_class_perthread_ctor,
- tesla_class_perthread_ctor_tag);
- EVENTHANDLER_DEREGISTER(tesla_class_perthread_dtor,
- tesla_class_perthread_dtor_tag);
-
- sx_xlock(&allproc_lock);
- sx_xlock(&tesla_class_perthread_sx);
- FOREACH_PROC_IN_SYSTEM(p) {
- PROC_LOCK(p);
- FOREACH_THREAD_IN_PROC(p, td) {
- tesla_class_perthread_dtor_locked(td);
- }
- PROC_UNLOCK(p);
- }
- sx_xunlock(&tesla_class_perthread_sx);
- sx_xunlock(&allproc_lock);
- sx_destroy(&tesla_class_perthread_sx);
-}
-SYSUNINIT(tesla_class_perthread, SI_SUB_TESLA, SI_ORDER_FIRST,
- tesla_class_perthread_sysuninit, NULL);
-
int
-tesla_class_perthread_new(struct tesla_class *tsp)
-{
- struct tesla_class_perthread_desc *tspdp;
- struct tesla_table *ttp;
- struct proc *p;
- struct thread *td;
- int looped;
- u_int index;
-
- /*
- * First, allocate a TESLA per-thread storage slot, if available.
- */
- tspdp = NULL;
- sx_xlock(&tesla_class_perthread_sx);
- for (index = 0; index < TESLA_PERTHREAD_MAX; index++) {
- if (tesla_class_perthread_desc[index].tspd_tesla_classp
- == NULL) {
- tspdp = &tesla_class_perthread_desc[index];
- break;
- }
- }
- if (tspdp == NULL) {
- sx_xunlock(&tesla_class_perthread_sx);
- return (TESLA_ERROR_ENOMEM);
- }
- tsp->ts_perthread_index = index;
- tspdp->tspd_tesla_classp = tsp;
- tspdp->tspd_len = sizeof(*ttp) + sizeof(struct tesla_instance) *
- tsp->ts_limit;
-
- /*
- * Walk all existing threads and add required allocations. If we
- * can't allocate under the process lock, we have to loop out, use
- * M_WAITOK, and then repeat. This looks starvation-prone, but
- * actually isn't: holding tesla_class_perthread_sx blocks further
- * thread allocations from taking place, so the main concern is
- * in-progress allocations, which will be bounded in number.
- */
- ttp = NULL;
- looped = 0;
- sx_slock(&allproc_lock);
- FOREACH_PROC_IN_SYSTEM(p) {
-loop:
- if (looped) {
- KASSERT(ttp == NULL,
- ("tesla_class_perthread_new: ttp not NULL"));
- ttp = malloc(tspdp->tspd_len, M_TESLA,
- M_WAITOK | M_ZERO);
- looped = 0;
- }
- PROC_LOCK(p);
- FOREACH_THREAD_IN_PROC(p, td) {
- /*
- * If we looped, then some threads may already have
- * memory; skip them.
- */
- if (td->td_tesla[index] != NULL)
- continue;
- if (ttp == NULL)
- ttp = malloc(tspdp->tspd_len, M_TESLA,
- M_NOWAIT | M_ZERO);
- if (ttp == NULL) {
- PROC_UNLOCK(p);
- looped = 1;
- goto loop;
- }
- ttp->tt_length = tsp->ts_limit;
- ttp->tt_free = tsp->ts_limit;
- td->td_tesla[index] = ttp;
- ttp = NULL;
- }
- PROC_UNLOCK(p);
- }
- sx_sunlock(&allproc_lock);
- /* Due to races, we may have allocated an extra, so free it now. */
- if (ttp != NULL)
- free(ttp, M_TESLA);
- sx_xunlock(&tesla_class_perthread_sx);
- return (TESLA_SUCCESS);
-}
-
-void
-tesla_class_perthread_destroy(struct tesla_class *tsp)
-{
- struct tesla_class_perthread_desc *tspdp;
- struct proc *p;
- struct thread *td;
- u_int index;
-
- sx_xlock(&tesla_class_perthread_sx);
- index = tsp->ts_perthread_index;
- tspdp = &tesla_class_perthread_desc[index];
-
- /*
- * First, walk all threads and release resources. This is easier on
- * free than alloc due to the non-blocking nature of free.
- *
- * XXXRW: Do we need a test for td->td_tesla[index] == NULL and a
- * continue? I think probably not.
- */
- sx_slock(&allproc_lock);
- FOREACH_PROC_IN_SYSTEM(p) {
- PROC_LOCK(p);
- FOREACH_THREAD_IN_PROC(p, td) {
- free(M_TESLA, td->td_tesla[index]);
- td->td_tesla[index] = NULL;
- }
- PROC_UNLOCK(p);
- }
- sx_unlock(&allproc_lock);
-
- /*
- * Finally, release the reservation.
- */
- tspdp->tspd_tesla_classp = NULL;
- tspdp->tspd_len = 0;
- sx_xunlock(&tesla_class_perthread_sx);
-}
-
-void
-tesla_class_perthread_flush(struct tesla_class *tsp)
-{
- struct tesla_table *ttp;
-
- ttp = curthread->td_tesla[tsp->ts_perthread_index];
- bzero(&ttp->tt_instances,
- sizeof(struct tesla_instance) * ttp->tt_length);
- ttp->tt_free = ttp->tt_length;
-}
-
-int
-tesla_class_perthread_gettable(struct tesla_class *tsp,
- struct tesla_table **ttpp)
-{
- struct tesla_table *ttp;
-
- ttp = curthread->td_tesla[tsp->ts_perthread_index];
- KASSERT(ttp != NULL,
- ("tesla_class_perthread_gettable: NULL tesla thread state"));
- *ttpp = ttp;
- return (TESLA_SUCCESS);
-}
-
-#else /* !_KERNEL */
-
-int
tesla_class_perthread_postinit(__unused struct tesla_class *c)
{
return 0;
@@ -321,5 +112,3 @@
tesla_class_perthread_destroy(__unused struct tesla_class *c)
{
}
-
-#endif /* _KERNEL */
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/state.c#3 (text+ko) ====
@@ -1,5 +1,5 @@
/*-
- * Copyright (c) 2011 Robert N. M. Watson
+ * Copyright (c) 2011, 2013 Robert N. M. Watson
* Copyright (c) 2011 Anil Madhavapeddy
* Copyright (c) 2012-2013 Jonathan Anderson
* All rights reserved.
@@ -34,11 +34,11 @@
#include "tesla_internal.h"
+#ifdef _KERNEL
+MALLOC_DEFINE(M_TESLA, "tesla", "TESLA internal state");
+#else
#include <inttypes.h>
#include <stdio.h>
-
-#ifdef _KERNEL
-MALLOC_DEFINE(M_TESLA, "tesla", "TESLA internal state");
#endif
@@ -84,8 +84,8 @@
void
tesla_class_free(struct tesla_class *class)
{
- free(class->ts_table);
- free(class);
+ tesla_free(class->ts_table);
+ tesla_free(class);
}
@@ -144,7 +144,7 @@
struct tesla_table *ttp = tclass->ts_table;
assert(ttp != NULL);
- tesla_assert(ttp->tt_length != 0, "Uninitialized tesla_table");
+ tesla_assert(ttp->tt_length != 0, ("Uninitialized tesla_table"));
if (ttp->tt_free == 0)
return (TESLA_ERROR_ENOMEM);
@@ -163,7 +163,7 @@
break;
}
- tesla_assert(*out != NULL, "no free instances but tt_free was > 0");
+ tesla_assert(*out != NULL, ("no free instances but tt_free was > 0"));
return (TESLA_SUCCESS);
}
@@ -194,6 +194,8 @@
tesla_class_reset(struct tesla_class *c)
{
+ DEBUG_PRINT("tesla_class_reset(%" PRId64 ")\n", (uint64_t) c);
+
struct tesla_table *t = c->ts_table;
bzero(&t->tt_instances, sizeof(struct tesla_instance) * t->tt_length);
t->tt_free = t->tt_length;
@@ -254,7 +256,7 @@
break;
}
- free(trans_str);
+ tesla_free(trans_str);
}
void
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/store.c#3 (text+ko) ====
@@ -1,7 +1,7 @@
/** @file tesla_store.c Implementation of @ref tesla_store. */
/*-
* Copyright (c) 2012 Jonathan Anderson
- * Copyright (c) 2011 Robert N. M. Watson
+ * Copyright (c) 2011, 2013 Robert N. M. Watson
* Copyright (c) 2011 Anil Madhavapeddy
* All rights reserved.
*
@@ -38,16 +38,27 @@
#ifndef _KERNEL
#include <errno.h>
-struct tesla_store global_store = { .length = 0 };
-
/** The pthreads key used to identify TESLA data. */
pthread_key_t pthread_key(void);
#endif
+struct tesla_store global_store = { .length = 0 };
+
static void tesla_class_acquire(tesla_class*);
-static int tesla_store_init(tesla_store*,
- uint32_t context, uint32_t classes, uint32_t instances);
+#ifdef _KERNEL
+static void
+tesla_global_store_sysinit(__unused void *arg)
+{
+ uint32_t error;
+
+ error = tesla_store_init(&global_store, TESLA_SCOPE_GLOBAL,
+ TESLA_MAX_CLASSES, TESLA_MAX_INSTANCES);
+ tesla_assert(error == TESLA_SUCCESS, ("tesla_store_init failed"));
+}
+SYSINIT(tesla_global_store, SI_SUB_TESLA, SI_ORDER_FIRST,
+ tesla_global_store_sysinit, NULL);
+#endif
int32_t
tesla_store_get(uint32_t context, uint32_t classes, uint32_t instances,
@@ -101,7 +112,7 @@
}
-static int32_t
+int32_t
tesla_store_init(tesla_store *store, uint32_t context,
uint32_t classes, uint32_t instances)
{
@@ -132,7 +143,7 @@
for (uint32_t i = 0; i < store->length; i++)
tesla_class_free(store->classes + i);
- free(store);
+ tesla_free(store);
}
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_internal.h#3 (text+ko) ====
@@ -1,5 +1,5 @@
/*-
- * Copyright (c) 2011 Robert N. M. Watson
+ * Copyright (c) 2011, 2013 Robert N. M. Watson
* All rights reserved.
*
* This software was developed by SRI International and the University of
@@ -36,21 +36,26 @@
#ifdef _KERNEL
#include "opt_kdb.h"
#include <sys/param.h>
+#include <sys/eventhandler.h>
#include <sys/kdb.h>
#include <sys/kernel.h>
#include <sys/lock.h>
#include <sys/mutex.h>
#include <sys/malloc.h>
+#include <sys/proc.h>
+#include <sys/sx.h>
#include <sys/systm.h>
+
+#include <libtesla/libtesla.h>
#else
#include <assert.h>
#include <err.h>
#include <pthread.h>
#include <stdlib.h>
#include <string.h>
-#endif
#include <libtesla.h>
+#endif
//! Is @ref x a subset of @ref y?
#define SUBSET(x,y) ((x & y) == x)
@@ -103,8 +108,13 @@
#define __debug
+#ifdef _KERNEL
+#include <sys/systm.h>
+#define DEBUG_PRINT(...) printf(__VA_ARGS__)
+#else
#include <stdio.h>
#define DEBUG_PRINT(...) printf(__VA_ARGS__)
+#endif
#define VERBOSE_PRINT(...) if (verbose_debug()) DEBUG_PRINT(__VA_ARGS__)
/** Are we in (verbose) debug mode? */
@@ -139,7 +149,7 @@
#define tesla_assert(...) KASSERT(__VA_ARGS__)
/** Emulate simple POSIX assertions. */
-#define assert(cond) KASSERT(cond, "Assertion failed: '" # cond "'")
+#define assert(cond) KASSERT((cond), ("Assertion failed: '%s'", #cond))
#define tesla_malloc(len) malloc(len, M_TESLA, M_WAITOK | M_ZERO)
#define tesla_free(x) free(x, M_TESLA)
@@ -223,6 +233,13 @@
};
/**
+ * Initialise @ref tesla_store internals.
+ * Locking is the responsibility of the caller.
+ */
+int tesla_store_init(tesla_store*, uint32_t context, uint32_t classes,
+ uint32_t instances);
+
+/**
* Initialize @ref tesla_class internals.
* Locking is the responsibility of the caller.
*/
@@ -234,6 +251,13 @@
const struct tesla_transitions*);
/*
+ * XXXRW: temporarily, maximum number of classes and instances are hard-coded
+ * constants. In the future, this should somehow be more dynamic.
+ */
+#define TESLA_MAX_CLASSES 12
+#define TESLA_MAX_INSTANCES 8
+
+/*
* When the assertion fails, what to do?
*/
#define TESLA_ACTION_FAILSTOP 1 /* Stop on failure. */
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/update.c#4 (text+ko) ====
@@ -32,8 +32,10 @@
#include "tesla_internal.h"
+#ifndef _KERNEL
#include <stdbool.h>
#include <inttypes.h>
+#endif
#define CHECK(fn, ...) do { \
int err = fn(__VA_ARGS__); \
@@ -67,7 +69,8 @@
}
struct tesla_store *store;
- CHECK(tesla_store_get, tesla_context, 12, 8, &store);
+ CHECK(tesla_store_get, tesla_context, TESLA_MAX_CLASSES,
+ TESLA_MAX_INSTANCES, &store);
VERBOSE_PRINT("store: 0x%tx", (intptr_t) store);
VERBOSE_PRINT("\n----\n");
@@ -116,6 +119,9 @@
if (!tesla_key_matches(&masked, k))
continue;
+ if (k->tk_mask != t->mask)
+ continue;
+
if (inst->ti_state != t->from) {
// If the instance matches everything but the
// state, so there had better be a transition
@@ -133,7 +139,8 @@
// If the keys just match (and we haven't been explictly
// instructed to fork), just update the state.
- if (!t->fork && key->tk_mask == k->tk_mask) {
+ if (!(t->flags & TESLA_TRANS_FORK)
+ && key->tk_mask == k->tk_mask) {
VERBOSE_PRINT("update %td: %tx->%tx\n",
inst - start, t->from, t->to);
@@ -168,19 +175,22 @@
}
- // If there is a (0 -> anything) transition, create a new instance.
+ // Is the transition "special" (e.g. init/cleanup)?
for (uint32_t i = 0; i < trans->length; i++) {
const tesla_transition *t = trans->transitions + i;
- if (t->from != 0)
- continue;
+ if (t->from == 0) {
+ struct tesla_instance *inst;
+ CHECK(tesla_instance_new, class, key, t->to, &inst);
+ assert(tesla_instance_active(inst));
- struct tesla_instance *inst;
- CHECK(tesla_instance_new, class, key, t->to, &inst);
- assert(tesla_instance_active(inst));
+ matched_something = true;
+ VERBOSE_PRINT("new %td: %tx\n",
+ inst - start, inst->ti_state);
+ }
- matched_something = true;
- VERBOSE_PRINT("new %td: %tx\n",
- inst - start, inst->ti_state);
+ if (t->flags & TESLA_TRANS_CLEANUP) {
+ tesla_class_reset(class);
+ }
}
if (verbose_debug()) {
More information about the p4-projects
mailing list