Changes between Version 132 and Version 133 of IR

Timestamp:

12/10/15 16:49:05 (10 years ago)

Author:

zmanchun

Comment:

--

IR

@@ -387 +387 @@
   mpi_requires expr ;
   mpi_ensures expr ;
-  assigns expr ;
-  reads expr ;
-  depends actions ;
+  behavior name:
+    assigns expr ;
+    reads expr ;
+    depends actions ;
 {
   // all of the following are missing for a system function...
@@ -444 +445 @@
 
 * memory set action expressions:
- * `reads e`: `e` has type `Mem`. The function reads the memory units specified by `e`.
- * `assigns e`: `e` has type `Mem`. The function writes the memory units specified by `e`.
- * `calls f, <e1, ...>`: `f` has type `Function`. The function calls `f` with parameters `e1, ...`.
- * `nothing`: no action
- * `everything`: all actions
- * `ma_union(ma0, ma1)`: the union of the two memory set actions `ma0` and `ma1`.
- * `ma_comp(ma0, ma1)`: action complement (everything not in `ma1`)
- * `ma_isect(ma0, ma1)`: action intersection
-
-* depends clause: `depends [condition] action0, action1, action2, ... `
- * Example: `depends ma_union(ma_comp(reads n, calls inc, <x>)), calls(dec, y))`
+ * `read(e)`: `e` has type `Mem`. The function reads the memory units specified by `e`.
+ * `write(e)`: `e` has type `Mem`. The function writes the memory units specified by `e`.
+ * `call(f, <e1, ...>)`: `f` has type `Function`. The function calls `f` with parameters `e1, ...`.
+ * `noaction`: no action
+ * `anyaction`: all actions
+ * `act_union(ma0, ma1)`: the union of the two memory set actions `ma0` and `ma1`.
+ * `act_comp(ma0, ma1)`: action complement (everything not in `ma1`)
+ * `act_isect(ma0, ma1)`: action intersection
+
+* depends clause: `depends action0, action1, action2, ... `
+ * Example: `depends act_union(act_comp(read(n), call(inc, <x>))), call(dec, <y>))`
  * absence of depends clause: there is no information about the dependency of the function, which means that the analysis needs to figure it out by itself.
 * some facts about assigns-or-reads clause
- * `reads nothing` implies `assigns nothing`
- * `reads nothing` is equivalent to: `ma_union(reads nothing, assigns nothing)`
- * `assigns X` where `X != nothing`, implies `reads X`
- * `assigns X` is equivalent to: `ma_union(assigns X, reads X)`
- * absence:
-  * absence of `reads` clause: there is no assumption about the read access of the function, i.e., the function could read anything
+ * absence of `reads`/`assigns` clause: there is no assumption about the read/assign access of the function, i.e., the function could read/assign anything
   * absence of `assigns` clause: similar to the absence of `reads` clause
- * `reads/assigns nothing` doesn’t necessarily means that the function never reads or assigns any variable. The function could still reads/assigns its “local” variables, including function parameters and any variable declared inside the function body.
+ * `reads/assigns nothing` doesn’t necessarily means that the function never reads or assigns any variable. The function could still reads/assigns its “local” variables, including function parameters and any variable declared inside the function body. **check it**
 
 * For an independent function which has `depends nothing`, usually we also need to specify `reads nothing`, for the purpose of reachability analysis.
@@ -479 +475 @@
 {{{
 fun[atomic] sendRecv(Int cmd, Pointer buf): Integer
-  depends [eq(cmd, SEND)] writes(buf)
-  depends [eq(cmd, RECV)] access(deref(buf))
-  assigns [eq(cmd, SEND)] nothing
-  assigns [eq(cmd, RECV)] deref(buf)
-  reads deref(buf)
+  reads deref(buf);
+  behavior send:
+    depends writes(buf);
+    assigns nothing;
+  behavior receive:
+    depends access(deref(buf));
+    assigns deref(buf);
 {
   begin choose
-  when (eq(cmd, SEND))
+  when (eq(cmd, 0))
      do CALL send, <buf, ...>; goto L1;
-  when (eq(cmd, RECV))
+  when (eq(cmd, 1))
     do CALL recv, <buf, ...>; goto L1;
-  when (and(neq(cmd, SEND), neq(cmd, RECV)))
+  when (and(neq(cmd, 0), neq(cmd, 1)))
     do NOOP; goto L1;
   end choose