Changes between Initial Version and Version 1 of Choose

Timestamp:

09/16/15 11:43:07 (11 years ago)

Author:

zmanchun

Comment:

--

Choose

@@ +1 @@
+= `$choose` statement =
+
+== current syntax ==
+{{{
+$choose{
+  S1
+  S2
+  ...
+  default: Sn
+}
+}}}
+`Sk` (`k=1..n`) could be any statement: a compound statement, any kind of atomic statement, a guarded statement, any other statement (if-else, while, for, ...).
+
+
+=== example ===
+
+{{{
+$choose{
+  $when(x<0){$when(y>0){int k; k=x+y;}}
+  $when(1){ 
+    $comm_enqueue(comm, out);
+    in = $comm_dequeue(comm, source, recvtag);
+  }
+  $when(1){
+    in = $comm_dequeue(comm, source, recvtag);
+    $comm_enqueue(comm, out);
+  }
+}
+}}}
+
+=== the result of the current translation would be ===
+
+`TRANS1`:
+
+{{{
+LOC0:
+[x<0 && y>0] k=x+y -> LOC3
+[true] $comm_enqueue(...) -> LOC1
+[comm_probe()] $comm_dequeue(...) -> LOC2
+
+LOC1:
+[$comm_probe()] $comm_dequeue(...) -> LOC3
+
+LOC2:
+[true] $comm_enqueue(...) -> LOC3
+
+LOC3:
+...  
+}}}
+
+=== problem of current translation (`TRANS1`) ===
+1. when there are new scope introduced by the any clause, the clauses can't share the same source location in the model, because a location is associated with a unique scope; for example, at `LOC0` in `TRANS1`, the first statement accesses `k` but `k` isn't visible in the scope associated to `LOC0` (`LOC0` is corresponding to the scope at `$choose`)
+2. a quick solution for 1 is introduce a noop at the beginning of each clause, and move the guard of the first statement of the clause to the noop; this would translate the example into `TRANS2`:
+
+`TRANS2`:
+{{{
+LOC0:
+[x<0 && y>0] noop -> LOC1
+[true] noop -> LOC2
+[comm_probe()] noop  -> LOC3
+
+LOC1:
+[true] k=x+y; -> LOC
+
+LOC2:
+[true] $comm_enqueue(...) -> LOC4
+
+LOC3:
+[true] $comm_dequeue(...) -> LOC5
+
+LOC4:
+[$comm_probe()] $comm_dequeue(...) -> LOC6
+
+LOC5:
+[true] $comm_enqueue(...) -> LOC6
+
+LOC6:
+...  
+}}}
+
+=== problem of `TRANS2` ===
+There are still a few problems in the above translation (`TRANS2`):
+
+1. it breaks the checking of potential deadlock. CIVL will report a false alarm of a potential deadlock.
+2. the extra noop changes the semantics slightly: for example, if at LOC0, the first noop is chosen to executed, i.e., `x<0 && y>0` is evaluated to be true; and then another process updates the value of `x` or `y` and then `x<0 && y>0` is no longer true, but since the process is now at LOC1, so the statement `k=x+y` will still be executed. This conflicts with the semantics of the guarded statement `$when(x<0){$when(y>0){int k; k=x+y;}}`.
+
+== new solutions ==
+
+=== new syntax ===
+
+- requires curly braces in each clause of `$choose` , not allowing clauses to introduce new scopes
+{{{
+choose_stmt: ‘$choose’ ‘{‘  choose_clause+ ‘}’;
+
+choose_clause: 
+      ‘{‘ block_item* ‘}’      
+    | when_stmt   
+    | labeled_stmt 
+}}}
+
+- uses labels
+{{{
+$choose {
+
+  LABEL0:  stmt*;
+
+  LABEL1:  stmt*;
+
+
+}
+}}}
+
+=== translation notes ===
+
+- inside a compound statement that is the body of a `$when` or a clause in a `$choose`, if the first item is a declaration a no-op is inserted before it in translation.  Then you are guaranteed that the guard will never involve a new variable. 
+
+example:
+
+{{{
+$when (e) {int x; blah}  translated to:   
+    LOC0 -e:noop-> LOC1(int x)
+$when (e) {$when (f) S} translated to: (let So the first atomic statement in S)
+    LOC0 -e&&f:S0-> LOC1  if S0 is not a variable declaration
+or otherwise
+    LOC0 -e&&f:noop-> LOC1(variable declared by S0) 
+$when (e) {$comm_dequeue; …} translated to: 
+    LOC0 -e&&$comm_probe(…):$comm_dequeue()-> LOC1
+}}}
+