tesla_internal.h

Go to the documentation of this file.

/*-
 * Copyright (c) 2011, 2013 Robert N. M. Watson
 * All rights reserved.
 *
 * This software was developed by SRI International and the University of
 * Cambridge Computer Laboratory under DARPA/AFRL contract (FA8750-10-C-0237)
 * ("CTSRD"), as part of the DARPA CRASH research programme.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions
 * are met:
 * 1. Redistributions of source code must retain the above copyright
 *    notice, this list of conditions and the following disclaimer.
 * 2. Redistributions in binary form must reproduce the above copyright
 *    notice, this list of conditions and the following disclaimer in the
 *    documentation and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
 * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
 * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
 * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
 * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
 * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
 * SUCH DAMAGE.
 *
 * $Id$
 */

#ifndef TESLA_INTERNAL_H
#define TESLA_INTERNAL_H

#ifdef HAVE_CONFIG_H
#include "config.h"
#endif

#ifdef _KERNEL
#include "opt_kdb.h"
#include "opt_kdtrace.h"
#include <sys/param.h>
#include <sys/eventhandler.h>
#include <sys/kdb.h>
#include <sys/kernel.h>
#include <sys/lock.h>
#include <sys/mutex.h>
#include <sys/malloc.h>
#include <sys/proc.h>
#include <sys/sx.h>
#include <sys/systm.h>

#include <machine/_inttypes.h>
#else
#include <assert.h>
#include <err.h>
#include <pthread.h>
#include <stdlib.h>
#include <string.h>
#endif

#include <libtesla.h>

#define SUBSET(x,y) ((x & y) == x)

void    tesla_die(int32_t errno, const char *event) __attribute__((noreturn));

int32_t tesla_store_reset(struct tesla_store *store);

void    tesla_store_free(struct tesla_store*);


void    tesla_class_reset(struct tesla_class*);

void    tesla_class_destroy(struct tesla_class*);


int32_t tesla_instance_new(struct tesla_class *tclass,
            const struct tesla_key *name, uint32_t state,
            struct tesla_instance **out);

int32_t tesla_instance_active(const struct tesla_instance *i);


int32_t tesla_instance_clone(struct tesla_class *tclass,
            const struct tesla_instance *orig, struct tesla_instance **copy);

void    tesla_instance_clear(struct tesla_instance *tip);


int32_t tesla_match(struct tesla_class *tclass, const struct tesla_key *key,
            struct tesla_instance **array, uint32_t *size);

int32_t tesla_key_matches(
            const struct tesla_key *pattern, const struct tesla_key *k);


enum tesla_action_t {
        UPDATE,

        FORK,

        JOIN,

        IGNORE,

        FAIL
};

enum tesla_action_t     tesla_action(const struct tesla_instance*,
            const struct tesla_key*, const struct tesla_transitions*,
            const struct tesla_transition** trigger);

int32_t tesla_key_union(struct tesla_key *dest, const struct tesla_key *source);


#ifndef __unused
#if __has_attribute(unused)
#define __unused __attribute__((unused))
#else
#define __unused
#endif
#endif

// Kernel vs userspace implementation details.
#ifdef _KERNEL

#define tesla_panic(...) panic(__VA_ARGS__)

#define tesla_assert(...) KASSERT(__VA_ARGS__)

#define assert(cond) KASSERT((cond), ("Assertion failed: '%s'", #cond))

#define tesla_malloc(len) malloc(len, M_TESLA, M_WAITOK | M_ZERO)
#define tesla_free(x) free(x, M_TESLA)

#define tesla_lock(l) mtx_lock(l)
#define tesla_unlock(l) mtx_unlock(l)

#else   /* !_KERNEL */

#define tesla_panic(...) errx(1, __VA_ARGS__)

#define tesla_assert(condition, ...) assert(condition)

#define tesla_malloc(len) calloc(1, len)
#define tesla_free(x) free(x)

#define tesla_lock(l) \
        do { __debug int err = pthread_mutex_lock(l); assert(err == 0); } while(0)

#define tesla_unlock(l) \
        do { __debug int err = pthread_mutex_unlock(l); assert(err == 0); } while(0)

#endif


/*
 * Assertion state definition is internal to libtesla so we can change it as
 * we need to.
 */
struct tesla_class {
        const char              *tc_name;       /* Name of the assertion. */
        const char              *tc_description;/* Automaton representation. */
        enum tesla_context       tc_context;    /* Global, thread... */
        uint32_t                 tc_limit;      /* Maximum instances. */

        struct tesla_instance   *tc_instances;  /* Instances of this class. */
        uint32_t                tc_free;        /* Unused instances. */

#ifdef _KERNEL
        struct mtx              tc_lock;        /* Synchronise tc_table. */
#else
        pthread_mutex_t          tc_lock;       /* Synchronise tc_table. */
#endif
};

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_transition         tesla_transition;
typedef struct tesla_transitions        tesla_transitions;


struct tesla_store {
        uint32_t                length;
        struct tesla_class      *classes;
};

int     tesla_store_init(tesla_store*, enum tesla_context context,
                uint32_t classes, uint32_t instances);

int     tesla_class_init(struct tesla_class*, enum tesla_context context,
                uint32_t instances);

/*
 * XXXRW: temporarily, maximum number of classes and instances are hard-coded
 * constants.  In the future, this should somehow be more dynamic.
 */
#define TESLA_MAX_CLASSES               128
#define TESLA_MAX_INSTANCES             128

#if defined(_KERNEL) && defined(MALLOC_DECLARE)
/*
 * Memory type for TESLA allocations in the kernel.
 */
MALLOC_DECLARE(M_TESLA);
#endif

/*
 * Context-specific automata management:
 */
int32_t tesla_class_global_postinit(struct tesla_class*);
void    tesla_class_global_acquire(struct tesla_class*);
void    tesla_class_global_release(struct tesla_class*);
void    tesla_class_global_destroy(struct tesla_class*);

int32_t tesla_class_perthread_postinit(struct tesla_class*);
void    tesla_class_perthread_acquire(struct tesla_class*);
void    tesla_class_perthread_release(struct tesla_class*);
void    tesla_class_perthread_destroy(struct tesla_class*);

/*
 * Event notification:
 */
#if defined(_KERNEL) && defined(KDTRACE_HOOKS)
extern const struct tesla_event_handlers dtrace_handlers;
#endif

void    ev_new_instance(struct tesla_class *, struct tesla_instance *);
void    ev_transition(struct tesla_class *, struct tesla_instance *,
            const struct tesla_transition*);
void    ev_clone(struct tesla_class *, struct tesla_instance *orig,
            struct tesla_instance *copy, const struct tesla_transition *);
void    ev_no_instance(struct tesla_class *, const struct tesla_key *,
            const struct tesla_transitions *);
void    ev_bad_transition(struct tesla_class *, struct tesla_instance *,
            const struct tesla_transitions *);
void    ev_err(struct tesla_class *tcp, int errno, const char *message);
void    ev_accept(struct tesla_class *, struct tesla_instance *);
void    ev_ignored(const struct tesla_class *, const struct tesla_key *,
            const struct tesla_transitions *);

/*
 * 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>
#else
#include <stdio.h>
#endif

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(...)
int32_t tesla_debugging(const char*) { return 0; }

#endif

void    assert_instanceof(struct tesla_instance *i, struct tesla_class *tclass);

char*   key_string(char *buffer, const char *end, const struct tesla_key *);

void    print_key(const char *debug_name, const struct tesla_key *key);

void    print_class(const struct tesla_class*);

void    print_transition(const char *debug, const struct tesla_transition *);

char*   sprint_transition(char *buffer, const char *end,
    const struct tesla_transition *);

void    print_transitions(const char *debug, const struct tesla_transitions *);

char*   sprint_transitions(char *buffer, const char *end,
    const struct tesla_transitions *);

#endif /* TESLA_INTERNAL_H */