Vector addition

A very simple GPU kernel (written in PVL) that adds the content of two matrices and stores it in an "output" array (in GPU programming fashion). This program is currently disabled due to refactoring of the Chalice back-end.

General Information

Backend: Silicon
Language: PVL
Features: GPU Kernels, Arrays, Barriers
Path to Example File: arrays/vector-add.pvl
Should Verify: No
Date: 2017-06-15
Lines of Code: 23 (comments not included)
Lines of Specification: 9 (39.1% of total)

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases vector-add
//:: tools silicon
//:: verdict Pass

class Ref {
  context_everywhere a != null && b != null && c != null;
	context_everywhere tcount >= 0;
	context_everywhere a.length == tcount && b.length == tcount && c.length == tcount;
  context (\forall* int i; 0 <= i && i < tcount; Perm(a[i], write));
  context (\forall* int i; 0 <= i && i < tcount; Perm(b[i], read));
  context (\forall* int i; 0 <= i && i < tcount; Perm(c[i], read));
  ensures (\forall  int i; 0 <= i && i < tcount; b[i]==\old(b[i])); // already encapsulated by read permission (requires) on b
  ensures (\forall  int i; 0 <= i && i < tcount; c[i]==\old(c[i])); // already encapsulated by read permission (requires) on c
  ensures (\forall  int i; 0 <= i && i < tcount; a[i]==b[i]+c[i]);
  void main(int tcount, int[] a, int[] b, int[] c) {
    par (int tid=0..tcount) 
      context Perm(a[tid], write);
      context Perm(b[tid], read);
      context Perm(c[tid], read);
      ensures b[tid]==\old(b[tid]); // already encapsulated by read permission (requires) on b[tid]
      ensures c[tid]==\old(c[tid]); // already encapsulated by read permission (requires) on c[tid]
      ensures a[tid]==b[tid]+c[tid];
    {
      a[tid]=b[tid]+c[tid];
    }
  }
}

Language: