projects
/
lttv.git
/ blob
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
blame
|
history
|
raw
|
HEAD
update verif
[lttv.git]
/
trunk
/
verif
/
examples
/
spin-increment.spin
1
#define NUMPROCS 2
2
3
byte counter = 0;
4
byte progress[NUMPROCS];
5
6
proctype incrementer(byte me)
7
{
8
int temp;
9
10
temp = counter;
11
counter = temp + 1;
12
progress[me] = 1;
13
}
14
15
init {
16
int i = 0;
17
int sum = 0;
18
19
atomic {
20
i = 0;
21
do
22
:: i < NUMPROCS ->
23
progress[i] = 0;
24
run incrementer(i);
25
i++
26
:: i >= NUMPROCS -> break
27
od;
28
}
29
atomic {
30
i = 0;
31
sum = 0;
32
do
33
:: i < NUMPROCS ->
34
sum = sum + progress[i];
35
i++
36
:: i >= NUMPROCS -> break
37
od;
38
assert(sum < NUMPROCS || counter == NUMPROCS)
39
}
40
}
This page took
0.030014 seconds
and
4
git commands to generate.