VSL: Verified Software Laboratory - Main

Numerical Software Verification.

Abstracts due Mar. 25, 2010 Submission deadline Apr 1, 2010 Notification Apr. 28

http://www.lix.polytechnique.fr/Labo/Sylvie.Putot/NSV3/

1. Tool paper 6 pages LNCS mention loop technique performance data and stress small configuration hypothesis language features that can be handled

  - and how we do it.

advances over previous work (TOSEM): more complicated queries

2. Benchmark paper 6 pages LNCS

program pairs (spec, impl)

standard form: read from files, etc.

diffusion1d (seq and parallel) diffusion2d (seq and parallel) laplace2d (seq and parallel) matmat (seq and parallel manager-worker, adapted from Gropp et al.) matrixMultiplication: normal and tiled seq nbody (seq and parallel) adder (seq and parallel) fib (two versions of phi estimation) factorial (iterative and recursion) mean (naive or running average) gaussian elimination (seq and parallel)

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

int B;
int n; /* {n>=0 && n<=B}; */
double *a; /* a[n] */
int NPROCS;
int PID;

output double sum;
double localSum = 0.0;

double computeGlobalSum() {
  double result = localSum;
  double buffer;
  int i;

  for (i=1; i<NPROCS; i++) {
    MPI_Recv(&buffer, 1, MPI_DOUBLE, i, 0, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
    result += buffer;
  }
  return result;
}

int main(int argc, char* argv[]) {
  int i;
  int first, afterLast;

  MPI_Init(&argc, &argv);
  MPI_Comm_size(MPI_COMM_WORLD, &NPROCS);
  MPI_Comm_rank(MPI_COMM_WORLD, &PID);
  B = atoi(argv[1]);
  n = atoi(argv[2]);
#pragma TASS_assume(n<=B && n>=0);
#pragma TASS_assume(n==argc-3);
  a = (double*)malloc(n*sizeof(double));
  for (i=0; i<n; i++) a[i]=atof(argv[i+3]);
  first = n*PID/NPROCS;
  afterLast = n*(PID+1)/NPROCS;
  for (i=first; i<afterLast; i++) localSum += a[i];
  if (PID == 0) {
    sum = computeGlobalSum();
    printf("%f\n", sum);
    fflush(stdout);
  }
  else {
    MPI_Send(&localSum, 1, MPI_DOUBLE, 0, 0, MPI_COMM_WORLD);
  }
  MPI_Finalize();
  return 0;
}

/*
  ignore #includes
  input is array of ints argv[argc]
  atoi, atof symbolic functions
  MPI_Comm_size(*,&x) ==> x=NPROCS
  MPI_Comm_rank(*,&y) ==> y=PID
  MPI_Send(...) ==> send statement
  MPI_Recv(...) ==> recv statement
  MPI_Init(), MPI_Finalize() ==>
  output: in model:
    int out_count;
    real out[out_count];
    printf("...%d...%lf...", x1,x2) ==>
      out[out_count]=x1; out_count++; 
      out[out_count]=cast(x2); out_count++; 
  assumptions in decls:

  assume ==> #pragma TASS_assume
*/

NSV 3