[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Mobile variables
Mobile Variables (2)
~~~~~~~~~~~~~~~~~~~~
This is a slightly revised version. In my first experiment, CLAIM had two
functions: to "grab" exclusive rights to the variable(s); and to define
a scope in which EREW usage rules apply. It was a variant on a PAR
constructor. I then needed an extra keyword OWN to test ownership. By
making CLAIM roughly equivalent to a function with side effects (I feel
uncomfortable about that), no extra keyword is needed. The second
function of the original CLAIM -- to delimit usage rule regions -- is
now done by a "mobile abbreviation".
1) A mobile variable is declared in the usual way but with a prefix
MOBILE. This decoration informs the compiler that the
variable will be MOBILE at some point and allows separate compilation
of processes.
Example: INITIAL MOBILE [2]INT IS [1,2] :
2) A VAR CHAN declaration has the form
CHAN OF VAR x,.. c,.. :
where x,... is a list of variables (necessarily in scope).
3) The ordinary CREW usage rules apply to a (potentially) mobile variable
except in the scope of a MOBILE abbreviation. Within the entirety of
such a scope, the variables must be held exclusively by a single branch
of any and all (PRI) PAR constructors, or initially, none.
Conceptually, the variable is held in a pointer: initially that pointer
is is outer scope, so is hidden by the abbreviation (none). But a
CLAIM can retrieve it.
4) A MOBILE abbreviation is of the form
new IS MOBILE old:
old is in outer scope, and may already be the subject to abbreviations
including MOBILE abbreviation. The usual antialiasing rules apply and
so there can be no reference to the original "old" in the scope. This
includes VAR CHAN communications like "c ! VAR new". This is valid
even when c was declared in the outer scope as
CHAN OF VAR old c: .
Conceptually, the variable must involve the same address regardless
of it current name.
Any further abbreviation of a MOBILE variable must also be mobile.
RETYPES may also be qualified as MOBILE and are equivalent to IS
as far as the mobile semantics are concerned. MOBILE retyping and
MOBILE abbreviation may be freely mixed.
5) CLAIM [x,...] or CLAIM x should only be applied to variables x,...
which are in the scope of a MOBILE abbreviation. It behaves as
STOP if passed any other variable. For a mobile variable, it returns
TRUE if the variable is captured or already owned, and FALSE otherwise.
If applied to a table of mobile variables, it returns TRUE if all are
captured. A CLAIM may appear as a statement in which case the boolean
returned is discarded. Otherwise it may appear as a term in any
expression where a boolean may be used.
A CLAIM inspects one level of enclosing scope. That is, it examines the
the process that executed the PAR of which it is a component, if any.
If that process owns the variable, or a variable which has been
subdivided by abbreviation, then it claims ownership and returns TRUE.
Otherwise it returns FALSE.
[ Note that a FALSE return can arise because the variable has been
claimed by another branch, or because it is still owned at some scope
further out. This gives the quickest response, is simple and gives
explicit control to the programmer. ]
6) VAR communications take the forms
c ! VAR x and c ? VAR x or c ? CASE VAR x or c ? CASE
...
They may only appear within the scope of a MOBILE abbreviation for
x. The usual anti-aliasing rules ensure that it is the innermost
such abbreviation.
The variable x must "correspond" to the variable in the declaration of
the MOBILE channel c, where "correspond" means "refers to the same data
object".
c ! VAR x is an error and behaves like STOP if the process does not
"own" the variable x.
7) The variant protocol syntax is used for VAR channels involving more
than one variable.
If these rules are obeyed/enforced by the compiler, it is safe for the
programmer to think of the variable being moved about within the scope
of a MOBILE abbreviation.
All comments welcome.
Is the new status of CLAIM sensible? The compiler has to examine context
to determine whether CLAIM x is a statement ot a boolean.
None of this is cast in stone, of course. :-)
--{{{ semantics
Informally, the simplest account is in terms of pointers. In passing, we note
that there is little point in using mobile variables for small data structures
which might just as well be copied.
When a compiler encounters a MOBILE abbreviation or a MOBILE declaration, it
will construct a pointer to the data. For code within the scope of a MOBILE
abbreviation, each process that refers to the relevant variable will have
a pointer in its workspace. Each such will initially be set to Not_a_pointer.
A successful CLAIM will replace the Not_a_pointer by the address of
the relevant data in its workspace. That pointer
can only be "moved" by
1) a further embedded CLAIM;
2) communication;
3) termination: the pointer returns to the enclosing process.
Of course, a transmitting process must replace its pointer with
Not_a_pointer, and a receiver places the pointer into its workspace.
Thus this style of code generation ensures the correct usage rule.
A compiler might well implement mobile variables in this way, but this
informal operational semantics is only intended clarify the ideas.
--}}}
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--{{{ Examples
--{{{ 1) Multiple abbreviation
MOBILE [4 *N]BYTE array:
first IS MOBILE [array FROM 0 FOR 2*N]:
second IS MOBILE [array FROM 2*N]:
PAR
SEQ
CLAIM first -- this might not succeed
quarter1 IS [first FROM 0 FOR N] :
quarter2 IS [second FROM N] :
CLAIM [quarter1,quarter2] -- the other process may own first
... -- so this might fail
SEQ
CLAIM first
... -- this process has no knowledge of quarter1 and quarter2
--}}}
--{{{ 2) Invalid CLAIM
-- This program compiles to STOP!
-- x appears in a CLAIM, but not in the scope of a MOBILE abbreviation
MOBILE INT x: -- This alone does not specify usage rule. It is CREW
--- until modified by MOBILE abbreviation
IF
TRUE
SKIP
FALSE
CLAIM x -- static usage check implies STOP before
-- any optimization that might eliminate this code
-- a CLAIM is invalid where CREW is in force.
--}}}
--{{{ 3) VAR CHAN declared inside MOBILE abbreviation
MOBILE INT x : -- maybe MOBILE can be omitted here?
SEQ
X IS MOBILE x:
CHAN OF VAR X c:
PAR
SEQ
CLAIM X
c ! VAR X
c ? VAR X
:
--}}}
--{{{ 4) VAR CHAN declared outside a MOBILE abbreviation
MOBILE INT x :
CHAN OF VAR x c : -- Declaration outside MOBILE abbreviation
SEQ
... some CREW stuff
x IS MOBILE x : -- Notice this is a new x descoping old x
PAR
SEQ
CLAIM x -- Claim the EREW "handle" (pointer)
c ! VAR x -- The new x, but that is ok
c ? VAR x -- Pointless except for illustration
... more CREW stuff on the original CREW x
xm IS MOBILE x : -- New name more obvious
PAR
c ? VAR xm -- ok since xm is same pointer as in declaration of c
SEQ
CLAIM xm -- collect the pointer
c ! VAR xm
... back to usual CREW x usage
--}}}
--{{{ 5) Mobile slices
MOBILE [2 * N]BYTE mem:
first IS MOBILE [mem FROM 0 FOR N]:
second IS MOBILE [mem FROM N] :
CHAN OF VAR first,second c1,c2:
PAR
--{{{ single ping
PAR
SEQ
CLAIM first
c1 ! VAR first
c2 ? VAR second
--}}}
--{{{ single pong
PAR
c1 ? VAR first
SEQ
CLAIM second
c2 ! VAR second
--}}}
--}}}
--{{{ 6) Subabbreviation
MOBILE [2]INT x :
whole IS MOBILE x :
CHAN OF VAR whole c:
SEQ
PAR
SEQ
CLAIM whole
c ! VAR whole
c ? VAR whole
first IS MOBILE whole[0]:
second IS MOBILE whole[1]:
CHAN OF VAR first d :
CHAN OF VAR second e :
PAR
SEQ
CLAIM first
d ! VAR first
e ? VAR second
SEQ
CLAIM second
e ! VAR second
d ? VAR first
--}}}
--{{{ 7) ping/pong
[2] MOBILE [rows][cols]INT image: -- MOBILE [2][rows][cols]INT image:
-- also allowed since mobile
-- applies to whole address range
--{{{ produce
PROC produce(CHAN OF VAR [rows][cols]INT image[0],
[rows][cols]INT image[1] in,out)
INITIAL INT i IS 1:
SEQ
WHILE TRUE
pong IS MOBILE image[i]:
SEQ
i := i >< 1
ping IS MOBILE image[i]:
PAR
SEQ
CLAIM ping
... fill ping from camera
out ! VAR ping
in ? CASE VAR pong
:
--}}}
--{{{ consume
PROC consume(CHAN OF VAR [rows][cols]INT image[0],
[rows][cols]INT image[1] in,out:)
INITIAL INT i IS 1:
WHILE TRUE
pong IS MOBILE image[i]:
SEQ
i := i >< 1
ping IS MOBILE image[i]:
PAR
SEQ
CLAIM pong
out ! VAR pong
SEQ
in ? CASE VAR ping
... process
:
--}}}
CHAN OF VAR image[0],image[1] up,down:
PAR
produce(down,up)
consume(up,down)
--}}}
--}}}
Adrian
--
A E Lawrence, MA., DPhil. adrian.lawrence@xxxxxxxxxxxxxx
MicroProcessor Unit, 13, Banbury Road, Oxford. OX2 6NN. UK.
Voice: (+44)-1865-273274, Fax: (+44)-1865-273275