PVL kernel (version 2)

A kernel program (written in PVL) with forward dependencies. Barrier synchronisation is used to redistribute permissions for this. This program currently does not verify due to refactoring of the Chalice back-end (we will use Silicon from now).

General Information

Backend: Silicon
Language: PVL
Features: GPU Kernels, Arrays, Barriers
Path to Example File: arrays/kernel-example-v2.pvl
Should Verify: No
Date: 2017-06-15
Lines of Code: 34 (comments not included)
Lines of Specification: 15 (44.1% of total)

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases kernel-example-v2
//:: tools silicon
//:: verdict Pass

class Ref {
  context_everywhere a != null && b != null && c != null;
	context_everywhere a.length == tcount && b.length == tcount && c.length == tcount;
  context_everywhere tcount >= 0;
  context  (\forall* int i; 0 <= i && i < tcount; Perm(c[i], 1\4) ** c[i] > 0); // Perm(c[i], read) also possible (1)
  requires (\forall* int i; 0 <= i && i < tcount; Perm(a[i], write));
  requires (\forall* int i; 0 <= i && i < tcount; Perm(b[i], write));
  ensures  (\forall* int i; 0 <= i && i < tcount; Perm(a[i], 1\4) ** a[i] > 0); // Perm(a[i], read) also possible (1)
  ensures  (\forall* int i; 0 <= i && i < tcount; Perm(b[i], 1\4) ** b[i] > 0); // Perm(b[i], read) also possible (1)
  void main(int tcount, int[] a, int[] b, int[] c) {
    par fwd (int tid=0..tcount)
      context  Perm(c[tid], 1\4) ** c[tid] > 0; // Perm(c[tid], read) also possible (2)
      requires Perm(a[tid], write);
      requires Perm(b[tid], write);
      ensures  Perm(a[tid], 1\4) ** a[tid] > 0; // Perm(a[tid], read) also possible (2)
      ensures  Perm(b[tid], 1\4) ** b[tid] > 0; // Perm(b[tid], read) also possible (2)
    {
      b[tid]=c[tid]; 
      barrier(fwd) {
        // losing all permissions:
				context 0 <= tid && tid < tcount;
        context  Perm(a[tid], write);
        context  Perm(c[tid], 1\4); // Perm(c[tid], read) also possible (3)
        requires Perm(b[tid], write);
        ensures  Perm(b[tid], 1\4); // Perm(b[tid], read) also possible (3)
        ensures  tid>0 ==> Perm(b[tid-1], 1\4); // Perm(b[tid-1], read) also possible (4)
        context  b[tid] > 0;
        context  c[tid] > 0;
        ensures  tid>0 ==> b[tid-1] > 0;
      }
      if(tid>0) {
        a[tid]=b[tid-1]+b[tid];
      } else {
        a[tid]=b[tid];
      }
    }
  }
}

Language: