source: CIVL/text/include/pthread.cvl@ 0c69eda

1.23 2.0 main test-branch
Last change on this file since 0c69eda was b0045d9, checked in by John Edenhofner <johneden@…>, 12 years ago

Added tests, did transformation

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@1287 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 4.9 KB
Line 
1#ifdef __PTHREAD_CVL__
2#else
3#define __PTHREAD_CVL__
4#include <sched.cvl>
5
6
7//Mutex types
8enum{
9PTHREAD_MUTEX_NORMAL,
10PTHREAD_MUTEX_RECURSIVE,
11PTHREAD_MUTEX_ERRORCHECK
12};
13
14enum{
15PTHREAD_MUTEX_STALLED,
16PTHREAD_MUTEX_ROBUST
17};
18
19enum{
20PTHREAD_CREATE_JOINABLE,
21PTHREAD_CREATE_DETACHED
22};
23
24enum{
25PTHREAD_SCOPE_SYSTEM,
26PTHREAD_SCOPE_PROCESS
27};
28
29enum{
30PTHREAD_INHERIT_SCHED,
31PTHREAD_EXPLICIT_SCHED
32};
33
34enum{
35PTHREAD_PROCESS_SHARED,
36PTHREAD_PROCESS_PRIVATE,
37};
38
39enum{
40PTHREAD_BARRIER_SERIAL_THREAD
41};
42
43//Mutex initializer
44#define __LOCK_INITIALIZER 0
45#define PTHREAD_MUTEX_INITIALIZER {0,0,0,PTHREAD_MUTEX_NORMAL,__LOCK_INITIALIZER}
46#define PTHREAD_COND_INITIALIZER {__LOCK_INITIALIZER,0}
47
48//Error definitions
49enum{
50EINVAL, //Designates an invalid value
51ENOTSUP,
52EOWNERDEAD, //Designates the termination of the owning thread
53EBUSY, //Mutex is already locked
54EDEADLK, //If mutex type is errorcheck and already owns the mutex
55EPERM, //If mutex is robust or errorcheck and does not own the mutex
56ERSCH
57};
58
59// In process of implementing
60
61typedef struct {
62 int pshared;
63} pthread_barrierattr_t;
64
65typedef struct {
66 pthread_barrierattr_t attr;
67 int numThrds;
68 int size;
69 $gbarrier barr;
70} pthread_barrier_t;
71
72typedef struct {
73 $proc owner;
74 _Bool lock;
75 int pshared;
76}pthread_spinlock_t;
77/*
78typedef struct {
79 int pshared;
80 clockid_t clock_id;
81}pthread_condattr_t;
82*/
83
84/* Implemented struct definitions */
85
86/* pthread_attr_t struct definition
87 Description: This struct corresponds to the pthread_attr_t which is the attribute of a pthread_t. It's fields
88 define the way the pthread_t is able to interact (join/detach), (memory capacity), (scope) etc.
89
90 Fields:
91 int detachstate: Defines a threads ability to join with two values: PTHREAD_CREATE_DETACHED and PTHREAD_CREATE_JOINABLE
92 int inheritsched: The inheritance scheduling policy of the thread
93 int contentionscope: Defines the contention scope of the thread
94 int schedpolicy: Determines the scheduling policy of the thread
95
96*/
97
98typedef struct {
99 int detachstate;
100 int inheritsched;
101 int contentionscope;
102 int schedpolicy;
103 //sched_param param;
104} pthread_attr_t;
105
106/* pthread_mutexattr_t struct definition
107 Description: The pthread_mutexattr_t defines multiple attributes of a mutex and controls its interactions with threads
108 Fields: robust: defines the robustness of the mutex; if robust and the owning thread terminates, it will notify the
109 next thread of this to prevent deadlocks and other errors
110 pshared: defines the process shared element of the thread and which processes can interact with the mutex
111 protocol: defines the priority protocol of the mutex and which threads may interact first
112 type: defines the type of the mutex as either PTHREAD_MUTEX_DEFAULT/NORMAL, PTHREAD_MUTEX_ERRORCHECK, or
113 PTHREAD_MUTEX_RECURSIVE, each explained in pthread_mutex_lock below
114 prioceiling: defines the lowest priority the mutex's critical section can be at
115*/
116
117typedef struct {
118 int robust;
119 int pshared;
120 int protocol;
121 int type;
122 int prioceiling;
123}pthread_mutexattr_t;
124
125/* pthread_mutex_t struct definition
126 Description: The pthread_mutex_t is a locking mechanism for threads to interact with in order to control the scheduling
127 of the threads. It can be locked, which allows for blocking of other threads waiting on the mutex and unlocked, allowing
128 access. It has a pthread_mutexattr_t which defines its behavior.
129 Fields: count - used for recursive mutex, incremented when locked, decremented when unlocked, mutex released when count is 0
130 owner - current process owner of the mutex
131 lock - int of 0 or 1, respectively 0 if unlocked, 1 if locked
132 prioceiling - allows locking without adherence to the priority ceiling
133 attr - see above
134*/
135
136typedef struct {
137 int count;
138 $proc owner;
139 int lock;
140 int prioceiling;
141 pthread_mutexattr_t attr;
142} pthread_mutex_t;
143
144
145/* pthread_cond_t struct definition
146 Description: The pthread_cond_t is another locking mechanism which interacts with the mutex variable. When
147 the mutex is locked, the condition can be accessed, leading the accessing thread to unlock it, and sleep
148 until the signal is given
149 Fields: proccount - specifies the number of processes/threads still waiting on this condition variable
150 signal - Boolean value stating whether the condition is satisfied (indicated by 1) or not (0)
151*/
152
153typedef struct {
154 int proccount;
155 _Bool signal;
156} pthread_cond_t;
157
158/* pthread_t struct definition
159 Description: The pthread_t is a struct containing a $proc variable as well as a thread attribute which defines
160 its interactions with other threads. It encapsulates the $proc and allows attributes to apply to it.
161 Fields: thr: the $proc variable that is the heart of the thread
162 attr: see above
163*/
164
165typedef struct {
166 $proc thr;
167 const pthread_attr_t attr;
168 int pid;
169} pthread_t;
170
171typedef struct __pthread_pool_t {
172 pthread_t** threads;
173 int len;
174} __pthread_pool_t;
175
176#endif
177
Note: See TracBrowser for help on using the repository browser.