• bearophile (36/36) Dec 16 2011 Second interesting thing I've found from the 2011 LLVM Developer Meeting...

bearophile <bearophileHUGS lycos.com> writes:

Second interesting thing I've found from the 2011 LLVM Developer Meeting:
http://www.youtube.com/playlist?list=PL970A5BD02C11F80C
Slides:
http://llvm.org/devmtg/2011-11/


In the "Integrating LLVM into FreeBSD" talk I have seen a reference to TESLA
(the talk itself is not interesting). It's not so easy to find good info about
TESLA, I have found this little tutorial:
http://wiki.freebsd.org/ShmSoc2011QGTT

And two examples:
https://socsvn.freebsd.org/socsvn/soc2011/shm/TESLA/examples/example2/
https://socsvn.freebsd.org/socsvn/soc2011/shm/TESLA/examples/ping/


From the page:

What is the TESLA?
TESLA is a framework for testing temporal properties of a software written in
the C language. Standard assertions i.e. assert(3) are able to test simple
expressions which refer only to an actual state of a program, testing temporal
properties in this case (e.g. conformance with the protocols, condition checks
before usage etc.) is complex, requires additional code and data structures,
thus it could be a source of unnecessary complexity and bugs. TESLA introduces
assertions which test temporal expressions, it means that it's able to refer to
the future and to the past, which is a great help when a goal is to verify some
property which refers to the time, i.e. check if access control checks were
done. 


You write a simple automata like this using temporal logic:


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;
  }
}


And the TESLA tool adds asserts (and small functions that contain asserts) to
your C code that enforce those temporal constraints.

It seems nice, its purpose seems similar to the typestates of the Rust
language, but this works on C programs.

Bye,
bearophile