PERFORCE change 223080 for review

Robert Watson rwatson at FreeBSD.org
Wed Mar 20 18:57:06 UTC 2013


http://p4web.freebsd.org/@@223080?ac=10

Change 223080 by rwatson at 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);
 


More information about the p4-projects mailing list