From owner-p4-projects@FreeBSD.ORG Thu May 30 07:46:31 2013 Return-Path: Delivered-To: p4-projects@freebsd.org Received: by hub.freebsd.org (Postfix, from userid 32767) id A8EA4DF6; Thu, 30 May 2013 07:46:31 +0000 (UTC) Delivered-To: perforce@freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by hub.freebsd.org (Postfix) with ESMTP id 68E74DF4 for ; Thu, 30 May 2013 07:46:31 +0000 (UTC) (envelope-from jonathan@freebsd.org) Received: from skunkworks.freebsd.org (skunkworks.freebsd.org [IPv6:2001:1900:2254:2068::682:0]) by mx1.freebsd.org (Postfix) with ESMTP id 4A15983A for ; Thu, 30 May 2013 07:46:31 +0000 (UTC) Received: from skunkworks.freebsd.org ([127.0.1.74]) by skunkworks.freebsd.org (8.14.6/8.14.6) with ESMTP id r4U7kV1T080601 for ; Thu, 30 May 2013 07:46:31 GMT (envelope-from jonathan@freebsd.org) Received: (from perforce@localhost) by skunkworks.freebsd.org (8.14.6/8.14.6/Submit) id r4U7kVaT080598 for perforce@freebsd.org; Thu, 30 May 2013 07:46:31 GMT (envelope-from jonathan@freebsd.org) Date: Thu, 30 May 2013 07:46:31 GMT Message-Id: <201305300746.r4U7kVaT080598@skunkworks.freebsd.org> X-Authentication-Warning: skunkworks.freebsd.org: perforce set sender to jonathan@freebsd.org using -f From: Jonathan Anderson Subject: PERFORCE change 229141 for review To: Perforce Change Reviews Precedence: bulk X-BeenThere: p4-projects@freebsd.org X-Mailman-Version: 2.1.14 List-Id: p4 projects tree changes List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 30 May 2013 07:46:31 -0000 http://p4web.freebsd.org/@@229141?ac=10 Change 229141 by jonathan@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 - ==== //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 if 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 @@ -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 -#define DEBUG_PRINT(...) print(__VA_ARGS__) #else #include -#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); }