Date: Sun, 17 Mar 2013 23:41:30 GMT From: Jonathan Anderson <jonathan@FreeBSD.org> To: Perforce Change Reviews <perforce@FreeBSD.org> Subject: PERFORCE change 222990 for review Message-ID: <201303172341.r2HNfU4V014451@skunkworks.freebsd.org>
next in thread | raw e-mail | index | archive | help
http://p4web.freebsd.org/@@222990?ac=10 Change 222990 by jonathan@jonathan-on-joe on 2013/03/17 23:41:17 Pull latest libtesla code from GitHub (commit d829c559). Submitted by: Robert Watson <rwatson@FreeBSD.org> Reviewed by: Jonathan Anderson <jonathan@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()) {
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201303172341.r2HNfU4V014451>