socsvn commit: r224224 - in soc2011/shm: TESLA TESLA/assertions/80211 TESLA/libtesla TESLA/tesla sys/amd64/conf sys/conf sys/tesla/assert

shm at FreeBSD.org shm at FreeBSD.org
Thu Jul 14 17:20:29 UTC 2011


Author: shm
Date: Thu Jul 14 17:20:27 2011
New Revision: 224224
URL: http://svnweb.FreeBSD.org/socsvn/?view=rev&rev=224224

Log:
   * the great merge (merged from g-soc)

Added:
  soc2011/shm/TESLA/assertions/80211/
  soc2011/shm/TESLA/assertions/80211/80211proto.spec
  soc2011/shm/TESLA/assertions/80211/80211proto.spl
  soc2011/shm/TESLA/assertions/80211/80211proto_assert.c
  soc2011/shm/TESLA/assertions/80211/80211proto_automata.c
  soc2011/shm/TESLA/assertions/80211/80211proto_defs.h
  soc2011/shm/TESLA/assertions/80211/instrumentation.spec
  soc2011/shm/TESLA/build_tesla.sh   (contents, props changed)
  soc2011/shm/sys/amd64/conf/TESLA_80211PROTO
  soc2011/shm/sys/amd64/conf/TESLA_MAC
  soc2011/shm/sys/tesla/assert/
  soc2011/shm/sys/tesla/assert/80211proto   (contents, props changed)
Deleted:
  soc2011/shm/TESLA/README.txt
  soc2011/shm/sys/amd64/conf/majestic
Modified:
  soc2011/shm/TESLA/libtesla/tesla_state.c
  soc2011/shm/TESLA/libtesla/tesla_state_global.c
  soc2011/shm/TESLA/tesla/tesla_state.h
  soc2011/shm/TESLA/tesla/tesla_util.h
  soc2011/shm/sys/conf/files
  soc2011/shm/sys/conf/options

Added: soc2011/shm/TESLA/assertions/80211/80211proto.spec
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/80211/80211proto.spec	Thu Jul 14 17:20:27 2011	(r224224)
@@ -0,0 +1,10 @@
+field_assign,v,iv_nstate,IEEE80211_S_ASSOC
+field_assign,v,iv_nstate,IEEE80211_S_ASSOC
+field_assign,v,iv_nstate,IEEE80211_S_AUTH
+field_assign,v,iv_nstate,IEEE80211_S_SCAN
+field_assign,v,iv_nstate,IEEE80211_S_AUTH
+field_assign,v,iv_nstate,IEEE80211_S_SCAN
+field_assign,v,iv_nstate,IEEE80211_S_CSA
+field_assign,v,iv_nstate,IEEE80211_S_SLEEP
+field_assign,v,iv_nstate,IEEE80211_S_RUN
+field_assign,v,iv_nstate,IEEE80211_S_INIT

Added: soc2011/shm/TESLA/assertions/80211/80211proto.spl
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/80211/80211proto.spl	Thu Jul 14 17:20:27 2011	(r224224)
@@ -0,0 +1,31 @@
+/* experimental */
+automaton ieee80211proto() {
+  void main(struct ieee80211vap *v) {
+    v->iv_nstate = IEEE80211_S_INIT;
+    multiple {
+      v->iv_nstate = IEEE80211_S_RUN;
+      either {
+        v->iv_nstate = IEEE80211_S_SLEEP;
+      } or {
+        v->iv_nstate = IEEE80211_S_CSA;
+      } or {
+        v->iv_nstate = IEEE80211_S_SCAN;
+      } or {
+        v->iv_nstate = IEEE80211_S_AUTH;
+      } or {
+        multiple {
+          either {
+            v->iv_nstate = IEEE80211_S_SCAN;
+          } or {
+            v->iv_nstate = IEEE80211_S_AUTH;
+            optional {
+              v->iv_nstate = IEEE80211_S_ASSOC;
+            }
+          }
+        }
+      } or {
+        v->iv_nstate = IEEE80211_S_ASSOC;
+      }
+    }
+  }
+}

Added: soc2011/shm/TESLA/assertions/80211/80211proto_assert.c
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/80211/80211proto_assert.c	Thu Jul 14 17:20:27 2011	(r224224)
@@ -0,0 +1,56 @@
+/*
+ * Copyright (c) 2011, Mateusz Kocielski <shm at FreeBSD.org>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ * 
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ */
+
+#include <tesla/tesla_state.h>
+#include <tesla/tesla_util.h>
+#include "80211_defs.h"
+
+static struct tesla_state *80211_state;
+
+#define 80211_PROTO_LIMIT 23
+#define 80211_PROTO_NAME "802.11 proto"
+#define 80211_PROTO_DESC \
+  "checks if state transitions is not violating 802.11 proto"
+
+void
+80211_init(int scope)
+{
+    assert(tesla_state_new(&80211_state, scope, 80211_PROTO_LIMIT, 80211_PROTO_NAME,
+      80211_PROTO_DESC) == 0);
+}
+ 
+void __tesla_event_function_prologue_80211_new_state(void **t, void *x, int
+event, int z)
+{
+    struct tesla_instance *tip;
+    int alloc;
+    int e
+    
+    KASSERT(tesla_instance_get1(80211_state, (register_t)x, &tip, &alloc) ==
+      0);
+
+    switch
+
+    if (alloc == 1)
+        80211proto_automata_init(tip);
+
+    if(80211proto_automata_prod(tip, event))
+        tesla_assert_fail(80211_state, tip);
+
+    tesla_instance_put(80211_state, tip);
+}
+
+void __tesla_event_function_return_80211_new_state(void **t) {}

Added: soc2011/shm/TESLA/assertions/80211/80211proto_automata.c
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/80211/80211proto_automata.c	Thu Jul 14 17:20:27 2011	(r224224)
@@ -0,0 +1,296 @@
+/*
+ * This file is autogenerated by the Tesla CFA compiler
+ * via: ../../cfa/splc -t tesla -s 80211proto 80211proto.spl
+ */
+
+
+#include <sys/types.h>
+
+#ifdef _KERNEL
+#include <sys/systm.h>
+#else
+#include <assert.h>
+#include <stdlib.h>
+#include <stdint.h>
+#include <string.h>
+#endif
+
+#include <tesla/tesla_state.h>
+#include <tesla/tesla_util.h>
+
+#include "80211proto_defs.h"
+
+struct main {
+  u_int state : 4;
+} __attribute__((__packed__));
+
+#define MAIN_PTR(tip) ((unsigned char *)((tip)->ti_state))
+#define MAIN_STATE(tip,off) ((struct main *)(MAIN_PTR(tip)+(off)+1))
+#define MAIN_NUM_STATES(tip) (MAIN_PTR(tip)[0])
+
+void
+80211proto_automata_init(struct tesla_instance *tip) {
+  MAIN_NUM_STATES(tip) = 1;
+  MAIN_STATE(tip,0)->state = 2; /* 1 */
+}
+
+int
+80211proto_automata_prod(struct tesla_instance *tip, u_int event)
+{
+  unsigned char newstate[16];
+  u_int i, curpos=1;
+  struct main tmpstate;
+  bzero(newstate, sizeof(newstate));
+  switch (event) {
+  case 0:  /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_AUTH */
+    for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+      switch (MAIN_STATE(tip,i)->state) {
+      case 8:
+        /* event 30 -> 2 */
+        tmpstate.state = 3;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 30 -> 5 */
+        tmpstate.state = 5;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 30 -> 28 */
+        tmpstate.state = 1;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 30 -> 30 */
+        tmpstate.state = 8;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 30 -> 32 */
+        tmpstate.state = 10;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        break;
+      case 9:
+        /* event 18 -> 2 */
+        tmpstate.state = 3;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 18 -> 5 */
+        tmpstate.state = 5;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        break;
+      default:
+        break;
+      }
+    }
+    newstate[0] = curpos-1;
+    if (newstate[0] == 0)
+      return 1; /* TESLA_ERROR */
+    memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+    return 0;
+
+  case 1:  /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_RUN */
+    for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+      switch (MAIN_STATE(tip,i)->state) {
+      case 5:
+        /* event 5 -> 2 */
+        tmpstate.state = 3;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 5 -> 5 */
+        tmpstate.state = 5;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 5 -> 28 */
+        tmpstate.state = 1;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 5 -> 30 */
+        tmpstate.state = 8;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 5 -> 12 */
+        tmpstate.state = 4;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 5 -> 14 */
+        tmpstate.state = 6;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 5 -> 16 */
+        tmpstate.state = 7;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 5 -> 18 */
+        tmpstate.state = 9;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 5 -> 35 */
+        tmpstate.state = 11;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        break;
+      default:
+        break;
+      }
+    }
+    newstate[0] = curpos-1;
+    if (newstate[0] == 0)
+      return 1; /* TESLA_ERROR */
+    memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+    return 0;
+
+  case 2:  /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_CSA */
+    for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+      switch (MAIN_STATE(tip,i)->state) {
+      case 6:
+        /* event 14 -> 2 */
+        tmpstate.state = 3;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 14 -> 5 */
+        tmpstate.state = 5;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        break;
+      default:
+        break;
+      }
+    }
+    newstate[0] = curpos-1;
+    if (newstate[0] == 0)
+      return 1; /* TESLA_ERROR */
+    memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+    return 0;
+
+  case 3:  /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_SLEEP */
+    for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+      switch (MAIN_STATE(tip,i)->state) {
+      case 4:
+        /* event 12 -> 2 */
+        tmpstate.state = 3;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 12 -> 5 */
+        tmpstate.state = 5;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        break;
+      default:
+        break;
+      }
+    }
+    newstate[0] = curpos-1;
+    if (newstate[0] == 0)
+      return 1; /* TESLA_ERROR */
+    memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+    return 0;
+
+  case 4:  /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_SCAN */
+    for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+      switch (MAIN_STATE(tip,i)->state) {
+      case 1:
+        /* event 28 -> 2 */
+        tmpstate.state = 3;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 28 -> 5 */
+        tmpstate.state = 5;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 28 -> 28 */
+        tmpstate.state = 1;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 28 -> 30 */
+        tmpstate.state = 8;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        break;
+      case 7:
+        /* event 16 -> 2 */
+        tmpstate.state = 3;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 16 -> 5 */
+        tmpstate.state = 5;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        break;
+      default:
+        break;
+      }
+    }
+    newstate[0] = curpos-1;
+    if (newstate[0] == 0)
+      return 1; /* TESLA_ERROR */
+    memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+    return 0;
+
+  case 5:  /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_ASSOC */
+    for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+      switch (MAIN_STATE(tip,i)->state) {
+      case 10:
+        /* event 32 -> 2 */
+        tmpstate.state = 3;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 32 -> 5 */
+        tmpstate.state = 5;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 32 -> 28 */
+        tmpstate.state = 1;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 32 -> 30 */
+        tmpstate.state = 8;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        break;
+      case 11:
+        /* event 35 -> 2 */
+        tmpstate.state = 3;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 35 -> 5 */
+        tmpstate.state = 5;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        break;
+      default:
+        break;
+      }
+    }
+    newstate[0] = curpos-1;
+    if (newstate[0] == 0)
+      return 1; /* TESLA_ERROR */
+    memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+    return 0;
+
+  case 6:  /* EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_INIT */
+    for (i=0; i < MAIN_NUM_STATES(tip); i++) {
+      switch (MAIN_STATE(tip,i)->state) {
+      case 2:
+        /* event 1 -> 2 */
+        tmpstate.state = 3;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        /* event 1 -> 5 */
+        tmpstate.state = 5;
+        memcpy(&(newstate[curpos]), &tmpstate, 1);
+        curpos++;
+        break;
+      default:
+        break;
+      }
+    }
+    newstate[0] = curpos-1;
+    if (newstate[0] == 0)
+      return 1; /* TESLA_ERROR */
+    memcpy(MAIN_PTR(tip), &newstate, sizeof(newstate));
+    return 0;
+
+  default:
+    return 1; /* TESLA_UNKNOWN_EVENT */
+  }
+}
+

Added: soc2011/shm/TESLA/assertions/80211/80211proto_defs.h
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/80211/80211proto_defs.h	Thu Jul 14 17:20:27 2011	(r224224)
@@ -0,0 +1,38 @@
+/*
+ * This file is autogenerated by the Tesla CFA compiler
+ * via: ../../cfa/splc -t tesla -s 80211proto 80211proto.spl
+ */
+
+#ifndef 80211PROTO_DEFS_H
+#define 80211PROTO_DEFS_H
+
+#include <sys/types.h>
+
+/*
+ * Names for events that will trigger 80211PROTO rules
+ */
+#define 80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_AUTH 0
+#define 80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_RUN 1
+#define 80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_CSA 2
+#define 80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_SLEEP 3
+#define 80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_SCAN 4
+#define 80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_ASSOC 5
+#define 80211PROTO_EVENT_V_IV_NSTATE_ASSIGN_IEEE80211_S_INIT 6
+
+/*
+ * Prod the 80211PROTO state machine, return (1) if the assertion failed
+ */
+struct tesla_instance;
+void 80211proto_automata_init(struct tesla_instance *);
+int 80211proto_automata_prod(struct tesla_instance *tip, u_int event);
+
+/*
+ * "Public" interfaces to the assertion, to be invoked by load, unload
+ * and instrumentation handlers.
+ */
+#ifndef _KERNEL
+void	80211proto_init(int scope);
+void	80211proto_destroy(void);
+void    80211proto_setaction_debug(void);
+#endif
+#endif /* 80211PROTO_DEFS_H */

Added: soc2011/shm/TESLA/assertions/80211/instrumentation.spec
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ soc2011/shm/TESLA/assertions/80211/instrumentation.spec	Thu Jul 14 17:20:27 2011	(r224224)
@@ -0,0 +1 @@
+function,ieee80211_new_state

Added: soc2011/shm/TESLA/build_tesla.sh
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ soc2011/shm/TESLA/build_tesla.sh	Thu Jul 14 17:20:27 2011	(r224224)
@@ -0,0 +1,16 @@
+#!/bin/sh
+
+echo "Building llvm/clang..."
+if [ ! -d llvm ]; then
+    ./build_clang.sh
+fi
+
+echo "Building CFA..."
+cd cfa/
+gmake
+cd ..
+
+echo "Building libtesla..."
+cd libtesla/
+make
+cd ..

Modified: soc2011/shm/TESLA/libtesla/tesla_state.c
==============================================================================
--- soc2011/shm/TESLA/libtesla/tesla_state.c	Thu Jul 14 15:35:43 2011	(r224223)
+++ soc2011/shm/TESLA/libtesla/tesla_state.c	Thu Jul 14 17:20:27 2011	(r224224)
@@ -58,6 +58,34 @@
 MALLOC_DEFINE(M_TESLA, "tesla", "TESLA internal state");
 #endif
 
+/* XXX: should be replaced with something better i.e. R-M test */
+static int
+tesla_is_prime(u_int n)
+{
+  u_int i;
+  
+  if (n < 2)
+    return 0;
+  
+  for (i = 2; i < n; i++)
+    if (n % i == 0)
+      return 0;
+
+  return 1;
+}
+
+static u_int
+tesla_nearest_prime(u_int n)
+{
+  u_int i;
+
+  for (i = n ; i >= n ; i++)
+    if (tesla_is_prime(i) == 1)
+      return i;
+
+  return 0;
+}
+
 int
 tesla_state_new(struct tesla_state **tspp, u_int scope, u_int limit,
     const char *name, const char *description)
@@ -68,18 +96,27 @@
 
 #ifdef _KERNEL
 	KASSERT((scope == TESLA_SCOPE_PERTHREAD) ||
-	    (scope == TESLA_SCOPE_GLOBAL),
-	    ("tesla_state_new: invalid scope %u", scope));
+	  (scope == TESLA_SCOPE_GLOBAL),
+	  ("tesla_state_new: invalid scope %u", scope));
 #else
 	assert(scope == TESLA_SCOPE_PERTHREAD || scope == TESLA_SCOPE_GLOBAL);
 #endif
 
-	/* XXXRW: Should validate 'limit' argument. */
+  limit = tesla_nearest_prime(limit);
+
+  if (limit == 0)
+    return (TESLA_ERROR_ELIMIT);  
 
 	if (scope == TESLA_SCOPE_PERTHREAD)
 		len = sizeof(*tsp);
 	else
+  {
 		len = sizeof(*tsp) + sizeof(struct tesla_instance) * limit;
+    /* overflow occured */
+    if (len < sizeof(struct tesla_instance) * limit ||
+      sizeof(struct tesla_instance) * limit < limit)
+       return (TESLA_ERROR_ELIMIT);
+  }
 
 #ifdef _KERNEL
 	tsp = malloc(len, M_TESLA, M_WAITOK | M_ZERO);
@@ -100,18 +137,20 @@
 	tsp->ts_action = TESLA_ACTION_FAILSTOP;	/* XXXRW: Default for now? */
 #endif
 
-	if (scope == TESLA_SCOPE_PERTHREAD) {
+	if (scope == TESLA_SCOPE_PERTHREAD)
 		error = tesla_state_perthread_new(tsp);
-		if (error != TESLA_SUCCESS) {
+	else
+		error = tesla_state_global_new(tsp);
+
+  if (error != TESLA_SUCCESS) {
 #ifdef _KERNEL
-			free(tsp, M_TESLA);
+	  free(tsp, M_TESLA);
 #else
-			free(tsp);
+	  free(tsp);
 #endif
-			return (error);
-		}
-	} else
-		tesla_state_global_new(tsp);
+	  return (error);
+	}
+
 	*tspp = tsp;
 	return (TESLA_SUCCESS);
 }
@@ -147,7 +186,7 @@
 {
 	struct tesla_instance *tip, *free_tip;
 	struct tesla_table *ttp;
-	u_int i;
+	u_int i, key;
 	int error;
 
 	if (tsp->ts_scope == TESLA_SCOPE_GLOBAL) {
@@ -158,11 +197,14 @@
 		if (error != TESLA_SUCCESS)
 			return (error);
 	}
+    
+  /* XXX: quick hack to speed up looking for instance */
+  key = (key0 + key1 + key2 + key3)  % tsp->ts_limit;
 
 	/* XXXRW: Absolutely the wrong algorithm. */
 	free_tip = NULL;
 	for (i = 0; i < ttp->tt_length; i++) {
-		tip = &ttp->tt_instances[i];
+		tip = &ttp->tt_instances[(i+key) % tsp->ts_limit];
 		if (free_tip == NULL &&
 		    tip->ti_keys[0] == 0 &&
 		    tip->ti_keys[1] == 0 &&
@@ -174,11 +216,13 @@
 		    tip->ti_keys[2] != key2 ||
 		    tip->ti_keys[3] != key3)
 			continue;
+    /* Found instance */
 		if (alloc != NULL)
 			*alloc = 0;
 		*tipp = tip;
 		return (TESLA_SUCCESS);
 	}
+
 	if (free_tip != NULL) {
 		tip = free_tip;
 		tip->ti_keys[0] = key0;
@@ -192,6 +236,7 @@
 			*alloc = 1;
 		return (TESLA_SUCCESS);
 	}
+
 	if (tsp->ts_scope == TESLA_SCOPE_GLOBAL) {
 		tesla_state_global_unlock(tsp);
 	}
@@ -258,20 +303,17 @@
 	/* No action required for TESLA_SCOPE_PERTHREAD. */
 }
 
-void
+int
 tesla_instance_destroy(struct tesla_state *tsp, struct tesla_instance *tip)
 {
 	struct tesla_table *ttp;
 	int error;
 
-	tip->ti_state[0] = 0;
-	tip->ti_state[1] = 0;
-	tip->ti_state[2] = 0;
-	tip->ti_state[3] = 0;
-	tip->ti_keys[0] = 0;
-	tip->ti_keys[1] = 0;
-	tip->ti_keys[2] = 0;
-	tip->ti_keys[3] = 0;
+  /* XXX: 0 is used to indicate that instance is free */
+	tip->ti_state[0] = tip->ti_state[1] = tip->ti_state[2] =
+    tip->ti_state[3] = 0;
+	tip->ti_keys[0] = tip->ti_keys[1] = tip->ti_keys[2] = 
+    tip->ti_keys[3] = 0;
 
 	/*
 	 * XXXRW: this will need revisiting if we change locking strategies.
@@ -282,9 +324,11 @@
 	} else  {
 		error = tesla_state_perthread_gettable(tsp, &ttp);
 		if (error != TESLA_SUCCESS)
-			return;
+			return error;
 		ttp->tt_free++;
 	}
+
+  return (TESLA_SUCCESS);
 }
 
 void
@@ -325,6 +369,5 @@
 tesla_state_setaction(struct tesla_state *tsp,
     tesla_assert_fail_callback handler)
 {
-
 	tsp->ts_handler = handler;
 }

Modified: soc2011/shm/TESLA/libtesla/tesla_state_global.c
==============================================================================
--- soc2011/shm/TESLA/libtesla/tesla_state_global.c	Thu Jul 14 15:35:43 2011	(r224223)
+++ soc2011/shm/TESLA/libtesla/tesla_state_global.c	Thu Jul 14 17:20:27 2011	(r224224)
@@ -62,8 +62,7 @@
 #ifdef _KERNEL
 	mtx_init(&tsp->ts_lock, "tesla", NULL, MTX_DEF);
 #else
-	int error = pthread_mutex_init(&tsp->ts_lock, NULL);
-	assert(error == 0);
+  assert(pthread_mutex_init(&tsp->ts_lock, NULL) == 0);
 #endif
 }
 
@@ -74,8 +73,7 @@
 #ifdef _KERNEL
 	mtx_destroy(&tsp->ts_lock);
 #else
-	int error = pthread_mutex_destroy(&tsp->ts_lock);
-	assert(error == 0);
+	assert(pthread_mutex_destroy(&tsp->ts_lock) == 0);
 #endif
 }
 
@@ -86,8 +84,7 @@
 #ifdef _KERNEL
 	mtx_lock(&tsp->ts_lock);
 #else
-	int error = pthread_mutex_lock(&tsp->ts_lock);
-	assert(error == 0);
+  assert(pthread_mutex_lock(&tsp->ts_lock) == 0);
 #endif
 }
 
@@ -98,8 +95,7 @@
 #ifdef _KERNEL
 	mtx_unlock(&tsp->ts_lock);
 #else
-	int error = pthread_mutex_unlock(&tsp->ts_lock);
-	assert(error == 0);
+  assert(pthread_mutex_unlock(&tsp->ts_lock) == 0);
 #endif
 }
 

Modified: soc2011/shm/TESLA/tesla/tesla_state.h
==============================================================================
--- soc2011/shm/TESLA/tesla/tesla_state.h	Thu Jul 14 15:35:43 2011	(r224223)
+++ soc2011/shm/TESLA/tesla/tesla_state.h	Thu Jul 14 17:20:27 2011	(r224224)
@@ -154,7 +154,7 @@
  * particular tesla_state.  An instance passed to tesla_instance_destroy()
  * will not require a call to tesla_instance_put().
  */
-void	tesla_instance_destroy(struct tesla_state *tsp,
+int 	tesla_instance_destroy(struct tesla_state *tsp,
 	    struct tesla_instance *tip);
 
 /*

Modified: soc2011/shm/TESLA/tesla/tesla_util.h
==============================================================================
--- soc2011/shm/TESLA/tesla/tesla_util.h	Thu Jul 14 15:35:43 2011	(r224223)
+++ soc2011/shm/TESLA/tesla/tesla_util.h	Thu Jul 14 17:20:27 2011	(r224224)
@@ -44,6 +44,7 @@
 #define	TESLA_ERROR_ENOENT	1	/* Entry not found. */
 #define	TESLA_ERROR_EEXIST	2	/* Entry already present. */
 #define	TESLA_ERROR_ENOMEM	3	/* Insufficient memory. */
+#define TESLA_ERROR_ELIMIT  4 /* Invalid limit value */
 
 /*
  * Provide string versions of TESLA errors.

Added: soc2011/shm/sys/amd64/conf/TESLA_80211PROTO
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ soc2011/shm/sys/amd64/conf/TESLA_80211PROTO	Thu Jul 14 17:20:27 2011	(r224224)
@@ -0,0 +1,4 @@
+include TESLA
+ident TESLA_80211PROTO
+
+options TESLA_80211PROTO

Added: soc2011/shm/sys/amd64/conf/TESLA_MAC
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ soc2011/shm/sys/amd64/conf/TESLA_MAC	Thu Jul 14 17:20:27 2011	(r224224)
@@ -0,0 +1,4 @@
+include TESLA
+ident TESLA_MAC2
+
+options TESLA_MAC2

Modified: soc2011/shm/sys/conf/files
==============================================================================
--- soc2011/shm/sys/conf/files	Thu Jul 14 15:35:43 2011	(r224223)
+++ soc2011/shm/sys/conf/files	Thu Jul 14 17:20:27 2011	(r224224)
@@ -2950,3 +2950,5 @@
 tesla/tesla_state_global.c     optional tesla
 tesla/tesla_state_perthread.c  optional tesla
 tesla/tesla_util.c             optional tesla
+tesla/assert/80211proto/80211proto_assert.c optional tesla_80211proto
+tesla/assert/80211proto/80211proto_automata.c optional tesla_80211proto

Modified: soc2011/shm/sys/conf/options
==============================================================================
--- soc2011/shm/sys/conf/options	Thu Jul 14 15:35:43 2011	(r224223)
+++ soc2011/shm/sys/conf/options	Thu Jul 14 17:20:27 2011	(r224224)
@@ -573,6 +573,7 @@
 SX_NOINLINE		opt_global.h
 VFS_BIO_DEBUG		opt_global.h
 TESLA   opt_global.h
+TESLA_80211PROTO opt_global.h
 
 # These are VM related options
 VM_KMEM_SIZE		opt_vm.h

Added: soc2011/shm/sys/tesla/assert/80211proto
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ soc2011/shm/sys/tesla/assert/80211proto	Thu Jul 14 17:20:27 2011	(r224224)
@@ -0,0 +1 @@
+link /home/shm/tesla/shm/TESLA/assertions/80211/
\ No newline at end of file


More information about the svn-soc-all mailing list