Date: Sun, 17 Mar 2013 21:17:51 GMT From: Robert Watson <rwatson@FreeBSD.org> To: Perforce Change Reviews <perforce@FreeBSD.org> Subject: PERFORCE change 222980 for review Message-ID: <201303172117.r2HLHpvu099918@skunkworks.freebsd.org>
next in thread | raw e-mail | index | archive | help
http://p4web.freebsd.org/@@222980?ac=10 Change 222980 by rwatson@rwatson_cinnamon on 2013/03/17 21:17:13 Merge more recent libtesla into the kernel version; in a few cases, make changes to either merge with incorrect expectations (e.g., tesla_store_destroy -> tesla_store_free), and to fix some problems in the imported version (e.g., free -> tesla_free). Affected files ... .. //depot/projects/ctsrd/tesla/src/sys/libtesla/debug.c#3 integrate .. //depot/projects/ctsrd/tesla/src/sys/libtesla/libtesla.h#3 integrate .. //depot/projects/ctsrd/tesla/src/sys/libtesla/state-global.c#2 integrate .. //depot/projects/ctsrd/tesla/src/sys/libtesla/state-perthread.c#3 edit .. //depot/projects/ctsrd/tesla/src/sys/libtesla/state.c#3 edit .. //depot/projects/ctsrd/tesla/src/sys/libtesla/store.c#3 edit .. //depot/projects/ctsrd/tesla/src/sys/libtesla/tesla_internal.h#4 edit .. //depot/projects/ctsrd/tesla/src/sys/libtesla/update.c#4 integrate .. //depot/projects/ctsrd/tesla/src/sys/libtesla/util.c#2 integrate Differences ... ==== //depot/projects/ctsrd/tesla/src/sys/libtesla/debug.c#3 (text+ko) ==== @@ -1,6 +1,6 @@ -/** @file tesla_debug.c Debugging helpers for TESLA state. */ +/** @file debug.c Debugging helpers for TESLA state. */ /*- - * Copyright (c) 2012 Jonathan Anderson + * Copyright (c) 2012-2013 Jonathan Anderson * All rights reserved. * * This software was developed by SRI International and the University of @@ -37,6 +37,11 @@ #include <stdlib.h> #endif +#define SAFE_SPRINTF(dest, end, ...) \ + dest += snprintf(dest, end - dest, __VA_ARGS__); \ + if (dest >= end) \ + return (TESLA_ERROR_ENOMEM); + char* transition_matrix(const struct tesla_transitions *trans) { @@ -59,6 +64,27 @@ return buffer; } +int +key_string(char *buffer, size_t len, const struct tesla_key *key) +{ + char *current = buffer; + const char *end = buffer + len; + + SAFE_SPRINTF(current, 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 "); + } + } + + SAFE_SPRINTF(current, end, "]"); + + return (TESLA_SUCCESS); +} + #ifndef NDEBUG #define print DEBUG_PRINT @@ -136,17 +162,13 @@ void print_key(const struct tesla_key *key) { - print("0x%tx [ ", key->tk_mask); + static const size_t LEN = 15 * TESLA_KEY_SIZE + 10; + char buffer[LEN]; - for (int32_t i = 0; i < TESLA_KEY_SIZE; i++) { - if (key->tk_mask & (1 << i)) { - print("%tx ", key->tk_keys[i]); - } else { - print("X "); - } - } + int err = key_string(buffer, LEN, key); + assert(err == TESLA_SUCCESS); - print("]"); + printf("%s", buffer); } #endif /* !NDEBUG */ ==== //depot/projects/ctsrd/tesla/src/sys/libtesla/libtesla.h#3 (text+ko) ==== @@ -122,6 +122,8 @@ int32_t tesla_store_reset(struct tesla_store *store); +/** Clean up a @ref tesla_store. */ +void tesla_store_free(struct tesla_store*); /** * A description of a TESLA automaton, which may be instantiated a number of ==== //depot/projects/ctsrd/tesla/src/sys/libtesla/state-global.c#2 (text+ko) ==== @@ -1,5 +1,6 @@ /*- * Copyright (c) 2011 Robert N. M. Watson + * Copyright (c) 2012-2013 Jonathan Anderson * All rights reserved. * * This software was developed by SRI International and the University of ==== //depot/projects/ctsrd/tesla/src/sys/libtesla/state-perthread.c#3 (text+ko) ==== @@ -1,5 +1,6 @@ /*- * Copyright (c) 2011 Robert N. M. Watson + * Copyright (c) 2012-2013 Jonathan Anderson * All rights reserved. * * This software was developed by SRI International and the University of @@ -73,7 +74,7 @@ store = curthread->td_tesla; curthread->td_tesla = NULL; - tesla_store_destroy(store); + tesla_store_free(store); tesla_free(store); } ==== //depot/projects/ctsrd/tesla/src/sys/libtesla/state.c#3 (text+ko) ==== @@ -1,6 +1,7 @@ /*- * Copyright (c) 2011 Robert N. M. Watson * Copyright (c) 2011 Anil Madhavapeddy + * Copyright (c) 2012-2013 Jonathan Anderson * All rights reserved. * * This software was developed by SRI International and the University of @@ -80,6 +81,14 @@ } +void +tesla_class_free(struct tesla_class *class) +{ + tesla_free(class->ts_table); + tesla_free(class); +} + + int tesla_match(struct tesla_class *tclass, const struct tesla_key *pattern, struct tesla_instance **array, uint32_t *size) @@ -202,6 +211,53 @@ } 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; + +#ifdef NOTYET + case TESLA_ACTION_DTRACE: + dtrace_probe(...); + return; +#endif + + 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) { @@ -216,11 +272,11 @@ switch (tsp->ts_action) { case TESLA_ACTION_FAILSTOP: tesla_panic( - "tesla_assert_failed: " - "unable to move '%s' from state %d" - " according to transition matrix %s", - tsp->ts_name, tip->ti_state, - transition_matrix(trans)); + "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. */ #ifdef NOTYET case TESLA_ACTION_DTRACE: ==== //depot/projects/ctsrd/tesla/src/sys/libtesla/store.c#3 (text+ko) ==== @@ -123,6 +123,16 @@ } +void +tesla_store_free(tesla_store *store) +{ + for (uint32_t i = 0; i < store->length; i++) + tesla_class_free(store->classes + i); + + tesla_free(store); +} + + int32_t tesla_class_get(tesla_store *store, uint32_t id, tesla_class **tclassp, const char *name, const char *description) ==== //depot/projects/ctsrd/tesla/src/sys/libtesla/tesla_internal.h#4 (text+ko) ==== @@ -63,7 +63,12 @@ /** * Call this if things go catastrophically, unrecoverably wrong. */ -void tesla_die(char *message) __attribute__((noreturn)); +void tesla_die(const char *event) __attribute__((noreturn)); + +/** + * Clean up a @ref tesla_class. + */ +void tesla_class_free(struct tesla_class*); /** * Create a new @ref tesla_instance. @@ -108,7 +113,7 @@ #define DEBUG_PRINT(...) printf(__VA_ARGS__) #else #include <stdio.h> -#define DEBUG_PRINT(...) fprintf(stderr, __VA_ARGS__) +#define DEBUG_PRINT(...) printf(__VA_ARGS__) #endif #define VERBOSE_PRINT(...) if (verbose_debug()) DEBUG_PRINT(__VA_ARGS__) @@ -126,6 +131,13 @@ #endif +#ifndef __unused +#if __has_attribute(unused) +#define __unused __attribute__((unused)) +#else +#define __unused +#endif +#endif // Kernel vs userspace implementation details. #ifdef _KERNEL @@ -226,7 +238,6 @@ */ int tesla_store_init(tesla_store*, uint32_t context, uint32_t classes, uint32_t instances); -void tesla_store_destroy(tesla_store*); /** * Initialize @ref tesla_class internals. @@ -235,6 +246,10 @@ int tesla_class_init(struct tesla_class*, uint32_t context, uint32_t instances); +//! 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*); + /* * XXXRW: temporarily, maximum number of classes and instances are hard-coded * constants. In the future, this should somehow be more dynamic. @@ -284,6 +299,9 @@ */ 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); + /** Print a @ref tesla_key to stderr. */ void print_key(const struct tesla_key *key); ==== //depot/projects/ctsrd/tesla/src/sys/libtesla/update.c#4 (text+ko) ==== @@ -87,69 +87,90 @@ assert(table->tt_length <= 32); + // Did we match any instances? + bool matched_something = false; + + // Make space for cloning existing instances. + tesla_instance clones[table->tt_free]; + size_t cloned = 0; + // Update existing instances, forking/specialising if necessary. for (uint32_t i = 0; i < table->tt_length; i++) { tesla_instance *inst = table->tt_instances + i; if (!tesla_instance_active(inst)) continue; - bool failure = false; + // Is this instance required to take a transition? + bool transition_required = false; + + // Has this instance actually taken a transition? + bool transition_taken = false; + for (uint32_t j = 0; j < trans->length; j++) { tesla_transition *t = trans->transitions + j; + const tesla_key *k = &inst->ti_key; // Check whether or not the instance matches the // provided key, masked by what the transition says to // expect from its 'previous' state. - tesla_key pattern = *key; - pattern.tk_mask &= t->mask; + tesla_key masked = *key; + masked.tk_mask &= t->mask; - if (!tesla_key_matches(&pattern, &inst->ti_key)) + if (!tesla_key_matches(&masked, k)) continue; - tesla_key *k = &inst->ti_key; - if (!t->fork && (k->tk_mask != pattern.tk_mask)) - continue; + if (inst->ti_state != t->from) { + // If the instance matches everything but the + // state, so there had better be a transition + // somewhere in 'trans' that can be taken! + if (k->tk_mask == masked.tk_mask) + transition_required = true; - // At this point, predjudice attaches: the instance - // matches a pattern in all ways that matter, so if - // it's not in the expected state, there had better - // be a successful transition somewhere in 'trans' - // that can be taken. - if (inst->ti_state != t->from) { - failure = true; continue; } + // The match has succeeded: we are either going to + // update or clone an existing state. + transition_taken = true; + matched_something = true; + // If the keys just match (and we haven't been explictly // instructed to fork), just update the state. - if (!t->fork - && SUBSET(key->tk_mask, k->tk_mask)) { + if (!t->fork && key->tk_mask == k->tk_mask) { VERBOSE_PRINT("update %td: %tx->%tx\n", inst - start, t->from, t->to); inst->ti_state = t->to; - failure = false; break; } // If the keys weren't an exact match, we need to fork // a new (more specific) automaton instance. - struct tesla_instance *copy; - CHECK(tesla_clone, class, inst, ©); - VERBOSE_PRINT("clone %td:%tx -> %td:%tx\n", + struct tesla_instance *clone = clones + cloned++; + *clone = *inst; + clone->ti_state = t->to; + + VERBOSE_PRINT("clone %td:%tx -> %tx\n", inst - start, inst->ti_state, - copy - start, t->to); + t->to); - CHECK(tesla_key_union, ©->ti_key, key); - copy->ti_state = t->to; - failure = false; + CHECK(tesla_key_union, &clone->ti_key, key); break; } - if (failure) + if (transition_required && !transition_taken) tesla_assert_fail(class, inst, trans); } + // Move any clones into the instance. + for (size_t i = 0; i < cloned; i++) { + struct tesla_instance *clone = clones + i; + struct tesla_instance *copied_in_place; + + CHECK(tesla_clone, class, clone, &copied_in_place); + } + + // If there is a (0 -> anything) transition, create a new instance. for (uint32_t i = 0; i < trans->length; i++) { const tesla_transition *t = trans->transitions + i; @@ -160,6 +181,7 @@ 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); } @@ -170,6 +192,9 @@ DEBUG_PRINT("\n====\n\n"); } + if (!matched_something) + tesla_match_fail(class, key, trans); + tesla_class_put(class); return (TESLA_SUCCESS); ==== //depot/projects/ctsrd/tesla/src/sys/libtesla/util.c#2 (text+ko) ==== @@ -1,5 +1,6 @@ /*- * Copyright (c) 2011 Robert N. M. Watson + * Copyright (c) 2012-2013 Jonathan Anderson * All rights reserved. * * This software was developed by SRI International and the University of @@ -34,9 +35,9 @@ void -tesla_die(char *message) +tesla_die(const char *event) { - tesla_panic("tesla_die: '%s'\n", message); + tesla_panic("tesla_die: fatal error in event '%s'\n", event); } const char *
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201303172117.r2HLHpvu099918>