Date: Wed, 20 Mar 2013 18:57:05 GMT From: Robert Watson <rwatson@FreeBSD.org> To: Perforce Change Reviews <perforce@FreeBSD.org> Subject: PERFORCE change 223080 for review Message-ID: <201303201857.r2KIv5I0023497@skunkworks.freebsd.org>
index | next in thread | raw e-mail
http://p4web.freebsd.org/@@223080?ac=10 Change 223080 by rwatson@rwatson_cinnamon on 2013/03/20 18:56:54 Merge libtesla from github through 8e193990d1df2418cc3b579309ad85501156e295. Affected files ... .. //depot/projects/ctsrd/tesla/src/lib/libtesla/Makefile#3 edit .. //depot/projects/ctsrd/tesla/src/lib/libtesla/debug.c#4 edit .. //depot/projects/ctsrd/tesla/src/lib/libtesla/libtesla.h#4 edit .. //depot/projects/ctsrd/tesla/src/lib/libtesla/state.c#5 edit .. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_internal.h#5 edit .. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_notification.c#3 edit .. //depot/projects/ctsrd/tesla/src/lib/libtesla/update.c#6 edit Differences ... ==== //depot/projects/ctsrd/tesla/src/lib/libtesla/Makefile#3 (text+ko) ==== @@ -7,8 +7,8 @@ CFLAGS+= -I${.CURDIR} INCS= tesla.h libtesla.h -SRCS= debug.c key.c tesla_dtrace.c tesla_notification.c state.c state-global.c - state-perthread.c store.c update.c util.c +SRCS= debug.c key.c tesla_dtrace.c tesla_notification.c state.c \ + state-global.c state-perthread.c store.c update.c util.c .include <bsd.lib.mk> ==== //depot/projects/ctsrd/tesla/src/lib/libtesla/debug.c#4 (text+ko) ==== @@ -37,61 +37,73 @@ #include <stdlib.h> #endif -#define SAFE_SPRINTF(dest, end, ...) \ - dest += snprintf(dest, end - dest, __VA_ARGS__); \ - if (dest >= end) \ - return (TESLA_ERROR_ENOMEM); +void +print_transitions(const struct tesla_transitions *transp) +{ + char buffer[1024]; + char *end = buffer + sizeof(buffer); + + sprint_transitions(buffer, end, transp); + print("%s", buffer); +} char* -transition_matrix(const struct tesla_transitions *trans) +sprint_transitions(char *buffer, const char *end, + const struct tesla_transitions *tp) { - static const char EACH[] = "(%d:0x%tx -> %d%s%s%s) "; + char *c = buffer; + + SAFE_SPRINTF(c, end, "[ "); + + for (size_t i = 0; i < tp->length; i++) { + const tesla_transition *t = tp->transitions + i; + + /* Note: On at least one Mac, combining the following + * into a single snprintf() causes the wrong thing + * to be printed (instead of t->mask, we get an address!). + */ + SAFE_SPRINTF(c, end, "(%d:", t->from); + SAFE_SPRINTF(c, end, "0x%tx", t->mask); + SAFE_SPRINTF(c, end, " -> %d", t->to); + + if (t->flags & TESLA_TRANS_FORK) + SAFE_SPRINTF(c, end, " <fork>"); - size_t needed = trans->length * (sizeof(EACH) + 12) + 4; - char *buffer = tesla_malloc(needed); - char *c = buffer; + if (t->flags & TESLA_TRANS_INIT) + SAFE_SPRINTF(c, end, " <init>"); - c += sprintf(c, "[ "); + if (t->flags & TESLA_TRANS_CLEANUP) + SAFE_SPRINTF(c, end, " <clean>"); - 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->flags & TESLA_TRANS_FORK ? " <fork>" : ""), - (t->flags & TESLA_TRANS_INIT ? " <init>" : ""), - (t->flags & TESLA_TRANS_CLEANUP ? " <clean>" : "") - ); + SAFE_SPRINTF(c, end, ") "); } - c += sprintf(c, "]"); + SAFE_SPRINTF(c, end, "]"); - return buffer; + return c; } -int -key_string(char *buffer, size_t len, const struct tesla_key *key) +char* +key_string(char *buffer, const char *end, const struct tesla_key *key) { - char *current = buffer; - const char *end = buffer + len; + char *c = buffer; - SAFE_SPRINTF(current, end, "0x%tx [ ", key->tk_mask); + SAFE_SPRINTF(c, end, "0x%tx [ ", key->tk_mask); for (int32_t i = 0; i < TESLA_KEY_SIZE; i++) { - if (key->tk_mask & (1 << i)) { - SAFE_SPRINTF(current, end, "%tx ", key->tk_keys[i]); - } else { - SAFE_SPRINTF(current, end, "X "); - } + if (key->tk_mask & (1 << i)) + SAFE_SPRINTF(c, end, "%tx ", key->tk_keys[i]); + else + SAFE_SPRINTF(c, end, "X "); } - SAFE_SPRINTF(current, end, "]"); + SAFE_SPRINTF(c, end, "]"); - return (TESLA_SUCCESS); + return c; } #ifndef NDEBUG -#define print DEBUG_PRINT - /* TODO: kernel version... probably just say no? */ int32_t verbose_debug() @@ -167,11 +179,12 @@ { static const size_t LEN = 15 * TESLA_KEY_SIZE + 10; char buffer[LEN]; + char *end = buffer + LEN; - int err = key_string(buffer, LEN, key); - assert(err == TESLA_SUCCESS); + char *e = key_string(buffer, end, key); + assert(e < end); - printf("%s", buffer); + print("%s", buffer); } #endif /* !NDEBUG */ ==== //depot/projects/ctsrd/tesla/src/lib/libtesla/libtesla.h#4 (text+ko) ==== @@ -205,14 +205,6 @@ #define TESLA_SCOPE_PERTHREAD 1 #define TESLA_SCOPE_GLOBAL 2 -/** - * Set the action to take when a TESLA assertion fails; implemented via a - * callback from the TESLA runtime. - */ -typedef void (*tesla_assert_fail_callback)(const struct tesla_instance *tip); -void tesla_class_setaction(struct tesla_class *tsp, - tesla_assert_fail_callback handler); - /** * Checks whether or not a TESLA automata instance is active (in use). @@ -242,15 +234,4 @@ void tesla_instance_destroy(struct tesla_class *tsp, struct tesla_instance *tip); -/** - * Function to invoke when a TESLA assertion fails. - * - * May not actually fail stop at this point, so assertions must handle - * continuation after this call. Further cases of this particular instance - * firing should be suppressed so that e.g. DTrace probes fire only once - * per failure. - */ -void tesla_assert_fail(struct tesla_class *tsp, - struct tesla_instance *tip, const struct tesla_transitions*); - #endif /* _TESLA_STATE */ ==== //depot/projects/ctsrd/tesla/src/lib/libtesla/state.c#5 (text+ko) ==== @@ -211,92 +211,3 @@ assert(0 && "unhandled TESLA context"); } } - -void -tesla_match_fail(struct tesla_class *class, const struct tesla_key *key, - const struct tesla_transitions *trans) -{ - assert(class !=NULL); - - if (class->ts_handler != NULL) { - class->ts_handler(NULL); - return; - } - - static const char *message = - "TESLA failure in automaton '%s':\n%s\n\n" - "no instance found to match key '%s' for transition(s) %s"; - - // Assume a pretty big key... - static const size_t LEN = 160; - char key_str[LEN]; - int err = key_string(key_str, LEN, key); - assert(err == TESLA_SUCCESS); - - char *trans_str = transition_matrix(trans); - - switch (class->ts_action) { - case TESLA_ACTION_FAILSTOP: - tesla_panic(message, class->ts_name, class->ts_description, - key_str, trans_str); - break; - - case TESLA_ACTION_DTRACE: - tesla_assert_fail_dtrace(class, NULL, trans); - return; - - case TESLA_ACTION_PRINTF: -#if defined(_KERNEL) && defined(KDB) - kdb_backtrace(); -#endif - printf(message, class->ts_name, class->ts_description, - key_str, trans_str); - break; - } - - tesla_free(trans_str); -} - -void -tesla_assert_fail(struct tesla_class *tsp, struct tesla_instance *tip, - const struct tesla_transitions *trans) -{ - assert(tsp != NULL); - assert(tip != NULL); - - if (tsp->ts_handler != NULL) { - tsp->ts_handler(tip); - return; - } - - switch (tsp->ts_action) { - case TESLA_ACTION_FAILSTOP: - tesla_panic( - "TESLA failure; in automaton '%s':\n%s\n\n" - "required to take a transition in %s " - "but currently in state %d", - tsp->ts_name, tsp->ts_description, - transition_matrix(trans), tip->ti_state); - break; /* A bit gratuitous. */ - - case TESLA_ACTION_DTRACE: - tesla_assert_fail_dtrace(tsp, tip, trans); - return; - - case TESLA_ACTION_PRINTF: -#if defined(_KERNEL) && defined(KDB) - kdb_backtrace(); -#endif - printf("tesla_assert_failed: %s: %s\n", tsp->ts_name, - tsp->ts_description); - break; - } -} - -void -tesla_class_setaction(struct tesla_class *tsp, - tesla_assert_fail_callback handler) -{ - - tsp->ts_handler = handler; -} ==== //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_internal.h#5 (text+ko) ==== @@ -106,33 +106,6 @@ int32_t tesla_key_union(struct tesla_key *dest, const struct tesla_key *source); -#ifndef NDEBUG - -#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? */ -int32_t verbose_debug(void); - -#else // NDEBUG - -// When not in debug mode, some values might not get checked. -#define __debug __unused -#define DEBUG_PRINT(...) -#define VERBOSE_PRINT(...) - -int32_t verbose_debug(void) { return 0; } - -#endif - #ifndef __unused #if __has_attribute(unused) #define __unused __attribute__((unused)) @@ -198,7 +171,6 @@ const char *ts_description;/* Description of the assertion. */ uint32_t ts_scope; /* Per-thread or global. */ uint32_t ts_limit; /* Simultaneous automata limit. */ - tesla_assert_fail_callback ts_handler; /* Run on failure. */ uint32_t ts_action; /* What to do on failure. */ /* @@ -248,9 +220,11 @@ int tesla_class_init(struct tesla_class*, uint32_t context, uint32_t instances); +#if 0 //! We have failed to find an instance that matches a @ref tesla_key. void tesla_match_fail(struct tesla_class*, const struct tesla_key*, const struct tesla_transitions*); +#endif /* * XXXRW: temporarily, maximum number of classes and instances are hard-coded @@ -289,19 +263,28 @@ /* * Event notification: */ -void tesla_state_notify_new_instance(struct tesla_class *, +/** A new @ref tesla_instance has been created. */ +void tesla_notify_new_instance(struct tesla_class *, struct tesla_instance *); -void tesla_state_notify_transition(struct tesla_class *, - struct tesla_instance *, const struct tesla_transitions *, uint32_t index); +/** A @ref tesla_instance has taken an expected transition. */ +void tesla_notify_transition(struct tesla_class *, struct tesla_instance *, + const struct tesla_transitions *, uint32_t index); -void tesla_state_notify_clone(struct tesla_class *, struct tesla_instance *, +/** An exisiting @ref tesla_instance has been cloned because of an event. */ +void tesla_notify_clone(struct tesla_class *, struct tesla_instance *, const struct tesla_transitions *, uint32_t index); -void tesla_state_notify_fail(struct tesla_class *, struct tesla_instance *, +/** A @ref tesla_instance was unable to take any of a set of transitions. */ +void tesla_notify_assert_fail(struct tesla_class *, struct tesla_instance *, + const struct tesla_transitions *); + +/** No @ref tesla_class instance was found to match a @ref tesla_key. */ +void tesla_notify_match_fail(struct tesla_class *, const struct tesla_key *, const struct tesla_transitions *); -void tesla_state_notify_pass(struct tesla_class *, struct tesla_instance *); +/** A @ref tesla_instance has "passed" (worked through the automaton). */ +void tesla_notify_pass(struct tesla_class *, struct tesla_instance *); /* * DTrace notifications of various events. @@ -318,6 +301,47 @@ * Debug helpers. */ +#define SAFE_SPRINTF(current, end, ...) do { \ + int written = snprintf(current, end - current, __VA_ARGS__); \ + if ((written > 0) && (current + written < end)) \ + current += written; \ +} while (0) + +#define print(...) printf(__VA_ARGS__) + +#ifdef _KERNEL +#define error(...) printf(__VA_ARGS__) +#else +#define error(...) fprintf(stderr, __VA_ARGS__) +#endif + +#ifndef NDEBUG + +#define __debug + +#ifdef _KERNEL +#include <sys/systm.h> +#define DEBUG_PRINT(...) print(__VA_ARGS__) +#else +#include <stdio.h> +#define DEBUG_PRINT(...) print(__VA_ARGS__) +#endif +#define VERBOSE_PRINT(...) if (verbose_debug()) DEBUG_PRINT(__VA_ARGS__) + +/** Are we in (verbose) debug mode? */ +int32_t verbose_debug(void); + +#else // NDEBUG + +// When not in debug mode, some values might not get checked. +#define __debug __unused +#define DEBUG_PRINT(...) +#define VERBOSE_PRINT(...) + +int32_t verbose_debug(void) { return 0; } + +#endif + /** * Assert that a @ref tesla_instance is an instance of a @ref tesla_class. * @@ -330,7 +354,7 @@ void assert_instanceof(struct tesla_instance *i, struct tesla_class *tclass); /** Print a key into a buffer. */ -int key_string(char *buffer, size_t len, const struct tesla_key *key); +char* key_string(char *buffer, const char *end, const struct tesla_key *); /** Print a @ref tesla_key to stderr. */ void print_key(const struct tesla_key *key); @@ -338,7 +362,11 @@ /** Print a @ref tesla_class to stderr. */ void print_class(const struct tesla_class*); -/** Provide a human-readable rendition of a transition matrix. */ -char* transition_matrix(const struct tesla_transitions*); +/** Print a human-readable version of @ref tesla_transitions. */ +void print_transitions(const struct tesla_transitions *); + +/** Print a human-readable version of @ref tesla_transitions into a buffer. */ +char* sprint_transitions(char *buffer, const char *end, + const struct tesla_transitions *); #endif /* TESLA_INTERNAL_H */ ==== //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_notification.c#3 (text+ko) ==== @@ -32,8 +32,12 @@ #include "tesla_internal.h" +#define ERROR_BUFFER_LENGTH 1024 + +static void print_failure_header(const struct tesla_class *); + void -tesla_state_notify_new_instance(struct tesla_class *tcp, +tesla_notify_new_instance(struct tesla_class *tcp, struct tesla_instance *tip) { @@ -59,7 +63,7 @@ } void -tesla_state_notify_clone(struct tesla_class *tcp, struct tesla_instance *tip, +tesla_notify_clone(struct tesla_class *tcp, struct tesla_instance *tip, const struct tesla_transitions *transp, uint32_t index) { @@ -80,7 +84,7 @@ tip->ti_state, t->to); if (t->flags & TESLA_TRANS_CLEANUP) - tesla_state_notify_pass(tcp, tip); + tesla_notify_pass(tcp, tip); break; } @@ -88,7 +92,7 @@ } void -tesla_state_notify_transition(struct tesla_class *tcp, +tesla_notify_transition(struct tesla_class *tcp, struct tesla_instance *tip, const struct tesla_transitions *transp, uint32_t index) { @@ -109,7 +113,7 @@ t->from, t->to); if (t->flags & TESLA_TRANS_CLEANUP) - tesla_state_notify_pass(tcp, tip); + tesla_notify_pass(tcp, tip); break; } @@ -117,23 +121,86 @@ } void -tesla_state_notify_fail(struct tesla_class *tcp, struct tesla_instance *tip, +tesla_notify_assert_fail(struct tesla_class *tcp, struct tesla_instance *tip, const struct tesla_transitions *transp) { + assert(tcp != NULL); + assert(tip != NULL); + + if (tcp->ts_action == TESLA_ACTION_DTRACE) { + tesla_assert_fail_dtrace(tcp, tip, transp); + return; + } + + print_failure_header(tcp); + char buffer[ERROR_BUFFER_LENGTH]; + char *next = buffer; + const char *end = buffer + sizeof(buffer); + + SAFE_SPRINTF(next, end, + "Instance %td is in state %d\n" + "but required to take a transition in ", + (tip - tcp->ts_table->tt_instances), tip->ti_state); + assert(next > buffer); + + next = sprint_transitions(next, end, transp); + switch (tcp->ts_action) { case TESLA_ACTION_DTRACE: - tesla_assert_fail_dtrace(tcp, tip, transp); + assert(0 && "handled above"); + return; + + case TESLA_ACTION_FAILSTOP: + tesla_panic("%s", buffer); + break; + + case TESLA_ACTION_PRINTF: + error("%s", buffer); + break; + } +} + +void +tesla_notify_match_fail(struct tesla_class *tcp, const struct tesla_key *tkp, + const struct tesla_transitions *transp) +{ + assert(tcp != NULL); + assert(tkp != NULL); + + if (tcp->ts_action == TESLA_ACTION_DTRACE) { + tesla_assert_fail_dtrace(tcp, NULL, NULL); return; + } + + print_failure_header(tcp); + + char buffer[ERROR_BUFFER_LENGTH]; + char *next = buffer; + const char *end = buffer + sizeof(buffer); + + SAFE_SPRINTF(next, end, "No instance matched key '"); + next = key_string(next, end, tkp); + SAFE_SPRINTF(next, end, "' for transition(s) "); + next = sprint_transitions(next, end, transp); + + switch (tcp->ts_action) { + case TESLA_ACTION_DTRACE: + assert(0 && "handled above"); + break; - default: - /* for now, don't do anything */ + case TESLA_ACTION_FAILSTOP: + tesla_panic("%s", buffer); + break; + + case TESLA_ACTION_PRINTF: + error("%s", buffer); break; } } void -tesla_state_notify_pass(struct tesla_class *tcp, struct tesla_instance *tip) +tesla_notify_pass(struct tesla_class *tcp, struct tesla_instance *tip) { switch (tcp->ts_action) { @@ -148,3 +215,16 @@ } } + +static void +print_failure_header(const struct tesla_class *tcp) +{ + + error("\n\nTESLA failure:\n"); +#if defined(_KERNEL) && defined(KDB) + kdb_backtrace(); +#endif + + error("In automaton '%s':\n%s\n", tcp->ts_name, tcp->ts_description); +} + ==== //depot/projects/ctsrd/tesla/src/lib/libtesla/update.c#6 (text+ko) ==== @@ -58,10 +58,8 @@ : "per-thread")); DEBUG_PRINT(" class: %d ('%s')\n", class_id, name); - char *matrix = transition_matrix(trans); - DEBUG_PRINT(" transitions: %s", matrix); - tesla_free(matrix); - + DEBUG_PRINT(" transitions: "); + print_transitions(trans); DEBUG_PRINT("\n"); DEBUG_PRINT(" key: "); print_key(key); @@ -139,8 +137,7 @@ // instructed to fork), just update the state. if (!(t->flags & TESLA_TRANS_FORK) && key->tk_mask == k->tk_mask) { - tesla_state_notify_transition(class, inst, - trans, j); + tesla_notify_transition(class, inst, trans, j); inst->ti_state = t->to; break; @@ -148,7 +145,7 @@ // If the keys weren't an exact match, we need to fork // a new (more specific) automaton instance. - tesla_state_notify_clone(class, inst, trans, j); + tesla_notify_clone(class, inst, trans, j); struct tesla_instance *clone = clones + cloned++; *clone = *inst; @@ -159,7 +156,7 @@ } if (transition_required && !transition_taken) - tesla_assert_fail(class, inst, trans); + tesla_notify_assert_fail(class, inst, trans); } // Move any clones into the instance. @@ -180,7 +177,7 @@ assert(tesla_instance_active(inst)); matched_something = true; - tesla_state_notify_new_instance(class, inst); + tesla_notify_new_instance(class, inst); } if (t->flags & TESLA_TRANS_CLEANUP) { @@ -195,7 +192,7 @@ } if (!matched_something) - tesla_match_fail(class, key, trans); + tesla_notify_match_fail(class, key, trans); tesla_class_put(class);help
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201303201857.r2KIv5I0023497>
