source: CIVL/examples/pthread/cprover/20_lamport_true.c@ 1aaefd4

main test-branch
Last change on this file since 1aaefd4 was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

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

  • Property mode set to 100644
File size: 1.1 KB
Line 
1#include <pthread.h>
2
3#define assert(e) { if(!(e)) { ERROR: goto ERROR; (void)0; } }
4
5int x;
6int y;
7int b1, b2; // N boolean flags
8int X; //variable to test mutual exclusion
9
10void* thr1(void* arg) {
11 while (1) {
12 b1 = 1;
13 x = 1;
14 if (y != 0) {
15 b1 = 0;
16 while (y != 0) {};
17 continue;
18 }
19 y = 1;
20 if (x != 1) {
21 b1 = 0;
22 while (b2 >= 1) {};
23 if (y != 1) {
24 while (y != 0) {};
25 continue;
26 }
27 }
28 break;
29 }
30 // begin: critical section
31 X = 0;
32 assert(X <= 0);
33 // end: critical section
34 y = 0;
35 b1 = 0;
36
37 return 0;
38}
39
40void* thr2(void* arg) {
41 while (1) {
42 b2 = 1;
43 x = 2;
44 if (y != 0) {
45 b2 = 0;
46 while (y != 0) {};
47 continue;
48 }
49 y = 2;
50 if (x != 2) {
51 b2 = 0;
52 while (b1 >= 1) {};
53 if (y != 2) {
54 while (y != 0) {};
55 continue;
56 }
57 }
58 break;
59 }
60 // begin: critical section
61 X = 1;
62 assert(X >= 1);
63 // end: critical section
64 y = 0;
65 b2 = 0;
66
67 return 0;
68}
69
70int main()
71{
72 pthread_t t;
73
74 pthread_create(&t, 0, thr1, 0);
75 thr2(0);
76
77 return 0;
78}
79
Note: See TracBrowser for help on using the repository browser.