Fork/join updates

Two threads that concurrently attempt to increase the values `p.x` and `p.y`, respectively, of an object `p` of type Point. The shared state can be splitted into two: one thread having writing permission to `p.x` and the other thread to `p.y`.

General Information

Backend: Chalice
Language: PVL
Features: Fork/join concurrency
Path to Example File: forkjoin/update-point.pvl
Should Verify: Yes
Date: 2017-06-16
Lines of Code: 47 (comments not included)
Lines of Specification: 5 (10.6% of total)
Computation Time: 7.6 seconds

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases UpdatePoint
//:: tools chalice
//:: verdict Pass

/* 
  Note that the silicon and chalice tool chains use
  different ways of specifying fork/join patterns.
  Therefore this specification cannot be verified
  with Silicon.
*/

class Point {
  int x;
  int y;
}

class X {
  Point p;
  
  requires Perm(this.p,33) ** Perm(this.p.x,100);
  ensures Perm(this.p,33) ** PointsTo(this.p.x,100,\old(this.p.x)+1);
  void run() {
    Point q = this.p;
    q.x = q.x+1 ;
  }
}

class Y {
  Point p;

requires Perm(this.p,33) ** Perm(this.p.y,100);
  ensures Perm(this.p,33) ** PointsTo(this.p.y,100,\old(this.p.y)+1);
  void run() {
    Point q = this.p;
    q.y = q.y+1 ;
  }
}

class Main {

void main(){
    Point p = new Point();
    p.x = 2;
    p.y = 6;

X obj1 = new X();
    obj1.p = p;
    fork obj1;
    
    Y obj2 = new Y();
    obj2.p = p;
    fork obj2;

join obj1;
    join obj2;
    assert PointsTo(p.x,100,3) ** PointsTo(p.y,100,7);
  }
}

Language: