Detailed Description

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...

Class Documentation

struct __tesla_event

struct __tesla_locality

Macro Definition Documentation

#define __tesla_any ( type ) __tesla_any_##type()

Definition at line 144 of file tesla.h.

#define __tesla_automaton	(	name,
		...
	)	struct __tesla_automaton_description* name(__VA_ARGS__)

Define an automaton to describe a struct's behaviour.

This should take the relevant structure as an argument.

Definition at line 187 of file tesla.h.

#define __tesla_struct_usage	(	subject,
		automaton,
		loc,
		start,
		end
	)

Value:

struct __tesla_automaton_usage*                                 \
        __tesla_struct_automaton_usage_##struct_name##_##automaton(subject) { \
                return __tesla_struct_uses_automaton(                   \
                        #automaton, loc, start, end);   \
        }

Declare that a struct's behaviour is described by an automaton.

Parameters

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

Definition at line 174 of file tesla.h.

#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.

#define eventually ( ... ) TSEQUENCE(TESLA_NOW, __VA_ARGS__)

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.

#define previously ( ... ) TSEQUENCE(__VA_ARGS__, TESLA_NOW)

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
	)

Value:

__tesla_inline_assertion(                                       \
                __FILE__, __LINE__, __COUNTER__,                        \
                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
	)

Value:

TESLA_PERTHREAD(                                                \
                callee(called(function)),                               \
                callee(returned(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 Documentation

typedef int __tesla_count

A number of times to match an event: positive or "any number".

Definition at line 54 of file tesla.h.

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

Function Documentation

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 ( )

struct __tesla_automaton_description* __tesla_automaton_done ( )

read

In an explicit automata description, return this to say "we're done".

struct __tesla_event* __tesla_call	(	void *	,
			...
	)

read

Entering a function (with optionally-specified arguments).

struct __tesla_event* __tesla_callee	(	__tesla_event *	,
			...
	)

read

Function events inside this predicate refer to the callee context.

struct __tesla_event* __tesla_caller	(	__tesla_event *	,
			...
	)

read

Function events inside this predicate refer to the caller context.

struct __tesla_event* __tesla_conditional	(	__tesla_event *	,
			...
	)

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.

void __tesla_inline_assertion	(	const char *	filename,
		int	line,
		int	count,
		__tesla_locality *	loc,
			...
	)

inline

Magic "function" representing a TESLA assertion.

Its arguments are:

name of the file the assertion is located in (FILE)
the line the assertion is defined at (LINE)
a counter to ensure uniqueness (COUNTER)
the TESLA context (per-thread or global)

Definition at line 66 of file tesla.h.

68 {

69 }

int __tesla_mask ( int )

A bitmask that an argument must not exceed.

struct __tesla_event* __tesla_optional	(	__tesla_event *	,
			...
	)

read

struct __tesla_event* __tesla_return	(	void *	,
			...
	)

read

Exiting a function (with optionally-specified arguments).

struct __tesla_event* __tesla_sequence	(	__tesla_event *	,
			...
	)

read

A sequence of TESLA events.

Can be combined with && or ||.

struct __tesla_event* __tesla_strict	(	__tesla_event *	,
			...
	)

read

Events named in this predicate should only occur exactly as described.

This is the default behaviour for explicit automata representations.

struct __tesla_automaton_usage* __tesla_struct_uses_automaton	(	const char *	automaton,
		__tesla_locality *	loc,
			...
	)

read

Definition at line 158 of file tesla.h.

 {
         return 0;
 }

Variable Documentation

__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

Nothing to see here, move along...

Definition at line 130 of file tesla.h.

struct __tesla_event* __tesla_now

Reaching the inline assertion.

Definition at line 133 of file tesla.h.

__tesla_locality* __tesla_perthread

Computer Laboratory

Detailed Description

Classes

Macros

Typedefs

Functions

Variables

Class Documentation

Macro Definition Documentation

Typedef Documentation

Function Documentation

Variable Documentation