LLVM talks 2: TESLA

[bearophile]

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