diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-09-18 14:40:45 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-18 14:40:45 +0100 |
commit | b666f88219893c82361606f8652297ecc7fb7a9f (patch) | |
tree | 946c2ddb5ce21b7af24ce6945fe5f83cbb274061 /benchmarks/polybench-syn-div/stencils | |
parent | c4d44af5f3135aba4d4878f8f41c80d1f0b9e9a2 (diff) | |
parent | c4436c02648502c4cb327d2018229e62a2c0d1c0 (diff) | |
download | vericert-b666f88219893c82361606f8652297ecc7fb7a9f.tar.gz vericert-b666f88219893c82361606f8652297ecc7fb7a9f.zip |
Merge branch 'master' into develop
Diffstat (limited to 'benchmarks/polybench-syn-div/stencils')
-rw-r--r-- | benchmarks/polybench-syn-div/stencils/Makefile | 6 | ||||
-rw-r--r-- | benchmarks/polybench-syn-div/stencils/adi.c | 125 | ||||
-rw-r--r-- | benchmarks/polybench-syn-div/stencils/fdtd-2d.c | 134 | ||||
-rw-r--r-- | benchmarks/polybench-syn-div/stencils/heat-3d.c | 112 | ||||
-rw-r--r-- | benchmarks/polybench-syn-div/stencils/jacobi-1d.c | 101 | ||||
-rw-r--r-- | benchmarks/polybench-syn-div/stencils/jacobi-2d.c | 108 | ||||
-rw-r--r-- | benchmarks/polybench-syn-div/stencils/seidel-2d.c | 92 |
7 files changed, 678 insertions, 0 deletions
diff --git a/benchmarks/polybench-syn-div/stencils/Makefile b/benchmarks/polybench-syn-div/stencils/Makefile new file mode 100644 index 0000000..d2e1c9b --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/Makefile @@ -0,0 +1,6 @@ +TARGETS := adi fdtd-2d heat-3d jacobi-1d jacobi-2d seidel-2d + +include ../common.mk + +adi.v: adi.c + $(VERICERT) $(VERICERT_OPTS) -O0 -finline $< -o $@ diff --git a/benchmarks/polybench-syn-div/stencils/adi.c b/benchmarks/polybench-syn-div/stencils/adi.c new file mode 100644 index 0000000..be2b766 --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/adi.c @@ -0,0 +1,125 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* adi.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +static +void init_array (int n, int u[ 20 + 0][20 + 0]) +{ + int i, j; + + for (i = 0; i < n; i++) + for (j = 0; j < n; j++) + { + u[i][j] = (((int)(i + n-j)) / n); + } +} + + + + +static +int print_array(int n, int u[ 20 + 0][20 + 0]) +{ + int i, j; + int res = 0; + + for (i = 0; i < n; i++) + for (j = 0; j < n; j++) { + res ^= u[i][j]; + } +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif + + return res; +} +static +void kernel_adi(int tsteps, int n, + int u[ 20 + 0][20 + 0], + int v[ 20 + 0][20 + 0], + int p[ 20 + 0][20 + 0], + int q[ 20 + 0][20 + 0]) +{ + int t, i, j; + int B1, B2; + int mul1, mul2; + int a, b, c, d, e, f; + + B1 = 2; + B2 = 1; + mul1 = ((B1 * n * n) / tsteps); + mul2 = ((B2 * n * n) /tsteps); + + a = -((mul1 / 2)); + b = 1+mul1; + c = a; + d = -((mul2 / 2)); + e = 1+mul2; + f = d; + int ZERO = 0; + + for (t=1; t<=tsteps; t++) { + + for (i=1; i<n-1; i++) { + v[ZERO][i] = 1; + p[i][ZERO] = 0; + q[i][ZERO] = v[ZERO][i]; + for (j=1; j<n-1; j++) { + p[i][j] = -(c / (a*p[i][j-1]+b)); + q[i][j] = -((-d*u[j][i-1]+(1+2*d)*u[j][i] - f*u[j][i+1]-a*q[i][j-1]) / (a*p[i][j-1]+b)); + } + + v[n-1][i] = 1; + for (j=n-2; j>=1; j--) { + v[j][i] = p[i][j] * v[j+1][i] + q[i][j]; + } + } + + for (i=1; i<n-1; i++) { + u[i][ZERO] = 1; + p[i][ZERO] = 0; + q[i][ZERO] = u[i][ZERO]; + for (j=1; j<n-1; j++) { + p[i][j] = -(f / (d*p[i][j-1]+e)); + q[i][j] = ((-a*v[i-1][j]+(1+2*a)*v[i][j] - c*v[i+1][j]-d*q[i][j-1]) / (d*p[i][j-1]+e)); + } + u[i][n-1] = 1; + for (j=n-2; j>=1; j--) { + u[i][j] = p[i][j] * u[i][j+1] + q[i][j]; + } + } + } +} + +int main() +{ + + int n = 20; + int tsteps = 20; + + + int u[20 + 0][20 + 0]; + int v[20 + 0][20 + 0]; + int p[20 + 0][20 + 0]; + int q[20 + 0][20 + 0]; + + + + init_array (n, u); + + kernel_adi (tsteps, n, u, v, p, q); + + return print_array(n, u); + +} diff --git a/benchmarks/polybench-syn-div/stencils/fdtd-2d.c b/benchmarks/polybench-syn-div/stencils/fdtd-2d.c new file mode 100644 index 0000000..2c5cdb2 --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/fdtd-2d.c @@ -0,0 +1,134 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* fdtd-2d.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array (int tmax, + int nx, + int ny, + int ex[ 20 + 0][30 + 0], + int ey[ 20 + 0][30 + 0], + int hz[ 20 + 0][30 + 0], + int _fict_[ 20 + 0]) +{ + int i, j; + int ONE = 1; + + for (i = 0; i < tmax; plus(i)) + _fict_[i] = (int) i; + for (i = 0; i < nx; plus(i)) + for (j = 0; j < ny; plus(j)) + { + ex[i][j] = ((i*(j+1)) / nx); + ey[i][j] = ((i*(j+2)) / ny); + hz[i][j] = ((i*(j+3)) / nx); + } + +} + + + + +static +int print_array(int nx, + int ny, + int ex[ 20 + 0][30 + 0], + int ey[ 20 + 0][30 + 0], + int hz[ 20 + 0][30 + 0]) +{ + int i, j; + int res = 0; + int ONE = 1; + + for (i = 0; i < nx; plus(i)) + for (j = 0; j < ny; plus(j)) { + res ^= ex[i][j]; + } + for (i = 0; i < nx; plus(i)) + for (j = 0; j < ny; plus(j)) { + res ^= ey[i][j]; + } + for (i = 0; i < nx; plus(i)) + for (j = 0; j < ny; plus(j)) { + res ^= hz[i][j]; + } + +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif + + return res; +} + + +static +void kernel_fdtd_2d(int tmax, + int nx, + int ny, + int ex[ 20 + 0][30 + 0], + int ey[ 20 + 0][30 + 0], + int hz[ 20 + 0][30 + 0], + int _fict_[ 20 + 0]) +{ + int t, i, j; + int ONE = 1; + + for(t = 0; t < tmax; t=t+ONE) + { + for (j = 0; j < ny; plus(j)) + ey[0][j] = _fict_[t]; + for (i = 1; i < nx; plus(i)) + for (j = 0; j < ny; plus(j)) + ey[i][j] = ey[i][j] - ((hz[i][j]-((hz[i-ONE][j])>>1))); + for (i = 0; i < nx; plus(i)) + for (j = 1; j < ny; plus(j)) + ex[i][j] = ex[i][j] - ((hz[i][j]-((hz[i][j-ONE])>>1))); + for (i = 0; i < nx - ONE; plus(i)) + for (j = 0; j < ny - ONE; plus(j)){ + int tmp = (ex[i][j+ONE] - ex[i][j] + + ey[i+ONE][j] - ey[i][j]); + hz[i][j] = hz[i][j] - (tmp >> 1) - (tmp >> 2); + } + } + +} + + +int main() +{ + + int tmax = 20; + int nx = 20; + int ny = 30; + + + int ex[20 + 0][30 + 0]; + int ey[20 + 0][30 + 0]; + int hz[20 + 0][30 + 0]; + int _fict_[20 + 0]; + + init_array (tmax, nx, ny, + ex, + ey, + hz, + _fict_); + kernel_fdtd_2d (tmax, nx, ny, + ex, + ey, + hz, + _fict_); + + return print_array(nx, ny, ex, ey, hz); +} diff --git a/benchmarks/polybench-syn-div/stencils/heat-3d.c b/benchmarks/polybench-syn-div/stencils/heat-3d.c new file mode 100644 index 0000000..f93082e --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/heat-3d.c @@ -0,0 +1,112 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* heat-3d.c: this file is part of PolyBench/C */ + +#include "../include/misc.h" + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array (int n, + int A[ 10 + 0][10 + 0][10 + 0], + int B[ 10 + 0][10 + 0][10 + 0]) +{ + int i, j, k; + int ONE = 1; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + for (k = 0; k < n; plus(k)) + A[i][j][k] = B[i][j][k] = (int) (i + j + (n-k))* (10 / n); +} + + + + +static +int print_array(int n, + int A[ 10 + 0][10 + 0][10 + 0]) + +{ + int i, j, k; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + for (k = 0; k < n; plus(k)) { + res ^= A[i][j][k]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_heat_3d(int tsteps, + int n, + int A[ 10 + 0][10 + 0][10 + 0], + int B[ 10 + 0][10 + 0][10 + 0]) +{ + int t, i, j, k; + int ONE = 1; + int TWO = 2; + + for (t = 1; t <= 5; plus(t)) { + for (i = 1; i < n-ONE; plus(i)) { + for (j = 1; j < n-ONE; plus(j)) { + for (k = 1; k < n-ONE; plus(k)) { + B[i][j][k] = ((A[i+ONE][j][k] - TWO * A[i][j][k] + A[i-ONE][j][k]) >> 4) + + ((A[i][j+ONE][k] - TWO * A[i][j][k] + A[i][j-ONE][k]) >> 4) + + ((A[i][j][k+ONE] - TWO * A[i][j][k] + A[i][j][k-ONE]) >> 4) + + A[i][j][k] + ; + } + } + } + for (i = 1; i < n-ONE; plus(i)) { + for (j = 1; j < n-ONE; plus(j)) { + for (k = 1; k < n-ONE; plus(k)) { + A[i][j][k] = ((B[i+ONE][j][k] - TWO * B[i][j][k] + B[i-ONE][j][k]) >> 4 ) + + ((B[i][j+ONE][k] - TWO * B[i][j][k] + B[i][j-ONE][k]) >> 4 ) + + ((B[i][j][k+ONE] - TWO * B[i][j][k] + B[i][j][k-ONE]) >> 4 ) + + B[i][j][k]; + //; + } + } + } + } +} + + +int main() +{ + + int n = 10; + int tsteps = 20; + + + int A[10 + 0][10 + 0][10 + 0]; + int B[10 + 0][10 + 0][10 + 0]; + + init_array (n, A, B); + + kernel_heat_3d (tsteps, n, A, B); + + return print_array(n, A); + +} diff --git a/benchmarks/polybench-syn-div/stencils/jacobi-1d.c b/benchmarks/polybench-syn-div/stencils/jacobi-1d.c new file mode 100644 index 0000000..993773e --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/jacobi-1d.c @@ -0,0 +1,101 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* jacobi-1d.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array (int n, + int A[ 30 + 0], + int B[ 30 + 0]) +{ + int i; + int ONE = 1; + int TWO = 2; + int THREE = 3; + + for (i = 0; i < n; plus(i)) + { + A[i] = (((int) i+TWO) / n); + B[i] = (((int) i+THREE) / n); + } +} + + + + +static +int print_array(int n, + int A[ 30 + 0]) + +{ + int i; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) + { + res ^= A[i]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_jacobi_1d(int tsteps, + int n, + int A[ 30 + 0], + int B[ 30 + 0]) +{ + int t, i; + int ONE = 1; + + for (t = 0; t < tsteps; plus(t)) + { + for (i = 1; i < n - ONE; plus(i)){ + B[i] = (A[i-ONE] + A[i] + A[i + ONE]); + B[i] = B[i] >> 2; + } + for (i = 1; i < n - ONE; plus(i)){ + A[i] = (B[i-ONE] + B[i] + B[i + ONE]); + A[i] = A[i] >> 2; + } + } + +} + + +int main() +{ + + int n = 30; + int tsteps = 20; + + + int A[30 + 0]; + int B[30 + 0]; + + + + init_array (n, A, B); + + kernel_jacobi_1d(tsteps, n, A, B); + + return print_array(n, A); + +} diff --git a/benchmarks/polybench-syn-div/stencils/jacobi-2d.c b/benchmarks/polybench-syn-div/stencils/jacobi-2d.c new file mode 100644 index 0000000..bb6afec --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/jacobi-2d.c @@ -0,0 +1,108 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* jacobi-2d.c: this file is part of PolyBench/C */ + +#include "../include/misc.h" + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + + +#define plus(i) i = i + ONE +static +void init_array (int n, + int A[ 30 + 0][30 + 0], + int B[ 30 + 0][30 + 0]) +{ + int i, j; + int ONE = 1; + int TWO = 2; + int THREE = 3; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + { + A[i][j] = (((int) i*(j+TWO) + TWO) / n); + B[i][j] = (((int) i*(j+THREE) + THREE) / n); + } +} + + + + +static +int print_array(int n, + int A[ 30 + 0][30 + 0]) + +{ + int i, j; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) { + res ^= A[i][j]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_jacobi_2d(int tsteps, + int n, + int A[ 30 + 0][30 + 0], + int B[ 30 + 0][30 + 0]) +{ + int t, i, j; + int ONE = 1; + int TWO = 2; + + for (t = 0; t < tsteps; plus(t)) + { + for (i = 1; i < n - ONE; plus(i)) + for (j = 1; j < n - ONE; plus(j)){ + B[i][j] = (A[i][j] + A[i][j-ONE] + A[i][ONE+j] + A[ONE+i][j] + A[i-ONE][j]); + B[i][j] = B[i][j] >> TWO; + } + for (i = 1; i < n - ONE; plus(i)) + for (j = 1; j < n - ONE; plus(j)){ + A[i][j] = (B[i][j] + B[i][j-ONE] + B[i][ONE+j] + B[ONE+i][j] + B[i-ONE][j]); + A[i][j] = A[i][j] >> TWO; + } + } + +} + + +int main() +{ + + int n = 30; + int tsteps = 5; + + + int A[30 + 0][30 + 0]; + int B[30 + 0][30 + 0]; + + + + init_array (n, A, B); + + kernel_jacobi_2d(tsteps, n, A, B); + + return print_array(n, A); + +} diff --git a/benchmarks/polybench-syn-div/stencils/seidel-2d.c b/benchmarks/polybench-syn-div/stencils/seidel-2d.c new file mode 100644 index 0000000..4a3b1ac --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/seidel-2d.c @@ -0,0 +1,92 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* seidel-2d.c: this file is part of PolyBench/C */ + +#include "../include/misc.h" + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array (int n, + int A[ 40 + 0][40 + 0]) +{ + int i, j; + int ONE = 1; + int TWO = 2; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + A[i][j] = (((int) i*(j+TWO) + TWO) / n); +} + + + + +static +int print_array(int n, + int A[ 40 + 0][40 + 0]) + +{ + int i, j; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) { + res ^= A[i][j]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_seidel_2d(int tsteps, + int n, + int A[ 40 + 0][40 + 0]) +{ + int t, i, j; + int ONE = 1; + int TWO = 2; + int NINE = 9; + + for (t = 0; t <= tsteps - ONE; plus(t)) + for (i = ONE; i<= n - TWO; plus(i)) + for (j = ONE; j <= n - TWO; plus(j)) + A[i][j] = ((A[i-ONE][j-ONE] + A[i-ONE][j] + A[i-ONE][j+ONE] + + A[i][j-ONE] + A[i][j] + A[i][j+ONE] + + A[i+ONE][j-ONE] + A[i+ONE][j] + A[i+ONE][j+ONE]) / NINE); + +} + + +int main() +{ + + int n = 40; + int tsteps = 5; + + + int A[40 + 0][40 + 0]; + + init_array (n, A); + + kernel_seidel_2d (tsteps, n, A); + + return print_array(n, A); + +} |