Notes on model package for the Chapel Verification Tool (CVT).

A model comprises:
  a set of Functions, and
  a designated outermost function "System"

A Function comprises the following data:
  a name
  sequence of input parameters/types
  output type
  a set of Scopes, including a designated "outermost local" scope.
  a set of Locations, including a designated "start location".
  a set of Statements that acts as edges from one location to another
  
A Scope consists of:
  a set of variables, each with a given Type.
  a parent scope and children scope (so they form a tree).

A Location consists of:
  the scope in which this location exists
  set of incoming statements
  set of outgoing statements
  
A Statement consists of:
  source location
  target location
  a boolean guard expression
  other stuff, depending on the type of Statement

A Variable comprises:
  a type
  isSync (boolean)
  isConst (boolean)
  extent (expression) for array variables (optional)

Types:
  Primitive: int, bool, real, string
  Array<T>
  Process

Expressions:
  Choose(int) : int.  Choose integer between 0 and arg-1, inclusive.
  literals
  +-*/%<,<=,==,!=,&&,||,!
  a[i]
  Me : Process (process in which the expression is evaluated)

Statements:
  AssignStatement: LHS, RHS expressions
  SendStatement: arguments include sending process and destination process, tag
  RecvStatement: arguments include receiving process and source process, tag.
    Must allow ANY_TAG and ANY_SOURCE.  Must provide way to get the tag and source.
    Copy TASS.
  ForkStatement: takes reference to Function, args, and returns a Process.
  JoinStatement: takes reference to Process
  ReturnStatement: possible expression
  WriteStatement: sequence of expressions
  CallStatement: optional LHS, reference to Function, argument expressions
  NoopStatement: no args


Notes

Translation of iterators, yield:

In the original Chapel, a general iterator is defined like a function

    iter f(...) : T { IS ... yield e; ... }
    
where the body IS of f contains "yield" statements.  In the model, f will become
a regular function.   The function will take an extra argument p of Process type,
which will be the process calling the iterator.  The yield statements will in IS
will be replaced by sends back to p of whatever the argument to yield is.
The body of the model function will look like:

    void f_model(Process caller, ...) {
      ...
      send(me,caller,e,NEXT_TAG);
      ...
      send(me,caller,NULL,TERM_TAG);
    }

Translation of the use of the iterator depends on the particular kind of use.

Translation of cobegin:

    cobegin {
      S1; ...; Sn
    }

becomes:

    {
      Process tmp_procs[n];
      
      void tmp_101() { S1 }
      ...
      void tmp_10n() { Sn }
      tmp_procs[0] = fork tmp_101();
      ...
      tmp_procs[n-1] = fork tmp_10n();
      join tmp_procs[0];
      ...
      join tmp_procs[n-1];
    }

Translation of for..in..

    for x in f(...) S

Is translated as
    {
      T x;
      Process p;
      int tag;
      
      p=start f_model(me,...);
      while (true) {
        recv(me,p,x,any(tag));
        if (tag==TERM_TAG) break;
        S;
      }
    }


Translation of forall:

    forall x in f(...) S2(x)
    
is translated as:

    {
      int numWorkers = 1 + choose(MAX_WORKERS);
      Process workers[numWorkers];
      
      void tmp_101(Process manager) {
        T x;
        int tag;
        
        while (true) {
          recv(me,manager,x,any(tag));
          if (tag==ITER_TERM) break;
          S2;
        }
      }
      
      for (i=0..numWorkers-1) workers[i]=fork tmp101(me);
      
      {
        T x;
        Process iterator;
        int tag;
      
        iterator=start f_model(me,...);
        while (true) {
          recv(me,iterator,x,any(tag));
          if (tag==TERM_TAG) break;
          dest = choose(numWorkers);
          send(me,workers[dest],FORALL_TAG,x);
      }
      for (i=0..numWorkers-1) send(me,workers[i],TERM_TAG, NULL);
      for (i=0..numWorkers-1) join workers[i];
    }
    
    
Translation of coforall:

    coforall 0..x in f(...) S2(x)
    
is translated as:

    {
      int numWorkers = x;
      Process workers[numWorkers];
      
      void tmp_101(Process manager) {
        T x;
        int tag;
        
        while (true) {
          recv(me,manager,x,any(tag));
          if (tag==ITER_TERM) break;
          S2;
        }
      }
      
      for (i=0..numWorkers-1) workers[i]=fork tmp101(me);
      
      {
        T x;
        Process iterator;
        int tag;
        int dest;
        
        dest=-1;
        iterator=start f_model(me,...);
        while (true) {
          recv(me,iterator,x,any(tag));
          if (tag==TERM_TAG) break;
          dest = dest+1;
          send(me,workers[dest],FORALL_TAG,x);
      }
      for (i=0..numWorkers-1) send(me,workers[i],TERM_TAG, NULL);
      for (i=0..numWorkers-1) join workers[i];
    }



State:

  define DynamicScope
    (lexical) Scope
    parent: DynamicScope
    children: set of DynamicScope
    symbolic expression value for every dynamic variable
  
  define DynamicVariable
    StaticVariable
    DynamicScope
     
  define Process
    id : int
  
  define Message
    tag: concrete int
    data: symbolic expression
    
  State:
    set of processes
    set of dynamic scopes
    each process has:
      location
      dynamic scope (which points up to other dynamic scopes)
    buffers:
      for each ordered pair of processes p,q a sequence of messages
  
  value for every variable (symbolic expression)


A variable of type "process" holds an integer value, which is the PID.
String holds a Java string.
integer: symbolic expression of integer type
reals: symbolic expression of real type
array

------

Transitions (Kripke structure):


add state package
