$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/$atomic/$atom 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