Quick Guide to TESLA

What is the TESLA?

Temporal Logic

  if current_state == IEEE80211_S_ASSOC, then 
        previous_state == IEEE80211_S_AUTH and authentication was
        successful
      or
        previous_state == IEEE80211_S_RUN and DisAssoc frame is received

Building

Pre-requirements

Getting sources

In order to get all sources (llvm/clang, CFA, TESLA) run command:

> svn co https://socsvn.freebsd.org/socsvn/soc2011/shm/

You can also browse sources at https://socsvn.freebsd.org/socsvn/soc2011/shm/ .

clang/llvm

$ ./build_clang.sh

CFA - TEAL compiler

CFA sources are placed in cfa/ directory, building it is easy as:

> gmake
...
> ./splc --help
Usage: splc <options> input-file
  -O Optimisation level [0|1]
  -q Quiet mode
  -v Verbose mode
  -hdir HTML Template Directory [.]
  -d Debug mode [false]
  -t Output mode [tesla|ocaml|dot|promela]
  -s Filename for statecalls output (backend specific)
  -o Output file basename (without extension)
  -help  Display this list of options
  --help  Display this list of options

=== libtesla ==

libtesla sources are located in the TESLA/libtesla/ directory. library can be built using makefile.

Using TESLA

TEAL

automaton example()
{
  void main(struct test *x)
  {
    x->y = z;
    abc();
  }
}

Directory contains also a few examples of TEAL automata, it's at least worth to review them.

dhcp.spl tcp_connect.spl tcpc.spl

Instrumenter

Tesla instrumenter is a clang/llvm plugin used to analyze C code, it looks for tesla assertions and generate teal code, then instrument code basing on *.spec file which includes two types of declarations:

Script kernel/tesla-clang can be used to invoke plugin.

Simple example

         +------+
         |      |
         +---> P2---+   +---> P4 ---+
  P1 ----+          +---+           +--> P6
         +---> P3---+   +---> P5 ---+
         |      |
         +------+

TEAL automata

automaton simple_protocol() {
  void main(struct test *t) {
    t->state = P1;
    multiple {
      either {
        t->state = P2;
      } or {
        t->state = P3;
      }
    }
    either {
      t->state = P4;
    } or {
      t->state = P5;
    }
    t->state = P6;
    exit;
  }
}

> splc -t tesla -s example2 example2.spl
Input files: example2.spl
Processing example2.spl
Compiling function main (public) ... 
  19 states
Optimising CFA... 
  12 states eliminated
Input files: example2.spl
Output files: example2

Connecting automata with the code

   *.c + *.spec --[clang, instrumentation]--> instrumented code --+--> code guarded by TESLA
                             *.spl --[cfa]--> automata          --/

field_assign,struct test,state

> kernel/tesla-clang-print-ast example2.c instrumentation.spec
...
        int __tesla_tmp_assign;
        __tesla_tmp_assign = atoi(x[i]);
        __tesla_event_field_assign_struct_test_state(t, __tesla_tmp_assign);
        t->state = __tesla_tmp_assign;

...

        t->state = atoi(x[i]);

void
__tesla_event_field_assign_struct_test_state(struct test *t, u_int state)
{
    struct tesla_instance *tip;
    int alloc;
    int event;
    printf("-> %d\n", state);
    assert(tesla_instance_get1(example_state, (register_t)t, &tip, &alloc) ==
      0);

    if (alloc == 1)
        example2_automata_init(tip);

    switch(state)
    {
      case P1:
        event = EXAMPLE2_EVENT_T_STATE_ASSIGN_P1;
        break;
      case P2:
        event = EXAMPLE2_EVENT_T_STATE_ASSIGN_P2;
        break;
      case P3:
        event = EXAMPLE2_EVENT_T_STATE_ASSIGN_P3;
        break;
      case P4:
        event = EXAMPLE2_EVENT_T_STATE_ASSIGN_P4;
        break;
      case P5:
        event = EXAMPLE2_EVENT_T_STATE_ASSIGN_P5;
        break;
      case P6:
        event = EXAMPLE2_EVENT_T_STATE_ASSIGN_P6;
        break;
      default:
        printf("UNKNOWN STATE\n");
        tesla_assert_fail(example_state, tip);
    }

    if(example2_automata_prod(tip, event))
        tesla_assert_fail(example_state, tip);

    tesla_instance_put(example_state, tip);
}

$ gmake
../../kernel/tesla-clang -c -Wall -g -I../.. -I. -O0 -o example2_automata.o example2_automata.c
../../kernel/tesla-clang -c -Wall -g -I../.. -I. -O0 -o example2_assert.o example2_assert.c
../../kernel/tesla-clang -Wall -g -I../.. -I. -O0   -c -o example2.o example2.c
example2.c:31:9: warning: Adding TESLA instrumentation
        t->state = atoi(x[i]);
        ^~~~~~~~~~~~~~~~~~~~~
1 warning generated.
../../kernel/tesla-clang -o example2 example2_automata.o example2_assert.o example2.o ../../libtesla/tesla_state.o ../../libtesla/tesla_state_global.o ../../libtesla/tesla_state_perthread.o ../../libtesla/tesla_util.o

$ ./example2 1 2 2 3 4 6
-> 1
-> 2
-> 2
-> 3
-> 4
-> 6
Processed 6 states

$ ./example2 1 2 4 2
-> 1
-> 2
-> 4
-> 2
example2: tesla_assert failed: TEAL automata example: this is just a simple example

Further reading

ShmSoc2011QGTT (last edited 2011-07-14 17:24:01 by MateuszKocielski)