Skip to content

Commit

Permalink
Merge pull request #142 from LChenGit/delaware
Browse files Browse the repository at this point in the history
delaware dataset part3
  • Loading branch information
chunhualiao authored Jul 11, 2023
2 parents 5e2d58f + b204677 commit 7d07c5d
Show file tree
Hide file tree
Showing 22 changed files with 620 additions and 12 deletions.
32 changes: 20 additions & 12 deletions benchmarkList.md
Original file line number Diff line number Diff line change
Expand Up @@ -105,12 +105,16 @@ DRB178-input-dependence-var-yes.c |Y1 | Input dependence r
DRB179-thread-sensitivity-yes.cc |Y6 | Conflicting writes to same address | New
DRB180-miniAMR-yes.c |Y6 | Race by shared index variable | MiniAMR app
DRB181-SmithWaterman-yes.c |Y6 | Race appears with larger data size | Smith-Waterman app
DRB183-atomic3_yes.c |Y3 | Races because the write is not protected by atomic | [Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB185-bar1_yes.c |Y3 | wrong 2-thread flag barrier using busy-waits, race [inline] |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB187-bar2_yes.c |Y3 | each thread uses its own lock, which doesn't work |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB189-bar3_yes.c |Y3 | one synchronization missed [inline] |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB191-critsec2_yes.c |Y3 | has race due to different critical section names |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB193-critsec3_yes.c |Y3 | has race due to different critical section names |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB183-atomic3-yes.c |Y3 | Races because the write is not protected by atomic | [Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB185-bar1-yes.c |Y3 | wrong 2-thread flag barrier using busy-waits | [Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB187-bar2-yes.c |Y3 | each thread uses its own lock, which doesn't work | [Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB189-bar3-yes.c |Y3 | one synchronization missed | [Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB191-critsec2-yes.c |Y3 | has race due to different critical section names | [Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB193-critsec3-yes.c |Y3 | has race due to different critical section names | [Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB195-diffusion1-yes.c |Y3 | has race due to the missing of proper synchronization when u1 and u2 are alias | [Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB197-diffusion2-yes.c |Y2 | has race due to the missing of proper synchronization | [Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB199-prodcons-yes.c |Y3 | races due to critical sections have different names | [Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB201-sync1-yes.c |Y3 | t1 can set then unset while setting t0. Both are write operations. | [Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
# Microbenchmarks without known data races

Microbenchmark |P-Label | Description | Source
Expand Down Expand Up @@ -206,9 +210,13 @@ DRB171-threadprivate3-orig-no.c |N1 | example of a threadprivate var
DRB172-critical2-orig-no.c |N2, N3 | Use of private and explicit barrier tto ensure no data race. | NAS Benchmark
DRB174-non-sibling-taskdep-no.c |N3 | Use of taskwait ensures no data race. | New
DRB176-fib-taskdep-no.c |N3 | Fibonacci code with proper task dependency. | Fibonacci code
DRB182-atomic3_no.c |N3 | sync with busy wait loop using atomic |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB184-bar1_no.c |N3 | 2-thread flag barrier using busy-wait loops and critical, no race |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB186-bar2_no.c |N3 | uses locks to create a barrier that is used once |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB188-bar3_no.c |N3 | implements 2-thread reuseable barrier using 3 locks, no race |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB190-critsec2_no.c |N2, N3 | single producer single consumer with critical sections |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB192-critsec3_no.c |N2, N3 | signal with busy wait loop using critical sections |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB182-atomic3-no.c |N3 | sync with busy wait loop using atomic |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB184-bar1-no.c |N3 | 2-thread flag barrier using busy-wait loops and critical, no race |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB186-bar2-no.c |N3 | uses locks to create a barrier that is used once |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB188-bar3-no.c |N3 | implements 2-thread reuseable barrier using 3 locks, no race |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB190-critsec2-no.c |N2, N3 | single producer single consumer with critical sections |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB192-critsec3-no.c |N2, N3 | signal with busy wait loop using critical sections |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB194-diffusion1-no.c |N1 | signal with busy wait loop using critical sections |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB196-diffusion2-no.c |N1 | similar to diffusion1, but two parts of one malloced object used |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB198-prodcons-no.c |N1 | multiple producer, multiple consumer with critical sections |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
DRB200-sync1-no.c |N3 | two threads sync using one lock |[Sequential Consistency for Data-race-free Programs](https://github.com/verified-software-lab/sc4drf/tree/main/experiments/civl/extra)
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
46 changes: 46 additions & 0 deletions micro-benchmarks/DRB194-diffusion1-no.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
/*
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
!!! Copyright (c) 2017-20, Lawrence Livermore National Security, LLC
!!! and DataRaceBench project contributors. See the DataRaceBench/COPYRIGHT file for details.
!!!
!!! SPDX-License-Identifier: (BSD-3-Clause)
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
*/

/*
* This is a program based on a dataset contributed by
* Wenhao Wu and Stephen F. Siegel @Univ. of Delaware.
* no race, but it needs to mention that u1 and u2 are not aliased
*/

#include <stdlib.h>
#include <stdio.h>

double *u1, *u2, c = 0.2;
int n = 10, nsteps = 10;

int main()
{
u1 = malloc(n * sizeof(double));
u2 = malloc(n * sizeof(double));
for (int i = 1; i < n - 1; i++)
u2[i] = u1[i] = 1.0 * rand() / RAND_MAX;
u1[0] = u1[n - 1] = u2[0] = u2[n - 1] = 0.5;
for (int t = 0; t < nsteps; t++)
{
#pragma omp parallel for
for (int i = 1; i < n - 1; i++)
{
u2[i] = u1[i] + c * (u1[i - 1] + u1[i + 1] - 2 * u1[i]);
}
double *tmp = u1;
u1 = u2;
u2 = tmp;
}
for (int i = 0; i < n; i++)
printf("%1.2lf ", u1[i]);
printf("\n");
free(u1);
free(u2);
}
49 changes: 49 additions & 0 deletions micro-benchmarks/DRB195-diffusion1-yes.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
/*
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
!!! Copyright (c) 2017-20, Lawrence Livermore National Security, LLC
!!! and DataRaceBench project contributors. See the DataRaceBench/COPYRIGHT file for details.
!!!
!!! SPDX-License-Identifier: (BSD-3-Clause)
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
*/

/*
* This is a program based on a dataset contributed by
* Wenhao Wu and Stephen F. Siegel @Univ. of Delaware.
* Race due to u1 and u2 are aliased.
* Data race pairs: u2[i]@39:7:W vs. u1[i]@39:15:R
* u2[i]@39:7:W vs. u1[i - 1]@39:28:R
* u2[i]@39:7:W vs. u1[i + 1]@39:40:R
* u2[i]@39:7:W vs. u1[i]@39:56:R
*/

#include <stdlib.h>
#include <stdio.h>

double *u1, *u2, c = 0.2;
int n = 10, nsteps = 10;

int main()
{
u1 = malloc(n * sizeof(double));
u2 = malloc(n * sizeof(double));
for (int i = 1; i < n - 1; i++)
u2[i] = u1[i] = 1.0 * rand() / RAND_MAX;
u1[0] = u1[n - 1] = u2[0] = u2[n - 1] = 0.5;
for (int t = 0; t < nsteps; t++)
{
#pragma omp parallel for
for (int i = 1; i < n - 1; i++)
{
u2[i] = u1[i] + c * (u1[i - 1] + u1[i + 1] - 2 * u1[i]);
}
double *tmp = u1;
u1 = u2; // u2 = tmp;
}
for (int i = 0; i < n; i++)
printf("%1.2lf ", u1[i]);
printf("\n");
free(u1);
free(u2);
}
44 changes: 44 additions & 0 deletions micro-benchmarks/DRB196-diffusion2-no.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
/*
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
!!! Copyright (c) 2017-20, Lawrence Livermore National Security, LLC
!!! and DataRaceBench project contributors. See the DataRaceBench/COPYRIGHT file for details.
!!!
!!! SPDX-License-Identifier: (BSD-3-Clause)
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
*/

/*
* This is a program based on a dataset contributed by
* Wenhao Wu and Stephen F. Siegel @Univ. of Delaware.
* No race. The array b is divided into two non-overlapping halves that are referenced by u[0] and u[1].
*/

#include <stdlib.h>
#include <stdio.h>

double c = 0.2;
int n = 20, nsteps = 100;

int main()
{
double *b = malloc(2 * n * sizeof(double));
double *u[2] = {&b[0], &b[n]};
for (int i = 1; i < n - 1; i++)
u[0][i] = u[1][i] = 1.0 * rand() / RAND_MAX;
u[0][0] = u[0][n - 1] = u[1][0] = u[1][n - 1] = 0.5;
int p = 0;
for (int t = 0; t < nsteps; t++)
{
#pragma omp parallel for
for (int i = 1; i < n - 1; i++)
{
u[1 - p][i] = u[p][i] + c * (u[p][i - 1] + u[p][i + 1] - 2 * u[p][i]);
}
p = 1 - p;
}
for (int i = 0; i < n; i++)
printf("%1.2lf ", u[p][i]);
printf("\n");
free(b);
}
46 changes: 46 additions & 0 deletions micro-benchmarks/DRB197-diffusion2-yes.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
/*
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
!!! Copyright (c) 2017-20, Lawrence Livermore National Security, LLC
!!! and DataRaceBench project contributors. See the DataRaceBench/COPYRIGHT file for details.
!!!
!!! SPDX-License-Identifier: (BSD-3-Clause)
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
*/

/*
* This is a program based on a dataset contributed by
* Wenhao Wu and Stephen F. Siegel @Univ. of Delaware.
* Overlap of the two ranges u[0] and u[1] when u[1][i] is accessed.
* Data race pairs: u[1 - p][i]@38:7:W vs. u[p][i - 1]@38:15:R
* u[1 - p][i]@38:7:W vs. u[p][i + 1]@38:50:R
*/

#include <stdlib.h>
#include <stdio.h>

double c = 0.2;
int n = 20, nsteps = 100;

int main()
{
double *b = malloc(2 * n * sizeof(double));
double *u[2] = {&b[0], &b[n - 2]}; // oops, should be b[n]
for (int i = 1; i < n - 1; i++)
u[0][i] = u[1][i] = 1.0 * rand() / RAND_MAX;
u[0][0] = u[0][n - 1] = u[1][0] = u[1][n - 1] = 0.5;
int p = 0;
for (int t = 0; t < nsteps; t++)
{
#pragma omp parallel for
for (int i = 1; i < n - 1; i++)
{
u[1 - p][i] = u[p][i] + c * (u[p][i - 1] + u[p][i + 1] - 2 * u[p][i]);
}
p = 1 - p;
}
for (int i = 0; i < n; i++)
printf("%1.2lf ", u[p][i]);
printf("\n");
free(b);
}
49 changes: 49 additions & 0 deletions micro-benchmarks/DRB198-prodcons-no.c.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
/*
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
!!! Copyright (c) 2017-20, Lawrence Livermore National Security, LLC
!!! and DataRaceBench project contributors. See the DataRaceBench/COPYRIGHT file for details.
!!!
!!! SPDX-License-Identifier: (BSD-3-Clause)
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
*/

/*
* This is a program based on a dataset contributed by
* Wenhao Wu and Stephen F. Siegel @Univ. of Delaware.
* no race
*/

#include <stdio.h>
int nprod = 4, ncons = 4;
int cap = 5, size = 0;
int main()
{
int nthread = nprod + ncons;
#pragma omp parallel for shared(size, cap, nprod, ncons, nthread) num_threads(nthread)
for (int i = 0; i < nthread; i++)
{
if (i < nprod)
while (1)
{ // I am a producer
#pragma omp critical
if (size < cap)
{
size++; // produce
printf("Producer %d produced! size=%d\n", i, size);
fflush(stdout);
}
}
else
while (1)
{ // I am a consumer
#pragma omp critical
if (size > 0)
{
size--; // consume
printf("Consumer %d consumed! size=%d\n", i - nprod, size);
fflush(stdout);
}
}
}
}
51 changes: 51 additions & 0 deletions micro-benchmarks/DRB199-prodcons-yes.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
/*
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
!!! Copyright (c) 2017-20, Lawrence Livermore National Security, LLC
!!! and DataRaceBench project contributors. See the DataRaceBench/COPYRIGHT file for details.
!!!
!!! SPDX-License-Identifier: (BSD-3-Clause)
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
*/

/*
* This is a program based on a dataset contributed by
* Wenhao Wu and Stephen F. Siegel @Univ. of Delaware.
* race introduced because critical sections have different names for producer and consumer.
* Data race pair: size@34:11:W vs. size@45:11:W
*/

#include <stdio.h>
#include <stdio.h>
int nprod = 4, ncons = 4;
int cap = 5, size = 0;
int main()
{
int nthread = nprod + ncons;
#pragma omp parallel for shared(size, cap, nprod, ncons, nthread) num_threads(nthread)
for (int i = 0; i < nthread; i++)
{
if (i < nprod)
while (1)
{ // I am a producer
#pragma omp critical(A)
if (size < cap)
{
size++; // produce
printf("Producer %d produced! size=%d\n", i, size);
fflush(stdout);
}
}
else
while (1)
{ // I am a consumer
#pragma omp critical(B)
if (size > 0)
{
size--; // consume
printf("Consumer %d consumed! size=%d\n", i - nprod, size);
fflush(stdout);
}
}
}
}
48 changes: 48 additions & 0 deletions micro-benchmarks/DRB200-sync1-no.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
/*
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
!!! Copyright (c) 2017-20, Lawrence Livermore National Security, LLC
!!! and DataRaceBench project contributors. See the DataRaceBench/COPYRIGHT file for details.
!!!
!!! SPDX-License-Identifier: (BSD-3-Clause)
!!!~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~!!!
*/

/*
* This is a program based on a dataset contributed by
* Wenhao Wu and Stephen F. Siegel @Univ. of Delaware.
* Two threads sync using one lock. No race.
*/

#include <stdio.h>
#include <omp.h>
#include <assert.h>

omp_lock_t l;
int x = 1;

int main()
{
omp_init_lock(&l);
#pragma omp parallel num_threads(2)
{
int tid = omp_get_thread_num();
if (tid == 0)
omp_set_lock(&l);
#pragma omp barrier
if (tid == 0)
{
x = 0;
omp_unset_lock(&l);
}
else if (tid == 1)
{
omp_set_lock(&l);
omp_unset_lock(&l);
x = 1;
}
#pragma omp barrier
} // end of parallel construct
omp_destroy_lock(&l);
printf("Done: x=%d\n", x);
}
Loading

0 comments on commit 7d07c5d

Please sign in to comment.