API for programmers who want to use TESLA in their code.
Classes | |
struct | __tesla_event |
The basic TESLA type is a pointer to a TESLA Basic TESLA types (magic for the compiler to munge). More... | |
struct | __tesla_locality |
Macros | |
#define | TESLA_WITHIN(function, expression) |
An assertion made within the execution of a particular function. More... | |
#define | TESLA_ASSERT(locality, start, end, expression) |
An inline assertion. More... | |
#define | TESLA_GLOBAL(...) TESLA_ASSERT(__tesla_global, __VA_ARGS__) |
An assertion in the global TESLA context. More... | |
#define | TESLA_PERTHREAD(...) TESLA_ASSERT(__tesla_perthread, __VA_ARGS__) |
An assertion in a thread's TESLA context. More... | |
#define | TIGNORE __tesla_ignore |
An epsilon transition in a a TESLA NFA; a non-event. More... | |
#define | TSEQUENCE(...) __tesla_sequence(TIGNORE, __VA_ARGS__) |
A strictly-ordered sequence of events. More... | |
#define | called(...) __tesla_call(((void)__VA_ARGS__, TIGNORE)) |
#define | returned(...) __tesla_return(__VA_ARGS__) |
#define | callee(...) __tesla_callee(TIGNORE, __VA_ARGS__) |
#define | caller(...) __tesla_caller(TIGNORE, __VA_ARGS__) |
#define | strict(...) __tesla_strict(TIGNORE, __VA_ARGS__) |
#define | conditional(...) __tesla_conditional(TIGNORE, __VA_ARGS__) |
#define | flags(...) __tesla_flags(__VA_ARGS__) |
#define | bitmask(...) __tesla_mask(__VA_ARGS__) |
#define | TESLA_NOW __tesla_now |
#define | TESLA_STRUCT_AUTOMATON(...) __tesla_struct_usage(__VA_ARGS__) |
#define | automaton(name,...) __tesla_automaton(name, __VA_ARGS__) |
#define | tesla_done return (__tesla_automaton_done()) |
#define | optional(...) __tesla_optional(TIGNORE, __VA_ARGS__) |
#define | ANY_REP INT_MAX |
#define | REPEAT(m, n,...) __tesla_repeat(m, n, __VA_ARGS__) |
#define | UPTO(n,...) __tesla_repeat(0, n, __VA_ARGS__) |
#define | ATLEAST(n,...) __tesla_repeat(n, ANY_REP, __VA_ARGS__) |
#define | ANY(int_type) __tesla_any(int_type) |
#define | previously(...) TSEQUENCE(__VA_ARGS__, TESLA_NOW) |
A more programmer-friendly way to write assertions about the past. More... | |
#define | eventually(...) TSEQUENCE(TESLA_NOW, __VA_ARGS__) |
A more programmer-friendly way to write assertions about the future. More... | |
#define | __tesla_any(type) __tesla_any_##type() |
#define | __tesla_struct_usage(subject, automaton, loc, start, end) |
Declare that a struct's behaviour is described by an automaton. More... | |
#define | __tesla_automaton(name,...) struct __tesla_automaton_description* name(__VA_ARGS__) |
Define an automaton to describe a struct's behaviour. More... | |
Typedefs | |
typedef struct __tesla_event | __tesla_event |
The basic TESLA type is a pointer to a TESLA Basic TESLA types (magic for the compiler to munge). More... | |
typedef struct __tesla_locality | __tesla_locality |
typedef int | __tesla_count |
A number of times to match an event: positive or "any number". More... | |
Functions | |
void | __tesla_inline_assertion (const char *filename, int line, int count, __tesla_locality *loc,...) |
Magic "function" representing a TESLA assertion. More... | |
struct __tesla_event * | __tesla_sequence (__tesla_event *,...) |
A sequence of TESLA events. More... | |
struct __tesla_event * | __tesla_call (void *,...) |
Entering a function (with optionally-specified arguments). More... | |
struct __tesla_event * | __tesla_return (void *,...) |
Exiting a function (with optionally-specified arguments). More... | |
struct __tesla_event * | __tesla_callee (__tesla_event *,...) |
Function events inside this predicate refer to the callee context. More... | |
struct __tesla_event * | __tesla_caller (__tesla_event *,...) |
Function events inside this predicate refer to the caller context. More... | |
int | __tesla_flags (int) |
A mask of flags we expect to see. More... | |
int | __tesla_mask (int) |
A bitmask that an argument must not exceed. More... | |
struct __tesla_event * | __tesla_strict (__tesla_event *,...) |
Events named in this predicate should only occur exactly as described. More... | |
struct __tesla_event * | __tesla_conditional (__tesla_event *,...) |
Events named in this predicate must occur as described if the execution trace includes a NOW event; otherwise, any number of non-NOW events can occur in any order. More... | |
struct __tesla_event * | __tesla_optional (__tesla_event *,...) |
void * | __tesla_any_ptr () |
A value that could match a lot of function parameters. More... | |
int | __tesla_any_int () |
long | __tesla_any_long () |
long long | __tesla_any_longlong () |
register_t | __tesla_any_register_t () |
struct __tesla_automaton_description * | __tesla_automaton_done () |
In an explicit automata description, return this to say "we're done". More... | |
struct __tesla_automaton_usage * | __tesla_struct_uses_automaton (const char *automaton, __tesla_locality *loc,...) |
Variables | |
__tesla_locality * | __tesla_global |
TESLA events can be serialised either with respect to the current thread or, using explicit synchronisation, the global execution context. More... | |
__tesla_locality * | __tesla_perthread |
struct __tesla_event * | __tesla_ignore |
Nothing to see here, move along... More... | |
struct __tesla_event * | __tesla_now |
Reaching the inline assertion. More... | |
struct __tesla_event |
struct __tesla_locality |
#define __tesla_automaton | ( | name, | |
... | |||
) | struct __tesla_automaton_description* name(__VA_ARGS__) |
#define __tesla_struct_usage | ( | subject, | |
automaton, | |||
loc, | |||
start, | |||
end | |||
) |
Declare that a struct's behaviour is described by an automaton.
subject | name of the struct that uses the automaton |
automaton | reference to the automaton description |
loc | a TESLA locality (global, per-thread...) |
start | event that kicks off the automaton |
end | event that winds up the automaton |
#define ANY | ( | int_type | ) | __tesla_any(int_type) |
Definition at line 97 of file tesla-macros.h.
#define ANY_REP INT_MAX |
Definition at line 93 of file tesla-macros.h.
#define ATLEAST | ( | n, | |
... | |||
) | __tesla_repeat(n, ANY_REP, __VA_ARGS__) |
Definition at line 96 of file tesla-macros.h.
#define automaton | ( | name, | |
... | |||
) | __tesla_automaton(name, __VA_ARGS__) |
Definition at line 89 of file tesla-macros.h.
#define bitmask | ( | ... | ) | __tesla_mask(__VA_ARGS__) |
Definition at line 82 of file tesla-macros.h.
#define called | ( | ... | ) | __tesla_call(((void)__VA_ARGS__, TIGNORE)) |
Definition at line 73 of file tesla-macros.h.
#define callee | ( | ... | ) | __tesla_callee(TIGNORE, __VA_ARGS__) |
Definition at line 76 of file tesla-macros.h.
#define caller | ( | ... | ) | __tesla_caller(TIGNORE, __VA_ARGS__) |
Definition at line 77 of file tesla-macros.h.
#define conditional | ( | ... | ) | __tesla_conditional(TIGNORE, __VA_ARGS__) |
Definition at line 79 of file tesla-macros.h.
A more programmer-friendly way to write assertions about the future.
Definition at line 103 of file tesla-macros.h.
#define flags | ( | ... | ) | __tesla_flags(__VA_ARGS__) |
Definition at line 81 of file tesla-macros.h.
#define optional | ( | ... | ) | __tesla_optional(TIGNORE, __VA_ARGS__) |
Definition at line 92 of file tesla-macros.h.
A more programmer-friendly way to write assertions about the past.
Definition at line 100 of file tesla-macros.h.
#define REPEAT | ( | m, | |
n, | |||
... | |||
) | __tesla_repeat(m, n, __VA_ARGS__) |
Definition at line 94 of file tesla-macros.h.
#define returned | ( | ... | ) | __tesla_return(__VA_ARGS__) |
Definition at line 74 of file tesla-macros.h.
#define strict | ( | ... | ) | __tesla_strict(TIGNORE, __VA_ARGS__) |
Definition at line 78 of file tesla-macros.h.
#define TESLA_ASSERT | ( | locality, | |
start, | |||
end, | |||
expression | |||
) |
An inline assertion.
Definition at line 55 of file tesla-macros.h.
#define tesla_done return (__tesla_automaton_done()) |
Definition at line 90 of file tesla-macros.h.
#define TESLA_GLOBAL | ( | ... | ) | TESLA_ASSERT(__tesla_global, __VA_ARGS__) |
An assertion in the global TESLA context.
Definition at line 62 of file tesla-macros.h.
#define TESLA_NOW __tesla_now |
Definition at line 84 of file tesla-macros.h.
#define TESLA_PERTHREAD | ( | ... | ) | TESLA_ASSERT(__tesla_perthread, __VA_ARGS__) |
An assertion in a thread's TESLA context.
Definition at line 65 of file tesla-macros.h.
#define TESLA_STRUCT_AUTOMATON | ( | ... | ) | __tesla_struct_usage(__VA_ARGS__) |
Definition at line 87 of file tesla-macros.h.
#define TESLA_WITHIN | ( | function, | |
expression | |||
) |
An assertion made within the execution of a particular function.
Definition at line 47 of file tesla-macros.h.
#define TIGNORE __tesla_ignore |
An epsilon transition in a a TESLA NFA; a non-event.
Definition at line 68 of file tesla-macros.h.
#define TSEQUENCE | ( | ... | ) | __tesla_sequence(TIGNORE, __VA_ARGS__) |
A strictly-ordered sequence of events.
Definition at line 71 of file tesla-macros.h.
#define UPTO | ( | n, | |
... | |||
) | __tesla_repeat(0, n, __VA_ARGS__) |
Definition at line 95 of file tesla-macros.h.
typedef int __tesla_count |
typedef struct __tesla_event __tesla_event |
The basic TESLA type is a pointer to a TESLA Basic TESLA types (magic for the compiler to munge).
typedef struct __tesla_locality __tesla_locality |
int __tesla_any_int | ( | ) |
long __tesla_any_long | ( | ) |
long long __tesla_any_longlong | ( | ) |
void* __tesla_any_ptr | ( | ) |
A value that could match a lot of function parameters.
Maybe anything?
register_t __tesla_any_register_t | ( | ) |
|
read |
In an explicit automata description, return this to say "we're done".
|
read |
Entering a function (with optionally-specified arguments).
|
read |
Function events inside this predicate refer to the callee context.
|
read |
Function events inside this predicate refer to the caller context.
|
read |
Events named in this predicate must occur as described if the execution trace includes a NOW event; otherwise, any number of non-NOW events can occur in any order.
For instance, if the assertion names the VOP_WRITE() event, we don't want to preclude the use of VOP_WRITE() in code paths that don't include this assertion's NOW event.
This is the default behaviour for inline assertions.
int __tesla_flags | ( | int | ) |
A mask of flags we expect to see.
|
inline |
int __tesla_mask | ( | int | ) |
A bitmask that an argument must not exceed.
|
read |
|
read |
Exiting a function (with optionally-specified arguments).
|
read |
A sequence of TESLA events.
Can be combined with && or ||.
|
read |
Events named in this predicate should only occur exactly as described.
This is the default behaviour for explicit automata representations.
|
read |
__tesla_locality* __tesla_global |
TESLA events can be serialised either with respect to the current thread or, using explicit synchronisation, the global execution context.
struct __tesla_event* __tesla_ignore |
struct __tesla_event* __tesla_now |
__tesla_locality* __tesla_perthread |