PERFORCE change 229141 for review
Jonathan Anderson
jonathan at FreeBSD.org
Thu May 30 07:46:31 UTC 2013
http://p4web.freebsd.org/@@229141?ac=10
Change 229141 by jonathan at jonathan-on-joe on 2013/05/30 07:45:34
Update libtesla in Perforce. Hopefully these new filenames will make it easier to merge things into the kernel.
Affected files ...
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/Makefile#4 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/config.h#1 add
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/debug.c#5 delete
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/key.c#3 delete
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/libtesla.h#5 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/state-global.c#3 delete
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/state-perthread.c#5 delete
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/state.c#6 delete
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/store.c#4 delete
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla.h#5 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_class.c#1 add
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_class_global.c#1 add
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_class_perthread.c#1 add
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_debug.c#1 add
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_dtrace.c#2 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_internal.h#6 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_key.c#1 add
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_notification.c#4 edit
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_store.c#1 add
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_strnlen.h#1 add
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_update.c#1 add
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_util.c#1 add
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/update.c#7 delete
.. //depot/projects/ctsrd/tesla/src/lib/libtesla/util.c#4 delete
Differences ...
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/Makefile#4 (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= tesla_class.c tesla_class_global.c tesla_class_perthread.c \
+ tesla_debug.c tesla_dtrace.c tesla_key.c tesla_notification.c \
+ tesla_store.c tesla_update.c tesla_util.c
.include <bsd.lib.mk>
-
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/libtesla.h#5 (text+ko) ====
@@ -60,16 +60,18 @@
uint32_t from;
/** The mask of the state we're moving from. */
- uint32_t mask;
+ uint32_t from_mask;
/** The state we are moving to. */
uint32_t to;
+ /** A mask of the keys that the 'to' state should have set. */
+ uint32_t to_mask;
+
/** 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. */
@@ -213,7 +215,7 @@
*
* @returns 1 if active, 0 if inactive
*/
-int32_t tesla_instance_active(struct tesla_instance *i);
+int32_t tesla_instance_active(const struct tesla_instance *i);
/** Clone an existing instance into a new instance. */
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla.h#5 (text+ko) ====
@@ -84,7 +84,27 @@
/** Function events inside this predicate refer to the caller context. */
struct __tesla_event* __tesla_caller(__tesla_event*, ...);
+/**
+ * Events named in this predicate should only occur exactly as described.
+ *
+ * This is the default behaviour for explicit automata representations.
+ */
+struct __tesla_event* __tesla_strict(__tesla_event*, ...);
+/**
+ * Events named in this predicate must occur as described <i>if</i> the
+ * execution trace includes a NOW event; otherwise, any number of non-NOW
+ * events can occur in any order.
+ *
+ * For instance, if the assertion names the VOP_WRITE() event, we don't want
+ * to preclude the use of VOP_WRITE() in code paths that don't include this
+ * assertion's NOW event.
+ *
+ * This is the default behaviour for inline assertions.
+ */
+struct __tesla_event* __tesla_conditional(__tesla_event*, ...);
+
+
/** Nothing to see here, move along... */
struct __tesla_event* __tesla_ignore;
@@ -108,14 +128,35 @@
*/
struct __tesla_automaton_description;
+struct __tesla_automaton_usage;
/** In an explicit automata description, return this to say "we're done". */
struct __tesla_automaton_description* __tesla_automaton_done();
+inline struct __tesla_automaton_usage*
+__tesla_struct_uses_automaton(const char *automaton,
+ __tesla_locality *loc, ...)
+{
+ return 0;
+}
+
+
+/**
+ * Declare that a struct's behaviour is described by an automaton.
+ *
+ * @param struct_name name of the struct that uses the automaton
+ * @param automaton reference to the automaton description
+ * @param loc a TESLA locality (global, per-thread...)
+ * @param start event that kicks off the automaton
+ * @param end event that winds up the automaton
+ */
+#define __tesla_struct_usage(subject, automaton, loc, start, end) \
+ struct __tesla_automaton_usage* \
+ __tesla_struct_automaton_usage_##struct_name##_##automaton(subject) { \
+ return __tesla_struct_uses_automaton( \
+ #automaton, loc, start, end); \
+ }
-/** Declare an automaton that describes behaviour of this struct. */
-#define __tesla_struct_automaton(fn_name) \
- void *__tesla_automaton_struct_uses_##fn_name;
/**
* Define an automaton to describe a struct's behaviour.
@@ -138,19 +179,22 @@
#define __tesla_global ((struct __tesla_locality*) 0)
#define __tesla_perthread ((struct __tesla_locality*) 0)
-#define __tesla_sequence(...) 1
+#define __tesla_sequence(...) 1
-#define __tesla_struct_automaton(fn_name)
+#define __tesla_struct_automaton(...)
#define __tesla_automaton(name, ...)
-#define __tesla_call(...) 0
-#define __tesla_return(...) 0
+#define __tesla_call(...) 0
+#define __tesla_return(...) 0
+
+#define __tesla_callee(...) 0
+#define __tesla_caller(...) 0
-#define __tesla_callee(...) 0
-#define __tesla_caller(...) 0
+#define __tesla_optional(...) 0
+#define __tesla_any(...) 0
-#define __tesla_optional(...) 0
-#define __tesla_any(...) 0
+#define __tesla_strict(...) 0
+#define __tesla_conditional(...) 0
#endif /* __TESLA_ANALYSER__ */
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_dtrace.c#2 (text+ko) ====
@@ -47,8 +47,7 @@
void
tesla_state_transition_dtrace(struct tesla_class *tcp,
struct tesla_instance *tip,
- __unused const struct tesla_transitions *transp,
- __unused uint32_t transition_index)
+ __unused const struct tesla_transition *transp)
{
SDT_PROBE(tesla, kernel, , state_transition, tcp, tip, 0, 0, 0);
@@ -80,8 +79,7 @@
void
tesla_state_transition_dtrace(__unused struct tesla_class *tcp,
__unused struct tesla_instance *tip,
- __unused const struct tesla_transitions *transp,
- __unused uint32_t transition_index)
+ __unused const struct tesla_transition *transp)
{
assert(0 && "DTrace not implemented in userspace");
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_internal.h#6 (text+ko) ====
@@ -33,6 +33,8 @@
#ifndef TESLA_INTERNAL_H
#define TESLA_INTERNAL_H
+#include "config.h"
+
#ifdef _KERNEL
#include "opt_kdb.h"
#include <sys/param.h>
@@ -70,7 +72,7 @@
/**
* Clean up a @ref tesla_class.
*/
-void tesla_class_free(struct tesla_class*);
+void tesla_class_destroy(struct tesla_class*);
/**
* Create a new @ref tesla_instance.
@@ -102,6 +104,31 @@
int32_t tesla_match(struct tesla_class *tclass, const struct tesla_key *key,
struct tesla_instance **array, uint32_t *size);
+/** Actions that can be taken by @ref tesla_update_state. */
+enum tesla_action_t {
+ /** The instance's state should be updated. */
+ UPDATE,
+
+ /** The instance should be copied to a new instance. */
+ FORK,
+
+ /** The instance is irrelevant to the given transitions. */
+ IGNORE,
+
+ /** The instance matches, but there are no valid transitions for it. */
+ FAIL
+};
+
+/**
+ * What is the correct action to perform on a given @ref tesla_instance to
+ * satisfy a set of @ref tesla_transitions?
+ *
+ * @param[out] trigger the @ref tesla_transition that triggered the action
+ */
+enum tesla_action_t tesla_action(const struct tesla_instance*,
+ const struct tesla_key*, const struct tesla_transitions*,
+ const struct tesla_transition** trigger);
+
/** Copy new entries from @ref source into @ref dest. */
int32_t tesla_key_union(struct tesla_key *dest, const struct tesla_key *source);
@@ -153,44 +180,30 @@
/*
- * Instance table definition, used for both global and per-thread scopes. A
- * more refined data structure might eventually be used here.
- */
-struct tesla_table {
- uint32_t tt_length;
- uint32_t tt_free;
- struct tesla_instance tt_instances[];
-};
-
-/*
* Assertion state definition is internal to libtesla so we can change it as
* we need to.
*/
struct tesla_class {
- const char *ts_name; /* Name of the assertion. */
- const char *ts_description;/* Description of the assertion. */
- uint32_t ts_scope; /* Per-thread or global. */
- uint32_t ts_limit; /* Simultaneous automata limit. */
- uint32_t ts_action; /* What to do on failure. */
+ const char *tc_name; /* Name of the assertion. */
+ const char *tc_description;/* Description of the assertion. */
+ uint32_t tc_scope; /* Per-thread or global. */
+ uint32_t tc_limit; /* Simultaneous automata limit. */
+ uint32_t tc_action; /* What to do on failure. */
+
+ struct tesla_instance *tc_instances; /* Instances of this class. */
+ uint32_t tc_free; /* Unused instances. */
- /*
- * State fields if global. Table must be last field as it uses a
- * zero-length array.
- */
#ifdef _KERNEL
- struct mtx ts_lock; /* Synchronise ts_table. */
+ struct mtx tc_lock; /* Synchronise tc_table. */
#else
- pthread_mutex_t ts_lock; /* Synchronise ts_table. */
+ pthread_mutex_t tc_lock; /* Synchronise tc_table. */
#endif
-
- struct tesla_table *ts_table; /* Table of instances. */
};
typedef struct tesla_class tesla_class;
typedef struct tesla_instance tesla_instance;
typedef struct tesla_key tesla_key;
typedef struct tesla_store tesla_store;
-typedef struct tesla_table tesla_table;
typedef struct tesla_transition tesla_transition;
typedef struct tesla_transitions tesla_transitions;
@@ -269,11 +282,12 @@
/** 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);
+ const struct tesla_transition*);
/** 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_notify_clone(struct tesla_class *,
+ struct tesla_instance *old_instance, struct tesla_instance *new_instance,
+ const struct tesla_transition*);
/** 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 *,
@@ -290,8 +304,7 @@
* DTrace notifications of various events.
*/
void tesla_state_transition_dtrace(struct tesla_class *,
- struct tesla_instance *, const struct tesla_transitions *,
- uint32_t transition_index);
+ struct tesla_instance *, const struct tesla_transition *);
void tesla_assert_fail_dtrace(struct tesla_class *,
struct tesla_instance *, const struct tesla_transitions *);
void tesla_assert_pass_dtrace(struct tesla_class *,
@@ -321,24 +334,23 @@
#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);
+int32_t tesla_debugging(const char*);
+
+#define DEBUG(dclass, ...) \
+ if (tesla_debugging(#dclass)) printf(__VA_ARGS__)
#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; }
+#define DEBUG(...)
+int32_t tesla_debugging(const char*) { return 0; }
#endif
@@ -357,13 +369,20 @@
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);
+void print_key(const char *debug_name, const struct tesla_key *key);
/** Print a @ref tesla_class to stderr. */
void print_class(const struct tesla_class*);
+/** Print a human-readable version of a @ref tesla_transition. */
+void print_transition(const char *debug, const struct tesla_transition *);
+
+/** Print a human-readable version of a @ref tesla_transition into a buffer. */
+char* sprint_transition(char *buffer, const char *end,
+ const struct tesla_transition *);
+
/** Print a human-readable version of @ref tesla_transitions. */
-void print_transitions(const struct tesla_transitions *);
+void print_transitions(const char *debug, const struct tesla_transitions *);
/** Print a human-readable version of @ref tesla_transitions into a buffer. */
char* sprint_transitions(char *buffer, const char *end,
==== //depot/projects/ctsrd/tesla/src/lib/libtesla/tesla_notification.c#4 (text+ko) ====
@@ -41,17 +41,16 @@
struct tesla_instance *tip)
{
- switch (tcp->ts_action) {
+ switch (tcp->tc_action) {
case TESLA_ACTION_DTRACE:
/* XXXRW: more fine-grained DTrace probes? */
- tesla_state_transition_dtrace(tcp, tip, NULL, -1);
+ tesla_state_transition_dtrace(tcp, tip, NULL);
return;
default:
/* for the PRINTF action, should this be a non-verbose print? */
- VERBOSE_PRINT("new %td: %tx\n",
- tip - tcp->ts_table->tt_instances,
- tip->ti_state);
+ DEBUG(libtesla.instance.new, "new %td: %tx\n",
+ tip - tcp->tc_instances, tip->ti_state);
/*
* XXXJA: convince self that we can never "pass" an assertion
@@ -63,28 +62,24 @@
}
void
-tesla_notify_clone(struct tesla_class *tcp, struct tesla_instance *tip,
- const struct tesla_transitions *transp, uint32_t index)
+tesla_notify_clone(struct tesla_class *tcp,
+ struct tesla_instance *old_instance, struct tesla_instance *new_instance,
+ const struct tesla_transition *transp)
{
- switch (tcp->ts_action) {
+ switch (tcp->tc_action) {
case TESLA_ACTION_DTRACE:
/* XXXRW: more fine-grained DTrace probes? */
- tesla_state_transition_dtrace(tcp, tip, transp, index);
+ tesla_state_transition_dtrace(tcp, new_instance, transp);
return;
default: {
- /* for the PRINTF action, should this be a non-verbose print? */
- assert(index >= 0);
- assert(index < transp->length);
- const struct tesla_transition *t = transp->transitions + index;
+ DEBUG(libtesla.instance.clone, "clone %td:%tx -> %td:%tx\n",
+ old_instance - tcp->tc_instances, transp->from,
+ new_instance - tcp->tc_instances, transp->to);
- VERBOSE_PRINT("clone %td:%tx -> %tx\n",
- tip - tcp->ts_table->tt_instances,
- tip->ti_state, t->to);
-
- if (t->flags & TESLA_TRANS_CLEANUP)
- tesla_notify_pass(tcp, tip);
+ if (transp->flags & TESLA_TRANS_CLEANUP)
+ tesla_notify_pass(tcp, new_instance);
break;
}
@@ -93,26 +88,19 @@
void
tesla_notify_transition(struct tesla_class *tcp,
- struct tesla_instance *tip, const struct tesla_transitions *transp,
- uint32_t index)
+ struct tesla_instance *tip, const struct tesla_transition *transp)
{
- switch (tcp->ts_action) {
+ switch (tcp->tc_action) {
case TESLA_ACTION_DTRACE:
- tesla_state_transition_dtrace(tcp, tip, transp, index);
+ tesla_state_transition_dtrace(tcp, tip, transp);
return;
default: {
- /* for the PRINTF action, should this be a non-verbose print? */
- assert(index >= 0);
- assert(index < transp->length);
- const struct tesla_transition *t = transp->transitions + index;
+ DEBUG(libtesla.state.transition, "update %td: %tx->%tx\n",
+ tip - tcp->tc_instances, transp->from, transp->to);
- VERBOSE_PRINT("update %td: %tx->%tx\n",
- tip - tcp->ts_table->tt_instances,
- t->from, t->to);
-
- if (t->flags & TESLA_TRANS_CLEANUP)
+ if (transp->flags & TESLA_TRANS_CLEANUP)
tesla_notify_pass(tcp, tip);
break;
@@ -127,7 +115,7 @@
assert(tcp != NULL);
assert(tip != NULL);
- if (tcp->ts_action == TESLA_ACTION_DTRACE) {
+ if (tcp->tc_action == TESLA_ACTION_DTRACE) {
tesla_assert_fail_dtrace(tcp, tip, transp);
return;
}
@@ -141,12 +129,13 @@
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);
+ (tip - tcp->tc_instances), tip->ti_state);
assert(next > buffer);
next = sprint_transitions(next, end, transp);
+ assert(next > buffer);
- switch (tcp->ts_action) {
+ switch (tcp->tc_action) {
case TESLA_ACTION_DTRACE:
assert(0 && "handled above");
return;
@@ -168,7 +157,7 @@
assert(tcp != NULL);
assert(tkp != NULL);
- if (tcp->ts_action == TESLA_ACTION_DTRACE) {
+ if (tcp->tc_action == TESLA_ACTION_DTRACE) {
tesla_assert_fail_dtrace(tcp, NULL, NULL);
return;
}
@@ -183,8 +172,9 @@
next = key_string(next, end, tkp);
SAFE_SPRINTF(next, end, "' for transition(s) ");
next = sprint_transitions(next, end, transp);
+ assert(next > buffer);
- switch (tcp->ts_action) {
+ switch (tcp->tc_action) {
case TESLA_ACTION_DTRACE:
assert(0 && "handled above");
break;
@@ -203,14 +193,15 @@
tesla_notify_pass(struct tesla_class *tcp, struct tesla_instance *tip)
{
- switch (tcp->ts_action) {
+ switch (tcp->tc_action) {
case TESLA_ACTION_DTRACE:
tesla_assert_pass_dtrace(tcp, tip);
return;
default:
- VERBOSE_PRINT("pass '%s': %td\n", tcp->ts_name,
- tip - tcp->ts_table->tt_instances);
+ DEBUG(libtesla.instance.success,
+ "pass '%s': %td\n", tcp->tc_name,
+ tip - tcp->tc_instances);
break;
}
}
@@ -225,6 +216,6 @@
kdb_backtrace();
#endif
- error("In automaton '%s':\n%s\n", tcp->ts_name, tcp->ts_description);
+ error("In automaton '%s':\n%s\n", tcp->tc_name, tcp->tc_description);
}
More information about the p4-projects
mailing list