nickng / sessc Goto Github PK

while (1) {
  send_int(42, P1, NULL); // This is considered
  recv_int(&v, P1);  // This is considered
  while (1) {
    send_int(3, P1, NULL); // This is considered
    recv_int(&v, P1); // This is considered
  }
  send_int(42, P1, NULL); // This is NOT considered
  recv_int(&v, P1);  // This is NOT considered
}

Because of how boundary are defined in asynchronous optimisation to limit its complexity (ie. only consider node 0 to first non send/recv node), it is not possible to have multiple segments of optimised code separated by non send/recv node. This can be improved if the all segments with well defined starting node and ending node is checked until ending node gets to the end of the recur-block body.

I have append the typechecker to recoginize MPI code. However, nested loops and choices that do not have any communication primitives, must not appear in the final tree.
An example of the issue is the following:

0 | Node { type: root }
1 | Node { type: MPI_Reduce, root: 9, msgsig: { tag: -, payload: MPI_CHAR }}
1 | Node { type: choice, var depend.: - } 1 children
2 | Node { type: root }
3 | Node { type: choice, var depend.: - } 0 children

Both choices are empty (no primitives) but after refactoring the tree they are still there.

Node comparison/type checking currently compares child blocks in order, ie.

node->children[i] != other->children[i+1]

despite the possibility with some of the nodes, eg. Choice, Parallel

Solution is either
(1) reorder the child-blocks in a canonical way; or
(2) try to match each child-blocks instead of the one with the same index.

Ensure that switch-case statements cannot contain session operations in any of the sub statements.

Current behaviour is ignoring switch-case statements altogether but it is not safe;
One might include a send_int in one of the cases but ignored by the session type extractor, eg.

switch (var) {
  case 0: break;
  case 1: send_int(1, A, NULL); break;
  default: break;
}

Which should be typed as

choice at A {
} or {
  (int) from A;
} or {
}