OEP

151

Title

Fix parallel-usage-checker and undefinedness-checker

Summary

Fix inconsistencies in parallel-usage-checker and undefinedness-checker.

Owner

Mario Schweigler

Status

Proposed

Date-Proposed

2005-09-12

Keywords

compiler bugs parallel-usage-checker undefinedness-checker

KRoC's parallel-usage-checker currently only takes into account parallel changes of a variable and parallel reads/writes from/to a variable, but _not_, in case of channel-type-end variables, when such a variable is assigned a new value in parallel with using the variable to communicate over one of its channels (in either direction). Consider the following code examples:

RECURSIVE CHAN TYPE FOO
  MOBILE RECORD
    CHAN INT i?:
    CHAN FOO! f?:
:

PROC sh.in (SHARED FOO! foo.cli)
  CHAN SHARED FOO! chan:
  PAR
    CLAIM foo.cli
      foo.cli[i] ! 5
    SEQ
      chan ? foo.cli
:

PROC sh.out (SHARED FOO! foo.cli)
  CHAN SHARED FOO! chan:
  PAR
    CLAIM foo.cli
      foo.cli[i] ! 5
    SEQ
      chan ! foo.cli
:

PROC sh.assign (SHARED FOO! foo.cli)
  PAR
    CLAIM foo.cli
      foo.cli[i] ! 5
    SEQ
      FOO? foo.svr:
      foo.cli, foo.svr := MOBILE FOO
:

PROC unsh.in (FOO! foo.cli)
  CHAN FOO! chan:
  PAR
    SEQ
      foo.cli[i] ! 5
    SEQ
      chan ? foo.cli
:

PROC unsh.out (FOO! foo.cli)
  CHAN FOO! chan:
  PAR
    SEQ
      foo.cli[i] ! 5
    SEQ
      chan ! foo.cli
:

PROC unsh.out.over.itself (FOO! foo.cli)
  PAR
    SEQ
      foo.cli[i] ! 5
    SEQ
      foo.cli[f] ! foo.cli
:

PROC unsh.assign (FOO! foo.cli)
  PAR
    SEQ
      foo.cli[i] ! 5
    SEQ
      FOO? foo.svr:
      foo.cli, foo.svr := MOBILE FOO
:

All of them currently compile without a complaint from the parallel-usage-checker. Actually (I talked to Peter about this earlier and he agreed as well), of all the above processes, only sh.out should compile, since the "chan ! foo.cli" line does not change the value of foo.cli because foo.cli is auto-cloned and then the clone communicated. All other processes should be disallowed by the parallel-usage-checker because in all cases, something is communicated over one of foo.cli's channels while the value of foo.cli is changed in parallel. [NB: This of course also applies to cases where something is inputted over a channel of foo.cli. To keep the code snippet short, I have not included extra examples for that.]

The _only_ case, where it should be allowed to send away an unshared end, and use a channel of that end at the same time, is when that end is sent over itself. While sending an unshared end over itself should continue to be allowed, cases like in unsh.out.over.itself (where another channel of foo.cli is used at the same time) should be prohibited, in accordance with what I wrote above.

Another thing I noticed (this concerns the undefinedness-checker rather than the parallel-usage-checker) is that sequentially sending an end over itself in the same communication like:

bar.cli[b] ! bar.cli; bar.cli

does not trigger any warnings from the compiler. I was able to compile a program that does the above, and in parallel to that reads the end into two different variables. When subsequently using the variables, using the second one triggers a runtime-error (as expected) since it is undefined. Nevertheless, since the above line is quite obviously wrong, it would be useful if the undefinedness-checker could trigger a warning when attempting to do things like that.

Another thing that is currently allowed in the compiler is this:

PROC proc (SHARED FOO! foo.cli, CHAN FOO! chan.foo)
  CLAIM foo.cli
    chan.foo ! CLONE foo.cli
:

This should be banned because the process reading from chan.foo would expect an unshared variable, but in fact get a shared one. This means that the variable would not be claimed before being used by the receiving process --- which would be disastrous.

OEP/151 (last edited 2007-09-27 01:25:08 by ats1)