main
|
Last change
on this file was 4491cfb, checked in by Stephen Siegel <siegel@…>, 2 years ago |
|
Fixed bug in POR. It involved the computation of reachable memory. To compute reachable for a proc, you have to iterate over its call stack and accumulate all the dyscopes reachable from each frame. That part was right. Once you have those dyscopes, you have to add all the variables in them to a set which is the result. That part was incorrect.
The old code would only add the variable if it is reachable from the top frame of the call stack. It was a no-op if the variable is reachable from some other frame but not from the top frame.
The bug was revealed by example doubleBarrierBad.cvl.
Fixed now.
git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5883 fb995dde-84ed-4084-dfe6-e5aef3e2452c
|
-
Property mode
set to
100644
|
|
File size:
480 bytes
|
| Rev | Line | |
|---|
| [7ffcb1b] | 1 | #include <concurrency.cvh>
|
|---|
| [4491cfb] | 2 | #include <stdio.h>
|
|---|
| [7ffcb1b] | 3 |
|
|---|
| 4 | $gbarrier gbarrier = $gbarrier_create($here, 2);
|
|---|
| 5 |
|
|---|
| 6 | int main() {
|
|---|
| [4491cfb] | 7 | int a;
|
|---|
| [7ffcb1b] | 8 | void foo(int id) {
|
|---|
| 9 | $barrier b = $barrier_create($here, gbarrier, id);
|
|---|
| 10 | $barrier_call(b);
|
|---|
| [4491cfb] | 11 | printf("Hello from thread %d\n", id);
|
|---|
| 12 | a=id;
|
|---|
| 13 | $barrier_call(b);
|
|---|
| 14 | printf("a=%d\n", a);
|
|---|
| 15 | $assert(a==1);
|
|---|
| [7ffcb1b] | 16 | $barrier_destroy(b);
|
|---|
| 17 | }
|
|---|
| 18 | $proc p0 = $spawn foo(0);
|
|---|
| 19 | $proc p1 = $spawn foo(1);
|
|---|
| 20 | $wait(p0);
|
|---|
| 21 | $wait(p1);
|
|---|
| 22 | $gbarrier_destroy(gbarrier);
|
|---|
| 23 | }
|
|---|
Note:
See
TracBrowser
for help on using the repository browser.
