Forward dependencies (kernel 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/forward-dep.pvl
Should Verify: No
Date: 2017-06-15
Lines of Code: 39 (comments not included)
Lines of Specification: 18 (46.2% of total)

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases forward-dep
//:: 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(b[i], read));
  context  (\forall* int i; 0 <= i && i < tcount; Perm(c[i], write));
  requires (\forall* int i; 0 <= i && i < tcount; Perm(a[i], write));
  ensures  (\forall* int i; 0 <= i && i < tcount; Perm(a[i], 1\2)); // Perm(a[i], read) also possible (1)
  context  (\forall  int i; 0 <= i && i < tcount; b[i]==i);
  ensures  (\forall  int i; 0 <= i && i < tcount; a[i]==i+1);
  ensures  (\forall  int i; 1 <= i && i < tcount; c[i]==i+2);
  void main(int tcount, int[] a, int[] b, int[] c) {
    par fwd (int tid=0..tcount)
      context  Perm(b[tid], read);
      context  Perm(c[tid], write);
      requires Perm(a[tid], write);
      ensures  Perm(a[tid], 1\2); // Perm(a[tid], read) also possible (2)
      context  b[tid]==tid;
      ensures  a[tid]==tid+1;
      ensures  tid>0 ==> c[tid]==tid+2; 
    {
      a[tid]=b[tid]+1; 
      barrier(fwd) {
        // losing all permissions:
				context 0 <= tid && tid < tcount;
        context  Perm(b[tid], read);
        context  Perm(c[tid], write);
        requires Perm(a[tid], write);
        ensures  Perm(a[tid], 1\2); // Perm(a[tid], read) also possible (3)
        ensures  tid>0 ==> Perm(a[tid-1], 1\2); // Perm(a[tid-1], read) also possible (4)
        requires a[tid]==tid+1;
        ensures  a[tid]==\old(a[tid]); // this one is necessary, due to write permission (requires) on a[tid]
        ensures  b[tid]==\old(b[tid]); // already encapsulated by read permission (requires) on b[tid]
        ensures  tid>0 ==> a[tid-1]==tid;        
      }
      if (tid>0) {
        c[tid]=a[tid-1]+2;
      }
    }
  }
}

Language: