source: CIVL/text/include/pthread-c.cvl@ b18cc45

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

Added basic scheduling header, modified pthread_mutex_lock as well as mutliple other methods

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

  • Property mode set to 100644
File size: 24.1 KB
Line 
1extern void *value = NULL;
2extern __pthread_pool_t _pool={.len = 0};
3
4/*void _add_thread(__pthread_pool_t* pool, pthread_t* thread){
5 $atomic{
6 int len = pool->len;
7 pthread_t** newThreads = (pthread_t**) malloc(sizeof(pthread_t*) * (len+1));
8
9 if(pool->threads != NULL)
10 for(int i = 0; i < len - 1; i++)
11 *(newThreads+i) = *(pool->threads+i);
12 *(newThreads+len) = thread;
13 pool->threads = newThreads;
14 pool->len = len + 1;
15 }
16}
17
18_Bool isTerminated($proc thr){
19 for(int i = 0; i < _pool.len - 1; i++){
20 if(_pool.threads[i]->thr == thr){
21 if(_pool.threads[i]->terminated == true){
22 return true;
23 }
24 }
25 }
26 return false;
27}
28*/
29/**
30 * Initializes an attribute with the default values defined for it by an implementation.
31 * Corresponding specification: p. 1532-4
32 *
33 * @param *attr
34 * The attribute to be initialized.
35 * @return Returns 0 upon successful completion
36 */
37
38int pthread_attr_init(pthread_attr_t *attr){
39 attr->detachstate = PTHREAD_CREATE_JOINABLE;
40 //attr->inheritsched = PTHREAD_EXPLICIT_SCHED;
41 attr->contentionscope = PTHREAD_SCOPE_SYSTEM;
42 //attr->schedpolicy = SCHED_OTHER;
43 return 0;
44}
45
46/**
47 * Uninitializes the specified attr variable.
48 * Corresponding specification: p. 1532-4
49 *
50 * @param *attr
51 * The attribute to be uninitialized.
52 * @return Returns 0 upon successful completion
53 */
54
55int pthread_attr_destroy(pthread_attr_t *attr)
56{
57 pthread_attr_t blank;
58
59 *attr = blank;
60 return 0;
61}
62
63
64/**
65 * Sets the detachstate field of the attribute
66 * Corresponding specification: p. 1535-6
67 *
68 * @param *attr
69 * The attribute to have it's detachstate set
70 * @param detachstate
71 * The detachstate to which the attribute's detachstate is set
72 * @return Returns 0 upon successful completion
73 */
74
75int pthread_attr_setdetachstate(pthread_attr_t *attr, int detachstate)
76{
77 attr->detachstate = detachstate;
78 return 0;
79}
80
81/**
82 * Stores the detachstate value of the attribute in an alternate location
83 * Corresponding specification: p. 1535-6
84 *
85 * @param *attr
86 * The attribute whose detachstate is to be stored
87 * @param *detachstate
88 * The location at which the detachstate is to be stored
89 * @return Returns 0 upon successful completion
90 */
91
92int pthread_attr_getdetachstate(const pthread_attr_t *attr, int *detachstate)
93{
94 *detachstate = attr->detachstate;
95 return 0;
96}
97
98/**
99 * Set scheduling inheritance
100 * Corresponding specification: p. 1540-1
101 *
102 * @param *attr
103 * The attribute to have it's inheritsched set
104 * @param inheritsched
105 * The inheritsched to which the attribute's inheritsched is set
106 * @return Returns 0 upon successful completion
107 */
108
109int pthread_attr_setinheritsched(pthread_attr_t *attr, int inheritsched)
110{
111 attr->inheritsched = inheritsched;
112 return 0;
113}
114
115/**
116 * Stores the inheritsched value of the attribute in an alternate location
117 * Corresponding specification: p. 1540-1
118 *
119 * @param *attr
120 * The attribute whose inheritsched is to be stored
121 * @param *intheritsched
122 * The location at which the attribute's inheritsched is to be stored
123 * @return Returns 0 upon successful completion
124 */
125
126int pthread_attr_getinheritsched(const pthread_attr_t *attr, int *inheritsched)
127{
128 *inheritsched = attr->inheritsched;
129 return 0;
130}
131/*
132int pthread_attr_setschedparam(pthread_attr_t *attr, int priority)
133{
134 attr->param.sched_priority = priority;
135 return 0;
136}
137
138int pthread_attr_getschedparam(const pthread_attr_t *attr, sched_param *param)
139{
140 *param = attr->param;
141 return 0;
142}
143
144*/
145/**
146 * Set contentionscope field of the attribute
147 * Corresponding specification: p. 1546-7
148 *
149 * @param *attr
150 * The attribute to have it's contentionscope set
151 * @param contentionscope
152 * The contentionscope to which the attribute's contentionscope is set
153 * @return Returns 0 upon successful completion
154 */
155
156int pthread_attr_setscope(pthread_attr_t *attr, int contentionscope)
157{
158 attr->contentionscope = contentionscope;
159 return 0;
160}
161
162/**
163 * Stores the contentionscope value of the attribute in an alternate location
164 * Corresponding specification: p. 1546-7
165 *
166 * @param *attr
167 * The attribute whose contentionscope is to be stored
168 * @param *contentionscope
169 * The location at which the attribute's contentionscope is to be stored
170 * @return Returns 0 upon successful completion
171 */
172
173int pthread_attr_getscope(const pthread_attr_t *attr, int *contentionscope)
174{
175 *contentionscope = attr->contentionscope;
176 return 0;
177}
178
179/**
180 * Sets the scheduling policy field of the attribute
181 * Corresponding specification: p. 1544-45
182 *
183 * @param *attr
184 * The attribute to have it's scheduling policy set
185 * @param policy
186 * The scheduling policy to which the attribute's scheduling policy is set
187 * @return Returns 0 upon successful completion
188 */
189
190int pthread_attr_setschedpolicy(pthread_attr_t *attr, int policy)
191{
192 attr->schedpolicy = policy;
193 return 0;
194}
195
196/**
197 * Stores the scheduling policy value in an alternate location
198 * Corresponding specification: p. 1544-45
199 *
200 * @param *attr
201 * The attribute whose scheduling policy is to be stored
202 * @param *policy
203 * The location at which the attribute's scheduling policy is to be stored
204 * @return Returns 0 upon successful completion
205 */
206
207int pthread_attr_getschedpolicy(const pthread_attr_t *attr, int *policy)
208{
209 *policy = attr->schedpolicy;
210 return 0;
211}
212
213/**
214 * Initializes an attribute with the default values defined for it by an implementation.
215 * Corresponding specification: p. 1647-51
216 *
217 * @param *attr
218 * The attribute to be initialized.
219 * @return Returns 0 upon successful completion
220 */
221
222int pthread_mutexattr_init(pthread_mutexattr_t *attr){
223 attr->robust = 0;
224 attr->pshared = 0;
225 attr->protocol = 0;
226 attr->type = 0;
227 attr->prioceiling = 0;
228 return 0;
229}
230
231/**
232 * Uninitializes the specified attr variable.
233 * Corresponding specification: p. 1647-51
234 *
235 * @param *attr
236 * The attribute to be uninitialized.
237 * @return Returns 0 upon successful completion
238 */
239
240int pthread_mutexattr_destroy(pthread_mutexattr_t *attr){
241 pthread_mutexattr_t blank;
242
243 *attr = blank;
244 return 0;
245}
246
247/**
248 * Stores the robustness value in an alternate location
249 * Corresponding specification: p. 1659-1660
250 *
251 * @param *attr
252 * The attribute whose robustness is to be stored
253 * @param *robust
254 * The location at which the attribute's robustness is to be stored
255 * @return Returns 0 upon successful completion
256 */
257
258int pthread_mutexattr_getrobust(const pthread_mutexattr_t *attr, int *robust){
259 *robust = attr->robust;
260 return 0;
261}
262
263/**
264 * Sets the robustness field of the attribute
265 * Corresponding specification: p. 1659-1660
266 *
267 * @param *attr
268 * The attribute to have it's robustness set
269 * @param robust
270 * The robustness to which the attribute's robustness is set
271 * @return Returns 0 upon successful completion
272 */
273
274int pthread_mutexattr_setrobust(pthread_mutexattr_t *attr, int robust){
275 attr->robust = robust;
276 return 0;
277}
278
279/**
280 * Stores the process shared variable in an alternate location
281 * Corresponding specification: p. 1657-8
282 *
283 * @param *attr
284 * The attribute whose process shared variable is to be stored
285 * @param *detachstate
286 * The location at which the attribute's process shared variable is to be stored
287 * @return Returns 0 upon successful completion
288 */
289
290int pthread_mutexattr_getpshared(const pthread_mutexattr_t *attr, int *pshared){
291 *pshared = attr->pshared;
292 return 0;
293}
294
295/**
296 * Sets the process shared variable field of the attribute
297 * Corresponding specification: p. 1657-8
298 *
299 * @param *attr
300 * The attribute to have it's process shared variable set
301 * @param detachstate
302 * The process shared variable to which the attribute's process shared variable is set
303 * @return Returns 0 upon successful completion
304 */
305
306int pthread_mutexattr_setpshared(pthread_mutexattr_t *attr, int pshared){
307 attr->pshared = pshared;
308 return 0;
309}
310
311/**
312 * Stores the protocol value in an alternate location
313 * Corresponding specification: p. 1654-56
314 *
315 * @param *attr
316 * The attribute whose protocol is to be stored
317 * @param *detachstate
318 * The location at which the attribute's protocol is to be stored
319 * @return Returns 0 upon successful completion
320 */
321
322int pthread_mutexattr_getprotocol(const pthread_mutexattr_t *attr, int *protocol){
323 *protocol = attr->protocol;
324 return 0;
325}
326
327/**
328 * Sets the protocol field of the attribute
329 * Corresponding specification: p. 1654-56
330 *
331 * @param *attr
332 * The protocol to have it's protocol set
333 * @param detachstate
334 * The protocol to which the attribute's protocol is set
335 * @return Returns 0 upon successful completion
336 */
337int pthread_mutexattr_setprotocol(pthread_mutexattr_t *attr, int protocol){
338 attr->protocol = protocol;
339 return 0;
340}
341
342/**
343 * Stores the type value in an alternate location
344 * Corresponding specification: p. 1709-10
345 *
346 * @param *attr
347 * The attribute whose type is to be stored
348 * @param *detachstate
349 * The location at which the attribute's type is to be stored
350 * @return Returns 0 upon successful completion
351 */
352int pthread_mutexattr_gettype(const pthread_mutexattr_t *attr, int *type){
353 *type = attr->type;
354 return 0;
355}
356
357/**
358 * Sets the type field of the attribute
359 * Corresponding specification: p. 1709-10
360 *
361 * @param *attr
362 * The attribute to have it's type set
363 * @param detachstate
364 * The type to which the attribute's type is set
365 * @return Returns 0 upon successful completion
366 */
367int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type){
368 attr->type = type;
369 return 0;
370}
371
372/**
373 * Stores the priority ceiling value in an alternate location
374 * Corresponding specification: p. 1700-1
375 *
376 * @param *attr
377 * The attribute whose priority ceiling is to be stored
378 * @param *detachstate
379 * The location at which the attribute's priority ceiling is to be stored
380 * @return Returns 0 upon successful completion
381 */
382
383int pthread_mutexattr_getprioceiling(const pthread_mutexattr_t *attr, int *prioceiling){
384 *prioceiling = attr->prioceiling;
385 return 0;
386}
387
388/**
389 * Sets the priority ceiling field of the attribute
390 * Corresponding specification: p. 1700-1
391 *
392 * @param *attr
393 * The attribute to have it's priority ceiling set
394 * @param detachstate
395 * The priority ceiling to which the attribute's priority ceiling is set
396 * @return Returns 0 upon successful completion
397 */
398
399int pthread_mutexattr_setprioceiling(pthread_mutexattr_t *attr, int prioceiling){
400 attr->prioceiling = prioceiling;
401 return 0;
402}
403
404
405/**
406 * Initializes a mutex with the default values defined for it by an implementation
407 * or with the values defined by the mutex attribute parameter
408 * Corresponding specification: p. 1676-81
409 *
410 * @param *mutex
411 * The mutex to be initialized.
412 * @param *attr
413 * The mutex attribute which the mutex shall take as it's field. May also
414 * be null for default values to be initialized.
415 * @return Returns 0 upon successful completion
416 */
417
418int pthread_mutex_init(pthread_mutex_t *mutex, const pthread_mutexattr_t *attr){
419 if(attr == NULL){
420 mutex->attr.robust = 0;
421 mutex->attr.pshared = 0;
422 mutex->attr.protocol = 0;
423 mutex->attr.type = PTHREAD_MUTEX_NORMAL;
424 mutex->attr.prioceiling = 0;
425 }
426 else{
427 mutex->attr = *attr;
428 }
429 mutex->lock = 0;
430 mutex->count = 0;
431 mutex->owner = $proc_null;
432 return 0;
433}
434
435/**
436 * Uninitializes the specified mutex variable.
437 * Corresponding specification: p. 1676-81
438 *
439 * @param *mutex
440 * The mutex to be uninitialized.
441 * @return Returns 0 upon successful completion
442 */
443
444int pthread_mutex_destroy(pthread_mutex_t *mutex){
445 pthread_mutex_t blank;
446
447 *mutex = blank;
448 return 0;
449}
450
451/**
452 * Initializes an condition with the default values defined for it by an implementation.
453 * Corresponding specification: p. 1630-32
454 *
455 * @param *cond
456 * The condition to be initialized.
457 * @param *arg
458 * Should be changed to condition attribute
459 * @return Returns 0 upon successful completion
460 */
461
462int pthread_cond_init(pthread_cond_t *cond, void *arg){
463 cond->proccount = 0;
464 cond->signal = 0;
465 return 0;
466}
467
468
469/**
470 * Uninitializes the specified cond variable.
471 * Corresponding specification: p. 1630-2
472 *
473 * @param *cond
474 * The condition to be uninitialized.
475 * @return Returns 0 upon successful completion
476 */
477
478int pthread_cond_destroy(pthread_cond_t *cond){
479 if(cond->proccount != 0){
480 $assert($false, "ERROR: Threads still waiting on specified condition variable");
481 }
482 else{
483 pthread_cond_t blank;
484 *cond = blank;
485 }
486 return 0;
487}
488
489/**
490 * Defines a pthread_t by assigning it an attribute value (by value so the original attribute's state is
491 * irrelevant), and spawning a process as the thr field with arguments void *arg
492 * Corresponding specification: p. 1649-51
493 *
494 * @param *thread
495 * The thread to be created with fields set from the other parameters.
496 * @param *attr
497 * The attribute to be assigned to the thread
498 * @param *startroutine
499 * The process to be spawned as the thread's actual 'thread'
500 * @param *arg
501 * The argument to be passed to the spawned function
502 *
503 * @return Returns 0 upon successful completion
504 */
505
506int pthread_create(pthread_t *thread, const pthread_attr_t *attr, void *(*start_routine)(void*), void *arg){
507 $atomic{
508 thread->thr = $spawn start_routine(arg);
509 thread->terminated = false;
510 if(attr == NULL){
511 thread->attr.detachstate = PTHREAD_CREATE_JOINABLE;
512 thread->attr.inheritsched = 0;
513 thread->attr.contentionscope = 0;
514 thread->attr.schedpolicy = 0;
515 }
516 else{
517 thread->attr = *attr;
518 }
519 _add_thread(&_pool, thread);
520 }
521 return 0;
522}
523
524/**
525 * Causes current thread to wait on thread specified as a parameter. If specified thread's detachstate field is set as PTHREAD_CREATE_DETACHED,
526 * error will be returned stating the the thread cannot be joined. The value_ptr of pthread_exit shall be passed to any joining thread to the
527 * terminated thread using pthread_join's value_ptr
528 * Corresponding specification: p. 1617-9
529 *
530 * @param thread
531 * The thread to be waited on by the current thread.
532 * @param **value_ptr
533 * The location at which the pthread_exit output is accessible
534 *
535 * @return Returns 0 upon successful completion
536 */
537
538int pthread_join(pthread_t thread, void **value_ptr){
539 if(&thread.attr != NULL){
540 if(thread.attr.detachstate == PTHREAD_CREATE_DETACHED){
541 $assert($false, "Thread is designated as unjoinable");
542 return 1;
543 }
544 }
545 $wait(thread.thr);
546 if(value_ptr!=NULL)
547 value_ptr = &value;
548 return 0;
549}
550
551/**
552 * Causes current thread to immediately terminate; if currently in the main method as specified by the
553 * isMain parameter, the main method will wait for each thread to terminate before it terminates. The value
554 * value_ptr will be made accessible in the location stated in pthread_join
555 * Corresponding specification: p. 1655-6
556 *
557 * @param *value_ptr
558 * The value to be stored in the location stated by pthread_join
559 * @param isMain
560 * Is this thread the main thread?
561 * @param *arr
562 * The array of threads which need to be waited upon by the main thread
563 * @param len
564 * The length of the array of threads to be waited upon
565 * @return Returns 0 upon successful completion
566 */
567
568int _pthread_exit(void *value_ptr, _Bool isMain){
569 if(isMain){
570 /*
571 for(int i = 0; i<_pool.len; i++){
572 if($proc_defined(_pool.threads[i]->thr)){
573 $wait(_pool.threads[i]->thr);
574 _pool.threads[i]->terminated = true;
575 }
576 }
577 */
578 $exit();
579 return 0;
580 }
581 else{
582 $atomic{
583 for(int i = 0; i<_pool.len-1; i++){
584 if($proc_defined(_pool.threads[i]->thr)){
585 if(_pool.threads[i]->thr == $self){
586 _pool.threads[i]->terminated = true;
587 }
588 }
589 }
590 }
591 value = value_ptr;
592 $exit();
593 return 0;
594 }
595}
596
597//Unimplemented
598int pthread_detach(pthread_t thread);
599
600/**
601 * Takes in a mutex variable and acts accordingly to its current state and type
602 * PTHREAD_MUTEX_NORMAL: Checks to see whether mutex is already locked and behaves accordingly
603 * locked and owner: Relock error, returns 0
604 * locked and not owner: Waits until mutex is unlocked and then locks and becomes owner
605 * unlocked and not owner: Locks the mutex and becomes owner
606 * PTHREAD_MUTEX_RECURSIVE: A recursive mutex increments its count when it is locked and decremented when
607 * it is unlocked and the lock is released when the count reaches 0.
608 * PTHREAD_MUTEX_ERRORCHECK: Implemented similarly to PTHREAD_MUTEX_NORMAL, but notifies the user of errors
609 * Corresponding specification: p. 1686-9
610 *
611 * @param *mutex
612 * The mutex to be locked
613 * @return Returns 0 upon successful completion, EOWNERDEAD upon termination of owner,
614 */
615
616
617int pthread_mutex_lock(pthread_mutex_t *mutex){
618 $choose{
619 $when((mutex->attr.type == PTHREAD_MUTEX_NORMAL || mutex->attr.type == PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner == $proc_null && mutex->attr.robust == PTHREAD_MUTEX_ROBUST && mutex->lock == 0)
620 {
621 $atomic{
622 mutex->lock = 1;
623 mutex->count = 1;
624 mutex->owner = $self;
625 }
626 }
627 $when((mutex->attr.type == PTHREAD_MUTEX_NORMAL || mutex->attr.type == PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner != $proc_null && mutex->owner != $self && mutex->lock == 0)
628 {
629 $atomic{
630 mutex->lock = 1;
631 mutex->count = 1;
632 mutex->owner = $self;
633 }
634 }
635 $when((mutex->attr.type != PTHREAD_MUTEX_NORMAL && mutex->attr.type != PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner != $self && mutex->owner != $proc_null && mutex->lock == 0)
636 {
637 $atomic{
638 mutex->lock = 1;
639 mutex->count = 1;
640 mutex->owner = $self;
641 }
642 }
643 $when((mutex->attr.type == PTHREAD_MUTEX_NORMAL || mutex->attr.type == PTHREAD_MUTEX_ERRORCHECK) && mutex->lock == 0 && mutex->owner == $proc_null)
644 {
645 $atomic{
646 mutex->lock = 1;
647 mutex->count = 1;
648 mutex->owner = $self;
649 }
650 }
651 $when((mutex->attr.type == PTHREAD_MUTEX_NORMAL || mutex->attr.type == PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner == $proc_null && mutex->attr.robust != PTHREAD_MUTEX_ROBUST)
652 {
653 $assert($false, "Owner terminated without releasing mutex and was not robust");
654 return EOWNERDEAD;
655 }
656 $when((mutex->attr.type == PTHREAD_MUTEX_NORMAL || mutex->attr.type == PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner != $proc_null && mutex->owner== $self)
657 {
658 $assert($false, "Attempting to relock locked lock");
659 return EDEADLK;
660 }
661 $when((mutex->attr.type != PTHREAD_MUTEX_NORMAL && mutex->attr.type != PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner == $self)
662 {
663 mutex->count++;
664 }
665 $when((mutex->attr.type != PTHREAD_MUTEX_NORMAL && mutex->attr.type != PTHREAD_MUTEX_ERRORCHECK) && mutex->lock != 0 && mutex->owner != $self && mutex->owner == $proc_null && mutex->attr.robust != PTHREAD_MUTEX_ROBUST)
666 {
667 $assert($false, "Attempting to relock locked lock");
668 return EDEADLK;
669 }
670 }
671 return 0;
672}
673
674/**
675 * Takes in a mutex variable and acts similarly to pthread_mutex_lock except that
676 * if the mutex is locked, it will return immeditately. In the case of a recursive mutex, the count will
677 * be incremented and will return successfully.
678 * Corresponding specification: p. 1686-9
679 *
680 * @param *mutex
681 * The mutex to be locked
682 * @return Returns 0 upon successful completion
683 */
684
685int pthread_mutex_trylock(pthread_mutex_t *mutex){
686 $atomic{
687 if (mutex->attr.type == PTHREAD_MUTEX_NORMAL){
688 if (mutex->lock != 0) {
689 return EBUSY;
690 }
691 mutex->owner = $self;
692 mutex->lock = 1;
693 }
694 else {
695 int tmp = mutex->lock;
696
697 mutex->lock = 1;
698 if (tmp == 0) { // Attempts lock and checks for whether lock is already locked
699 mutex->count = 1;
700 mutex->owner = $self;
701 }
702 else {
703 //Checks for ownership, otherwise returns error
704 if(mutex->owner == $self){
705 // Checks for recursive mutex, otherwise returns an error
706 if (mutex->attr.type == PTHREAD_MUTEX_RECURSIVE) {
707 mutex->count++;
708 }
709 else {
710 $assert($false);
711 return 0;
712 }
713 }
714 else {
715 return EBUSY;
716 }
717 }
718 }
719 return 0;
720 }
721}
722
723/**
724 * Takes in a mutex variable and acts accordingly to its current state and type
725 * PTHREAD_MUTEX_NORMAL: Checks to see whether mutex is already unlocked and behaves accordingly
726 * unlocked: returns error
727 * locked: unlocks
728 * PTHREAD_MUTEX_RECURSIVE: A recursive mutex increments its count when it is locked and decremented when
729 * it is unlocked and the lock is released when the count reaches 0.
730 * PTHREAD_MUTEX_ERRORCHECK: Currently implemented similarly to PTHREAD_MUTEX_NORMAL
731 * Corresponding specification: p. 1686-9
732 *
733 * @param *mutex
734 * The mutex to be unlocked
735 * @return Returns 0 upon successful completion
736 */
737
738int pthread_mutex_unlock(pthread_mutex_t *mutex){
739 $atomic{
740 if (mutex->attr.type == 0 || mutex->attr.type == 2) {
741 // Attempts unlock, if already unlocked, returns error
742 if (mutex->lock == 0) {
743 $assert($false, "Attempting to unlock unlocked lock\n");
744 return 0;
745 }
746 else {
747 mutex->lock = 0;
748 mutex->owner = $proc_null;
749 }
750 }
751 else {
752 //Checks for ownership of thread, if not, returns error
753 if(mutex->owner == $self)
754 {
755 if (--mutex->count == 0){
756 mutex->lock = 0;
757 mutex->owner = $proc_null;
758 }
759 }
760 else {
761 $assert($false);
762 return 0;
763 }
764 }
765 return 0;
766 }
767}
768
769/**
770 * Checks for robustness of mutex: if robust, the mutex is unlocked, otherwise an error is caused
771 * and EINVAL is returned
772 * Corresponding specification: p. 1674-5
773 *
774 * @param *mutex
775 * The mutex to be marked as consistent
776 * @return Returns 0 upon successful completion, EINVAL upon non-robust mutex input
777 */
778
779int pthread_mutex_consistent(pthread_mutex_t *mutex){
780 if(mutex->attr.robust == PTHREAD_MUTEX_ROBUST){
781 mutex->lock = 0;
782 return 0;
783 }
784 $assert($false);
785 return EINVAL;
786}
787
788/**
789 * Checks for calling thread as owner of the mutex, then increments proccount, unlocks the mutex
790 * and sleeps. Awakens upon signal and decrements proccount and locks mutex.
791 * Corresponding specification: p. 1634-9
792 *
793 * @param *cond
794 * The condition to be waited upon until a signal is given
795 * @param *mutex
796 * The mutex used to lock other threads out
797 * @return Returns 0 upon successful completion, EINVAL upon non-robust mutex input
798 */
799
800int pthread_cond_wait(pthread_cond_t *cond, pthread_mutex_t *mutex){
801 if(mutex->owner != $self){
802 printf("Mutex not owned by thread");
803 $assert($false);
804 return 0;
805 }
806
807 cond->proccount= cond->proccount+1;
808 cond->signal = false;
809 pthread_mutex_unlock(mutex);
810
811 $when(cond->signal);
812 cond->signal = false;
813 --cond->proccount;
814 $when(mutex->lock == 0){pthread_mutex_lock(mutex);}
815 return 0;
816}
817
818/**
819 * Signals the condition by setting the signal to true
820 * Corresponding specification: p. 1627-30
821 *
822 * @param *cond
823 * The condition to be signalled
824 * @return Returns 0 upon successful completion
825 */
826
827int pthread_cond_signal(pthread_cond_t *cond){
828 cond->signal = true;
829 return 0;
830}
831
832/**
833 * Repeated signals the condition until all processes waiting have been signalled and awoken
834 * Corresponding specification: p. 1627-30
835 *
836 * @param *cond
837 * The condition to be signalled repeatedly
838 * @return Returns 0 upon successful completion
839 */
840
841int pthread_cond_broadcast(pthread_cond_t *cond){
842 while(cond->proccount > 0){
843 cond->signal = true;
844 }
845 return 0;
846}
Note: See TracBrowser for help on using the repository browser.