Changes between Version 122 and Version 123 of IR2

Timestamp:

06/09/21 01:54:12 (5 years ago)

Author:

ziqing

Comment:

--

IR2

@@ -492 +492 @@
 
 * In`$parspawn` `*f` must have the function type that consumes n `$int`s, where n is the dimension of the domain.   The function is spawned once for each element of the domain.  References to the new processes are stored in the process array.   The call to `$parspawn` returns immediately.
+
+=== `state.cvh` ===
+* `$state $state_get()`:  returns a program state containing ONLY the current process state of the calling process.  Equivalent to taking a snapshot of the calling process at the current state.
+
+* `$bool $state_eval_local($state s, void *buf, int size, void *out)`: reads the data of `size` from `buf` at state `s` and writes the data to `out` at the current state.  Returns true iff the data being read is defined.
+
+* `$state $state_merge($state s, $state mono, int * place)`: merges the snapshot `mono` to the state `s` and returns the merged state.  The process in `mono` is assigned a new place in the merged state. The new place is returned to the output argument `place`.  Note that the `mono` state is not necessarily a state containing a single process.  This function treats it as if it only contains a single process, i.e., this function only reads the process state of place 0 in `mono`.
+
+* '''Remark 1''': There is no way to let a process `p` to read data of a different process `q` in a $state through a pointer.   So we still need a language construct like `$state_eval(state, place, expr)`.
+
+* '''Remark 2''': To make the `$state_eval_local` function above more useful, we need functions to iterate elements in `$mem` objects.  An element in a `$mem` object can be represented by a pair: a pointer and a size.  The loop invariant transformer currently needs to write values from a `$state` to memory locations in a `$mem` object.