pthread_lib.c File Reference

#include <errno.h>
#include <pthread.h>
#include <stddef.h>

Include dependency graph for pthread_lib.c:

Classes
struct	__pthread_start_data
struct	thread_key

Macros
#define	CLEANUP_STACK_CHUNK_SIZE   1024
#define	__ESBMC_mutex_lock_field(a)
#define	__ESBMC_mutex_waiters(a)
#define	__ESBMC_mutex_owner_field(a)
#define	__ESBMC_mutex_kind_field(a)
#define	__ESBMC_mutex_depth_field(a)
#define	__ESBMC_mutexattr_kind(a)
#define	__ESBMC_cond_lock_field(a)
#define	__ESBMC_cond_futex_field(a)
#define	__ESBMC_cond_nwaiters_field(a)
#define	__ESBMC_rwlock_readers(a)
#define	__ESBMC_rwlock_writer(a)
#define	__ESBMC_rwlock_waiters(a)
#define	__ESBMC_barrier_count(a)
#define	__ESBMC_barrier_arrived(a)
#define	__ESBMC_barrier_generation(a)
#define	__ESBMC_barrier_waiters(a)
#define	__ESBMC_spin_lock_field(a)
#define	__ESBMC_spin_waiters(a)
#define	__ESBMC_MUTEX_NOT_HELD_BY_SELF   (-1)
#define	__ESBMC_ONCE_RUNNING   1
#define	__ESBMC_ONCE_DONE   2

Typedefs
typedef void *(*	__ESBMC_thread_start_func_type) (void *)
typedef struct thread_key	__ESBMC_thread_key

Functions
void	__ESBMC_terminate_thread (void)
unsigned int	__ESBMC_spawn_thread (void(*)(void))
void	__ESBMC_init_thread_local (void)
struct __pthread_start_data	__ESBMC_get_thread_internal_data (pthread_t tid)
void	__ESBMC_set_thread_internal_data (pthread_t tid, struct __pthread_start_data data)
	__attribute__ ((annotate("__ESBMC_inf_size")))
size_t	__esbmc_get_cleanup_level (void)
void	__esbmc_set_cleanup_level (int level)
static __ESBMC_thread_key *	search_key (pthread_key_t key)
static int	delete_key (__ESBMC_thread_key *l)
void	__ESBMC_pthread_start_main_hook (void)
void	__ESBMC_pthread_end_main_hook (void)
void	pthread_exec_key_destructors (void)
void	pthread_trampoline (void)
int	pthread_create (pthread_t *thread, const pthread_attr_t *attr, void *(*start_routine)(void *), void *arg)
void	pthread_exit (void *retval)
pthread_t	pthread_self (void)
void	pthread_testcancel (void)
	Deliver a pending cancellation if cancelstate is PTHREAD_CANCEL_ENABLE.
int	pthread_cancel (pthread_t th)
	Send a cancellation request to thread th.
int	pthread_setcancelstate (int state, int *oldstate)
	Set the calling thread's cancellability state.
int	pthread_setcanceltype (int type, int *oldtype)
	Set the calling thread's cancellation type.
int	pthread_join_switch (pthread_t thread, void **retval)
int	pthread_join_noswitch (pthread_t thread, void **retval)
int	pthread_mutexattr_init (pthread_mutexattr_t *attr)
int	pthread_mutexattr_destroy (pthread_mutexattr_t *attr)
int	pthread_mutexattr_settype (pthread_mutexattr_t *attr, int kind)
int	pthread_mutexattr_gettype (const pthread_mutexattr_t *attr, int *kind)
static void	__ESBMC_mutex_clear (pthread_mutex_t *mutex)
int	pthread_mutex_init (pthread_mutex_t *mutex, const pthread_mutexattr_t *mutexattr)
int	pthread_mutex_initializer (pthread_mutex_t *mutex)
static int	__ESBMC_mutex_relock (pthread_mutex_t *mutex)
static void	__ESBMC_mutex_acquire (pthread_mutex_t *mutex)
static _Bool	__ESBMC_mutex_release (pthread_mutex_t *mutex)
static _Bool	__ESBMC_mutex_unlock_denied (pthread_mutex_t *mutex)
int	pthread_mutex_lock_noassert (pthread_mutex_t *mutex)
int	pthread_mutex_lock_nocheck (pthread_mutex_t *mutex)
int	pthread_mutex_unlock_noassert (pthread_mutex_t *mutex)
int	pthread_mutex_unlock_nocheck (pthread_mutex_t *mutex)
int	pthread_mutex_lock_check (pthread_mutex_t *mutex)
int	pthread_mutex_unlock_check (pthread_mutex_t *mutex)
int	pthread_mutex_trylock (pthread_mutex_t *mutex)
int	pthread_mutex_destroy_check (pthread_mutex_t *mutex)
int	pthread_mutex_destroy (pthread_mutex_t *mutex)
int	pthread_rwlock_destroy (pthread_rwlock_t *lock)
int	pthread_rwlock_init (pthread_rwlock_t *lock, const pthread_rwlockattr_t *attr)
int	pthread_rwlock_rdlock (pthread_rwlock_t *lock)
int	pthread_rwlock_rdlock_check (pthread_rwlock_t *lock)
int	pthread_rwlock_tryrdlock (pthread_rwlock_t *lock)
int	pthread_rwlock_trywrlock (pthread_rwlock_t *lock)
int	pthread_rwlock_unlock (pthread_rwlock_t *lock)
int	pthread_rwlock_wrlock (pthread_rwlock_t *lock)
int	pthread_rwlock_wrlock_check (pthread_rwlock_t *lock)
int	pthread_barrierattr_init (pthread_barrierattr_t *attr)
int	pthread_barrierattr_destroy (pthread_barrierattr_t *attr)
int	pthread_barrierattr_getpshared (const pthread_barrierattr_t *attr, int *pshared)
int	pthread_barrierattr_setpshared (pthread_barrierattr_t *attr, int pshared)
int	pthread_barrier_init (pthread_barrier_t *barrier, const pthread_barrierattr_t *attr, unsigned int count)
int	pthread_barrier_destroy (pthread_barrier_t *barrier)
int	pthread_barrier_wait (pthread_barrier_t *barrier)
int	pthread_spin_init (pthread_spinlock_t *lock, int pshared)
int	pthread_spin_destroy (pthread_spinlock_t *lock)
int	pthread_spin_lock (pthread_spinlock_t *lock)
int	pthread_spin_trylock (pthread_spinlock_t *lock)
int	pthread_spin_unlock (pthread_spinlock_t *lock)
int	pthread_cond_broadcast (pthread_cond_t *cond)
int	pthread_cond_init (pthread_cond_t *cond, __const pthread_condattr_t *cond_attr)
int	pthread_cond_destroy (pthread_cond_t *__cond)
int	pthread_cond_signal (pthread_cond_t *__cond)
static void	do_pthread_cond_wait (pthread_cond_t *cond, pthread_mutex_t *mutex, _Bool assrt)
int	pthread_cond_wait_nocheck (pthread_cond_t *cond, pthread_mutex_t *mutex)
int	pthread_cond_wait_check (pthread_cond_t *cond, pthread_mutex_t *mutex)
int	pthread_key_create (pthread_key_t *key, void(*destructor)(void *))
void *	pthread_getspecific (pthread_key_t key)
int	pthread_setspecific (pthread_key_t key, const void *value)
int	pthread_equal (pthread_t tid1, pthread_t tid2)
int	pthread_once (pthread_once_t *once_control, void(*init_routine)(void))
int	pthread_detach (pthread_t threadid)
void	pthread_cleanup_push (void(*function)(void *), void *arg)
	Push a cleanup handler onto the current thread's cleanup stack.
void	pthread_cleanup_pop (int execute)
	Pop a cleanup handler from the current thread's cleanup stack and optionally execute it.
void	__pyt_init_tid (unsigned int tid)
void	__pyt_terminate (void)
void	__pyt_join (unsigned int thread)
void	__ESBMC_pylock_block_and_check (void)
void	__pyt_lock_release_waiters (unsigned int waiters)

Variables
	cleanup_entry_t
static _Bool	__ESBMC_mutex_owner_tracking = 0

Macro Definition Documentation

__ESBMC_barrier_arrived

#define __ESBMC_barrier_arrived

(

a

)

Value:

((a)->__arrived)

__ESBMC_barrier_count

#define __ESBMC_barrier_count

(

a

)

Value:

((a)->__count)

__ESBMC_barrier_generation

#define __ESBMC_barrier_generation

(

a

)

Value:

((a)->__generation)

__ESBMC_barrier_waiters

#define __ESBMC_barrier_waiters

(

a

)

Value:

((a)->__waiters)

__ESBMC_cond_futex_field

#define __ESBMC_cond_futex_field

(

a

)

Value:

((a).__futex)

__ESBMC_cond_lock_field

#define __ESBMC_cond_lock_field

(

a

)

Value:

((a).__lock)

__ESBMC_cond_nwaiters_field

#define __ESBMC_cond_nwaiters_field

(

a

)

Value:

((a).__nwaiters)

__ESBMC_mutex_depth_field

#define __ESBMC_mutex_depth_field

(

a

)

Value:

((a).__depth)

__ESBMC_mutex_kind_field

#define __ESBMC_mutex_kind_field

(

a

)

Value:

((a).__kind)

__ESBMC_mutex_lock_field

#define __ESBMC_mutex_lock_field

(

a

)

Value:

((a).__lock)

__ESBMC_MUTEX_NOT_HELD_BY_SELF

#define __ESBMC_MUTEX_NOT_HELD_BY_SELF   (-1)

__ESBMC_mutex_owner_field

#define __ESBMC_mutex_owner_field

(

a

)

Value:

((a).__owner)

__ESBMC_mutex_waiters

#define __ESBMC_mutex_waiters

(

a

)

Value:

((a).__count)

__ESBMC_mutexattr_kind

#define __ESBMC_mutexattr_kind

(

a

)

Value:

((a).__align)

__ESBMC_ONCE_DONE

#define __ESBMC_ONCE_DONE   2

__ESBMC_ONCE_RUNNING

#define __ESBMC_ONCE_RUNNING   1

__ESBMC_rwlock_readers

#define __ESBMC_rwlock_readers

(

a

)

Value:

((a)->__readers)

__ESBMC_rwlock_waiters

#define __ESBMC_rwlock_waiters

(

a

)

Value:

((a)->__waiters)

__ESBMC_rwlock_writer

#define __ESBMC_rwlock_writer

(

a

)

Value:

((a)->__writer)

__ESBMC_spin_lock_field

#define __ESBMC_spin_lock_field

(

a

)

Value:

((a)->__lock)

__ESBMC_spin_waiters

#define __ESBMC_spin_waiters

(

a

)

Value:

((a)->__waiters)

CLEANUP_STACK_CHUNK_SIZE

#define CLEANUP_STACK_CHUNK_SIZE   1024

Typedef Documentation

__ESBMC_thread_key

typedef struct thread_key __ESBMC_thread_key

__ESBMC_thread_start_func_type

typedef void *(* __ESBMC_thread_start_func_type) (void *)

Function Documentation

__attribute__()

__attribute__

(

( annotate("__ESBMC_inf_size"))

)

__esbmc_get_cleanup_level()

size_t __esbmc_get_cleanup_level

(

void

)

__ESBMC_get_thread_internal_data()

struct __pthread_start_data __ESBMC_get_thread_internal_data

(

pthread_t

tid

)

__ESBMC_init_thread_local()

void __ESBMC_init_thread_local

(

void

)

__ESBMC_mutex_acquire()

void __ESBMC_mutex_acquire ( pthread_mutex_t * mutex )

static

__ESBMC_mutex_clear()

void __ESBMC_mutex_clear ( pthread_mutex_t * mutex )

static

__ESBMC_mutex_release()

_Bool __ESBMC_mutex_release ( pthread_mutex_t * mutex )

static

__ESBMC_mutex_relock()

int __ESBMC_mutex_relock ( pthread_mutex_t * mutex )

static

__ESBMC_mutex_unlock_denied()

_Bool __ESBMC_mutex_unlock_denied ( pthread_mutex_t * mutex )

static

__ESBMC_pthread_end_main_hook()

void __ESBMC_pthread_end_main_hook

(

void

)

__ESBMC_pthread_start_main_hook()

void __ESBMC_pthread_start_main_hook

(

void

)

__ESBMC_pylock_block_and_check()

void __ESBMC_pylock_block_and_check

(

void

)

__esbmc_set_cleanup_level()

void __esbmc_set_cleanup_level

(

int

level

)

__ESBMC_set_thread_internal_data()

void __ESBMC_set_thread_internal_data	(	pthread_t	tid,
		struct __pthread_start_data	data )

__ESBMC_spawn_thread()

unsigned int __ESBMC_spawn_thread

(

void(*

)(void)

)

__ESBMC_terminate_thread()

void __ESBMC_terminate_thread

(

void

)

__pyt_init_tid()

void __pyt_init_tid

(

unsigned int

tid

)

__pyt_join()

void __pyt_join

(

unsigned int

thread

)

__pyt_lock_release_waiters()

void __pyt_lock_release_waiters

(

unsigned int

waiters

)

__pyt_terminate()

void __pyt_terminate

(

void

)

delete_key()

int delete_key ( __ESBMC_thread_key * l )

static

do_pthread_cond_wait()

void do_pthread_cond_wait ( pthread_cond_t * cond, pthread_mutex_t * mutex, _Bool assrt )

static

NOTE:

When using condition variables there is always a boolean predicate involving shared variables associated with each condition wait that is true if the thread should proceed.

Spurious wakeups from the pthread_cond_wait() or pthread_cond_timedwait() functions may occur. Since the return from pthread_cond_wait() or pthread_cond_timedwait() does not imply anything about the value of this predicate, the predicate should be re-evaluated upon such return.

pthread_barrier_destroy()

int pthread_barrier_destroy

(

pthread_barrier_t *

barrier

)

pthread_barrier_init()

int pthread_barrier_init	(	pthread_barrier_t *	barrier,
		const pthread_barrierattr_t *	attr,
		unsigned int	count )

pthread_barrier_wait()

int pthread_barrier_wait

(

pthread_barrier_t *

barrier

)

pthread_barrierattr_destroy()

int pthread_barrierattr_destroy

(

pthread_barrierattr_t *

attr

)

pthread_barrierattr_getpshared()

int pthread_barrierattr_getpshared	(	const pthread_barrierattr_t *	attr,
		int *	pshared )

pthread_barrierattr_init()

int pthread_barrierattr_init

(

pthread_barrierattr_t *

attr

)

pthread_barrierattr_setpshared()

int pthread_barrierattr_setpshared	(	pthread_barrierattr_t *	attr,
		int	pshared )

pthread_cancel()

int pthread_cancel

(

pthread_t

th

)

Send a cancellation request to thread th.

pthread_cleanup_pop()

void pthread_cleanup_pop

(

int

execute

)

Pop a cleanup handler from the current thread's cleanup stack and optionally execute it.

This function removes the most recently pushed cleanup handler. If execute is non-zero, it calls the cleanup function with the stored argument.

Parameters

execute

If non-zero, execute the popped cleanup handler.

pthread_cleanup_push()

void pthread_cleanup_push	(	void(*	function )(void *),
		void *	arg )

Push a cleanup handler onto the current thread's cleanup stack.

This function registers a cleanup handler function along with its argument to be called later if pthread_cleanup_pop is invoked with execute != 0.

The cleanup handlers are stored in a large symbolic array divided into chunks of size CLEANUP_STACK_CHUNK_SIZE per thread to avoid overlap between threads.

Parameters

function	Pointer to the cleanup function to be called.
arg	Argument to pass to the cleanup function.

pthread_cond_broadcast()

int pthread_cond_broadcast

(

pthread_cond_t *

cond

)

pthread_cond_destroy()

int pthread_cond_destroy

(

pthread_cond_t *

__cond

)

pthread_cond_init()

int pthread_cond_init	(	pthread_cond_t *	cond,
		__const pthread_condattr_t *	cond_attr )

pthread_cond_signal()

int pthread_cond_signal ( pthread_cond_t * __cond )

extern

pthread_cond_wait_check()

int pthread_cond_wait_check	(	pthread_cond_t *	cond,
		pthread_mutex_t *	mutex )

pthread_cond_wait_nocheck()

int pthread_cond_wait_nocheck	(	pthread_cond_t *	cond,
		pthread_mutex_t *	mutex )

pthread_create()

int pthread_create	(	pthread_t *	thread,
		const pthread_attr_t *	attr,
		void *(*	start_routine )(void *),
		void *	arg )

pthread_detach()

int pthread_detach

(

pthread_t

threadid

)

pthread_equal()

int pthread_equal	(	pthread_t	tid1,
		pthread_t	tid2 )

pthread_exec_key_destructors()

void pthread_exec_key_destructors

(

void

)

pthread_exit()

void pthread_exit

(

void *

retval

)

pthread_getspecific()

void * pthread_getspecific

(

pthread_key_t

key

)

pthread_join_noswitch()

int pthread_join_noswitch	(	pthread_t	thread,
		void **	retval )

pthread_join_switch()

int pthread_join_switch	(	pthread_t	thread,
		void **	retval )

pthread_key_create()

int pthread_key_create	(	pthread_key_t *	key,
		void(*	destructor )(void *) )

pthread_mutex_destroy()

int pthread_mutex_destroy

(

pthread_mutex_t *

mutex

)

pthread_mutex_destroy_check()

int pthread_mutex_destroy_check

(

pthread_mutex_t *

mutex

)

pthread_mutex_init()

int pthread_mutex_init	(	pthread_mutex_t *	mutex,
		const pthread_mutexattr_t *	mutexattr )

pthread_mutex_initializer()

int pthread_mutex_initializer

(

pthread_mutex_t *

mutex

)

pthread_mutex_lock_check()

int pthread_mutex_lock_check

(

pthread_mutex_t *

mutex

)

pthread_mutex_lock_noassert()

int pthread_mutex_lock_noassert

(

pthread_mutex_t *

mutex

)

pthread_mutex_lock_nocheck()

int pthread_mutex_lock_nocheck

(

pthread_mutex_t *

mutex

)

pthread_mutex_trylock()

int pthread_mutex_trylock

(

pthread_mutex_t *

mutex

)

pthread_mutex_unlock_check()

int pthread_mutex_unlock_check

(

pthread_mutex_t *

mutex

)

pthread_mutex_unlock_noassert()

int pthread_mutex_unlock_noassert

(

pthread_mutex_t *

mutex

)

pthread_mutex_unlock_nocheck()

int pthread_mutex_unlock_nocheck

(

pthread_mutex_t *

mutex

)

pthread_mutexattr_destroy()

int pthread_mutexattr_destroy

(

pthread_mutexattr_t *

attr

)

pthread_mutexattr_gettype()

int pthread_mutexattr_gettype	(	const pthread_mutexattr_t *	attr,
		int *	kind )

pthread_mutexattr_init()

int pthread_mutexattr_init

(

pthread_mutexattr_t *

attr

)

pthread_mutexattr_settype()

int pthread_mutexattr_settype	(	pthread_mutexattr_t *	attr,
		int	kind )

pthread_once()

int pthread_once	(	pthread_once_t *	once_control,
		void(*	init_routine )(void) )

pthread_rwlock_destroy()

int pthread_rwlock_destroy

(

pthread_rwlock_t *

lock

)

pthread_rwlock_init()

int pthread_rwlock_init	(	pthread_rwlock_t *	lock,
		const pthread_rwlockattr_t *	attr )

pthread_rwlock_rdlock()

int pthread_rwlock_rdlock

(

pthread_rwlock_t *

lock

)

pthread_rwlock_rdlock_check()

int pthread_rwlock_rdlock_check

(

pthread_rwlock_t *

lock

)

pthread_rwlock_tryrdlock()

int pthread_rwlock_tryrdlock

(

pthread_rwlock_t *

lock

)

pthread_rwlock_trywrlock()

int pthread_rwlock_trywrlock

(

pthread_rwlock_t *

lock

)

pthread_rwlock_unlock()

int pthread_rwlock_unlock

(

pthread_rwlock_t *

lock

)

pthread_rwlock_wrlock()

int pthread_rwlock_wrlock

(

pthread_rwlock_t *

lock

)

pthread_rwlock_wrlock_check()

int pthread_rwlock_wrlock_check

(

pthread_rwlock_t *

lock

)

pthread_self()

pthread_t pthread_self

(

void

)

pthread_setcancelstate()

int pthread_setcancelstate	(	int	state,
		int *	oldstate )

Set the calling thread's cancellability state.

pthread_setcanceltype()

int pthread_setcanceltype	(	int	type,
		int *	oldtype )

Set the calling thread's cancellation type.

pthread_setspecific()

int pthread_setspecific	(	pthread_key_t	key,
		const void *	value )

pthread_spin_destroy()

int pthread_spin_destroy

(

pthread_spinlock_t *

lock

)

pthread_spin_init()

int pthread_spin_init	(	pthread_spinlock_t *	lock,
		int	pshared )

pthread_spin_lock()

int pthread_spin_lock

(

pthread_spinlock_t *

lock

)

pthread_spin_trylock()

int pthread_spin_trylock

(

pthread_spinlock_t *

lock

)

pthread_spin_unlock()

int pthread_spin_unlock

(

pthread_spinlock_t *

lock

)

pthread_testcancel()

void pthread_testcancel

(

void

)

Deliver a pending cancellation if cancelstate is PTHREAD_CANCEL_ENABLE.

pthread_trampoline()

void pthread_trampoline

(

void

)

search_key()

__ESBMC_thread_key * search_key ( pthread_key_t key )

static

Variable Documentation

__ESBMC_mutex_owner_tracking

_Bool __ESBMC_mutex_owner_tracking = 0

static

cleanup_entry_t

cleanup_entry_t