source: CIVL/examples/translation/pthread/pthread.cvh@ 50f834b

1.23 2.0 main test-branch
Last change on this file since 50f834b was 5fb1a47, checked in by Manchun Zheng <zmanchun@…>, 12 years ago

added pthread examples

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

  • Property mode set to 100755
File size: 2.0 KB
Line 
1#include <civlc.h>
2#include <stdio.h>
3#include <stdlib.h>
4#include <assert.h>
5#include <stdbool.h>
6
7#define PTHREAD_MUTEX_DEFAULT 0
8#define PTHREAD_MUTEX_NORMAL 0
9#define PTHREAD_MUTEX_RECURSIVE 1
10#define PTHREAD_MUTEX_ERRORCHECK 2
11#define PTHREAD_MUTEX_INITIALIZER \
12 {0,0,0,PTHREAD_MUTEX_NORMAL,__LOCK_INITIALIZER}
13#define __LOCK_INITIALIZER { 0, 0 }
14#define PTHREAD_COND_INITIALIZER {__LOCK_INITIALIZER,0}
15
16typedef $proc pthread_t;
17
18typedef struct {
19 int count;
20 $proc owner;
21 int lock;
22 int kind;
23} pthread_mutex_t;
24
25typedef struct {
26 void *stackaddr;
27 size_t stacksize;
28 int detachstate;
29 int param;
30 int inheritsched;
31 int contentionscope;
32}pthread_attr_t;
33
34typedef struct {
35 int proccount;
36 _Bool signal;
37} pthread_cond_t;
38
39void pthread_cond_init(pthread_cond_t *cond, int kind){
40 cond->proccount = 0;
41 cond->signal = false;
42}
43
44//Initializes mutex as unlocked and kind as defined by int m
45void pthread_mutex_init(pthread_mutex_t *mutex, int m){
46 mutex->kind = m;
47 mutex->lock = 0;
48}
49
50int pthread_mutex_lock(pthread_mutex_t *mutex) {
51 $when(mutex->lock == 0) mutex->lock = 1;
52 mutex->owner = $self;
53 return 0;
54}
55
56
57int pthread_mutex_unlock(pthread_mutex_t *mutex) {
58 mutex->lock = 0;
59 return 0;
60}
61
62int pthread_cond_wait(pthread_cond_t *cond, pthread_mutex_t *mutex){
63 if(mutex->owner != $self)
64 {
65 printf("Mutex not owned by thread");
66 $assert($false);
67 return 0;
68 }
69 cond->proccount++;
70 pthread_mutex_unlock(mutex);
71 $when(cond->signal == true);
72 cond->signal = false;
73 --cond->proccount;
74 $when(mutex->lock == 0){pthread_mutex_lock(mutex);}
75}
76
77int pthread_cond_signal(pthread_cond_t *cond){
78 cond->signal = true;
79}
80
81int pthread_cond_broadcast(pthread_cond_t *cond){
82 while(cond->proccount > 0){
83 cond->signal = true;
84 }
85}
86
87int pthread_create(pthread_t *thread, const pthread_attr_t *attr,
88 void *(*start_routine)(void*), void *arg){
89 *thread = $spawn start_routine(arg);
90 return 0;
91}
92
93int pthread_join(pthread_t thread, void **value_ptr) {
94 $wait(thread);
95 return 0;
96}
97
Note: See TracBrowser for help on using the repository browser.