Changes between Version 43 and Version 44 of IR2

Timestamp:

04/28/21 18:14:37 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -23 +23 @@
 1. **How to you translate between sequences and arrays?**
 1. Can you make types values? (reification)
-1. `$depends_on`
 1. read/write sets: function calls to start, stop monitoring reads/writes?  All part of mem library
-1. function calls for atomic enter/exit
 1. a type for $state ? 
 1. How do you model `malloc` when the element type is not known?  (Create a type `$byte`?)
@@ -54 +52 @@
 block: '{' typedef* decl* function-definition* statement* '}' ;
 statement: block | simpleStmt | chooseStmt ;
-simpleStmt: label? guard? primitiveStmt gotoStmt? ;
+simpleStmt: label? dependency? guard? primitiveStmt gotoStmt? ;
 chooseStmt: label? '$choose' '{' simpleStmt* '}' ;
 label: ID ':' ;
-guard: '$when' '(' expr ')' ;  
+guard: '$when' '(' expr ')' ;
+dependency: '$depends_on' '(' expression-list? ')'
+expression-list: expr (',' expr)* ;
 gotoStmt: 'goto' ID ;
 contract-clause :
@@ -82 +82 @@
 * A program must contain a function definition for a function named `main`.
 * `$input` and `$output` can be used only on global variable declarations (not on function definitions, not in block scope).
-* the `expr` in a guard must have type `$bool`
+* The `expr` in a guard must have type `$bool`.
+* The expressions in a dependency clause must have pointer type.   This declares that the following transition depends only on the objects pointed to.  
 
 {{{
@@ -145 +146 @@
   | lvalue '=' expr ';'  /* assignment */
   | expr '(' arg-list? ')' ';'  /* function call */
-  | (lvalue '=')? '$spawn' expr '(' arg-list? ')' ';'  /* process creation */
+  | (lvalue '=')? '$spawn' expr '(' expression-list? ')' ';'  /* process creation */
   | 'return' expr? ';'  /* return from function call */
   | (lvalue '=')? '$alloc' '(' expr ',' expr ',' type-name ')' ';'  /* heap allocation */
-arg-list: expr (',' expr)* ;  /* actual argument list */
 
 }}}