Changes between Initial Version and Version 1 of Pointers

Timestamp:

07/11/13 13:28:51 (13 years ago)

Author:

siegel

Comment:

--

Pointers

@@ +1 @@
+
+= Pointers and Scopes =
+
+== Scoping goals ==
+
+* It should be possible to statically determine the scope of any expression.  That means the expression only references objects in that scope.
+* It should be possible to specify/verify the "read scope" and "write scope" of any procedure.
+* The goals above are complicated by pointers, which can potentially to point to any scope if not controlled. So there must be ways to specify/verify some restrictions on the scopes of pointers.
+
+== Scopes ==
+
+First, scopes are declared like variable declarations:
+
+{{{
+{ ...
+  $scope s;
+  …
+}
+}}}
+
+gives a name to that scope.  In fact, every scope has a name automatically, this just gives the program a way to refer to it.
+
+Scopes cannot be used in expressions except as specified below.  In particular they cannot be assigned or passed as arguments to functions.
+
+== Pointer types ==
+
+* Given any object type T, there is a type "pointer-to-T".
+* Given in addition a scope s, there is a type "pointer-to-T-in-s".
+* The type "pointer-to-T-in-s" is a subtype of "pointer-to-T".
+* The type "pointer-to-T" is identical to the type "pointer-to-T-in-CIVL_Root_scope", where `CIVL_Root_scope` is the root system (most global) scope.
+* Furthermore, if s1 is contained in s2, "pointer-to-T-in-s1" is a subtype of "pointer-to-T-in-s2". 
+
+Syntax: a variable is declared to have type "pointer-to-int-in-s", for example, as follows:
+{{{
+  int *<s> t;
+}}}
+In general, the scope modifier is always placed after the `*` and surrounded by angle brackets.
+
+=== Address-of ===
+
+The address-of operator `&` returns a pointer of the appropriate subtype using the innermost scope in which its lhs argument is declared.  For example:
+{{{
+{ 
+  $scope s1;
+  int x;
+  double a[N];
+  int *<s1> p = &x;
+  double *<s1> q = &a[2];
+}
+}}}
+is legal (it will type-check) because `&x` has type pointer-to-int-in-s1, since `s1` is the scope in which `x` is declared. Etc.
+
+=== Pointer addition and subtractions ===
+
+if p has type pointer-to-T-in-s, then p+i (for an integer i) has type pointer-to-T-in-s. I.e., pointer addition cannot leave the scope.  (in fact, it cannot leave the object).
+
+Pointer subtraction: pointer subtraction is defined on two pointers of the same type, where "same" includes the scope.  That is checked statically.    As in C, it is only defined if the two pointers point to the same object.  In CIVL-C, a runtime error will be thrown if they do not point to the same object.
+
+=== Pointer casts ===
+
+If scope s1 is contained in scope s2, an expression of type pointer-to-T-in-s1 can always be cast to pointer-to-T-in-s2, because the first is a subtype of the second.  This is checked statically.  The cast in the other direction is also OK, but will only be checked at runtime.  If neither s1 is contained in s2 nor s2 is contained in s1, a cast from one pointer type to the other is illegal and will be reported as a syntax error statically.
+
+A type pointer-to-T1-in-s can be cast to a type pointer-to-T2-in-s according to the usual rules of C (or whatever variation is used in CIVL-C). In other words, usual casting rules apply as long as you don't change the scope.
+
+== Parameterized typedefs ==
+
+typedefs can be parameterized by scopes, e.g.
+
+{{{
+<s> typedef struct message_struct {
+  int size;
+  void *<s> data;
+} Message;
+}}}
+
+When the typedef is used, you specify the scope parameters:
+
+{{{
+Message<s1> buffer[N];
+}}}
+
+For each scope s, you get a different type `Message<s>`.  There is no (subtype or other) relationship between `Message<s1>` and `Message<s2>` and you cannot cast from one to the other.
+
+Multiple scopes can be used as parameters:
+{{{
+<s1,s2,s3> typedef struct ...
+}}}
+
+== Parameterized procedures ==
+
+Procedures can be parameterized by scopes, for example, as follows:
+{{{
+<s> int *<s> f(int *<s> p);
+}}}
+This means: for any scope s, f takes a pointer-to-int-in-s and returns a pointer-to-int-in-s.  Multiple scopes can be used as parameters: `<s,t>` ....
+
+The procedure f is invoked by specifying the scope as follows: ` ... f<s1>(...) …`.  Eventually we can infer the s in most cases.
+
+== Procedure contracts ==
+
+Procedure contracts can be optionally associated to procedure declarations or definitions in CIVL-C.  There will be typical requires/ensures and other clauses in these contracts. In addition, the following two kinds of clauses can be used:
+{{{
+    $reads s1;
+    $writes s2;
+}}}
+where s1 and s2 are scopes.  This means that any object read in any execution of f must lie in scope s1 and any object modified in any execution of f must lie is scope s2.  The scopes s1 and s2 can be parameters, as in:
+{{{
+<s1,s2> double *<s2> f(int *<s1> p)
+  $reads s1;
+  $writes s2;
+  {
+    ...
+  }
+ }}}
+
+== Heaps ==
+
+A heap is declared using the built-in type `$heap`:
+{{{
+{ ... $heap h1; …}
+
+}}}
+However, a heap cannot be assigned or used in expressions, with one exception: it can be the argument of address-of (&).  Hence this is fine:
+
+{{{
+{ ...
+  $scope s1;
+  $heap h1;
+  $heap *<s1> p = &h1;
+  ...
+}
+}}}
+
+=== Malloc and free ===
+
+These built-in functions have the following signatures:
+{{{
+<s> void *<s> $malloc($heap *<s> heap, int size)
+  $reads s;
+  $writes s;
+  
+<s> void $free($heap *<s> heap, void *<s> ptr)
+  $reads s;
+  $writes s;
+}}}
+
+This means:
+* for any scope s, `$malloc` takes a pointer-to-heap-in-s,  and an integer `size`, and returns a pointer-to-void-in-s.
+* `$free` takes a pointer-to-heap-in-s and a pointer-to-void-in-s, and returns nothing.
+* both procedures can only read and modify s.
+
+A runtime error will be generated if the second argument to `$free` is not really a pointer to the heap specified in the first argument.
+
+It may be that the first argument to `$free` is unnecessary. However, it helps keep track of what is modified by the procedure (namely, the heap that that argument points to).  At the very least, we need to keep track of the scope of the heap. Possibly, we could get by with:
+{{{
+<s> void $free(void *<s> ptr)
+  $reads s;
+  $writes s;
+}}}
+
+== Memcpy ==
+
+This is another built-in function with signature:
+{{{
+  <s,t> void memcpy(void *<s> p, void *<t> q, size_t size)
+    $reads t;
+    $writes s;
+}}}
+This copies data from `q` to `p` as usual.  
+
+== Examples==
+
+
+{{{
+{
+  $scope shared;
+  $heap shared_heap;
+  double *<shared> p = $malloc<shared>(&shared_heap, n*sizeof(double));
+  double *<shared> q = $malloc<shared>(&shared_heap, n*sizeof(double));
+
+  for (int i=0; i<n; i++) p[i] = (double)i;
+  $memcpy<shared,shared>(p, q, n*sizeof(double));
+  $free<shared>(&shared_heap, p);
+  $free<shared>(&shared_heap, q);
+}
+}}}
+
+Here is how an MPI program can be modeled with every process getting its own heap:
+
+{{{
+void MPI_proc(int pid) {
+  $scope proc_scope;
+  $heap proc_heap;
+  ...
+  ... $malloc<proc_scope>(&proc_heap, size) ...
+  ...
+}
+
+void main(int nprocs) {
+  $proc procs[nprocs];
+  
+  for (int i=0; i<nprocs; i++)
+    procs[i] = $spawn MPI_proc(i);
+  ...
+}
+}}}