PERFORCE change 222980 for review
Robert Watson
rwatson at FreeBSD.org
Sun Mar 17 21:17:53 UTC 2013
http://p4web.freebsd.org/@@222980?ac=10
Change 222980 by rwatson at 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 *
More information about the p4-projects
mailing list