[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Question on mobile swaps



Hello Peter, Fred, Brian, and all,

As several of you know, we’re on the hunt for a static-only variant of occam-Pi, which I’ve tentatively named occam-Sigma (Greek s for static) - sorry, Fred! So I am studying Fred’s dissertation. Relating mobile data (section 4.2) and undefined usage checking (4.6), I notice that the undefined usage algorithm assumes a mobile communication is one-way, while the pointer exchange supports a swap.

Could there be a mobile primitive that would swap data both sides of which are defined, e.g. “?!” as

CHAN MOBILE INT c:
PAR
  MOBILE INT x:
  SEQ
    ... define x
    c ?! x
    ... continue work with x

being in classic occam

CHAN OF INT c1, c2:
PAR
  INT x:
  SEQ
    ... define x
    INT y:
    SEQ
      y := x
      PAR
        c1 ! y
        c2 ? x
    ... continue work with x

and the same for the second component of the PAR (channels swapped in the classic occam)?

This would correspond to the “swap caddy” that I drew on the board at CPA2016, while what is described in Fred’s dissertation would be a “slider slot”.

Larry Dickson