Summation kernel (version 1)

Verification of a GPU kernel program, encoded in PVL, that sums the elements of an input array.

General Information

Backend: Silicon
Language: PVL
Features: GPU Kernels, Iteration contracts, Arrays
Path to Example File: carp/summation-kernel-0.pvl
Should Verify: Yes
Date: 2017-06-15
Lines of Code: 28 (comments not included)
Lines of Specification: 10 (35.7% of total)
Computation Time: 38.4 seconds

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases SummationKernel
//:: suite puptol
//:: tools silicon
//:: verdict Pass

class Ref {
  int res;

context_everywhere ar != null ** N > 0 ** M > 0 ** \array(ar,M*N);
  context Perm(res,write) ** (\forall* int i;0 <= i && i < M*N ; Perm(ar[i],1\2));
  requires res==0;
  void do_sum(int M,int N, int[M*N] ar){
		
    invariant outer( Perm(res,write) ){
      par kern(int g = 0 .. M)
        context (\forall* int k ; 0 <= k && k < N ; Perm(ar[g*N+k],1\4));
      {
        int[1] temp=new int[1]; temp[0]=0;
        invariant inner( \array(temp,1) ** Perm(temp[0],write) ){
          par workgroup(int t = 0 .. N)
						context_everywhere 0 <= g && g < M;
            requires Perm(ar[g*N+t],1\4);
            ensures t==0 ==> (\forall* int k; 0 <= k && k < N ; Perm(ar[g*N+k],1\4));
          {
            atomic(inner){ temp[0]=temp[0]+ar[g*N+t]; }
            barrier(workgroup){
							context 0 <= g && g < M;
							context 0 <= t && t < N; // TODO REMOVE??
              requires Perm(ar[g*N+t],1\4);
              ensures  t==0 ==> (\forall* int k; 0 <= k && k < N ; Perm(ar[g*N+k],1\4));
            }
            if(t==0){ int tmp;
              atomic(inner){ tmp=temp[0]; }
              atomic(outer){ res=res+tmp; }
  } } } } } }
}

Language: