[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Mobile variables
Adrian,
This is something to help us conform to AUT guidelines on industrial
action during exam marking ...
> This is so obvious that it must have been suggested before?
There was a lot of chat about such things back in '94 ... John Burren,
myself and some others on the old occam3-talk mailing list (occam3-talk
became occam-com when we gave up waiting on occam3 :-() ...
Enclosed is one message from June '94 (when, like now, I was trying to
do anything but exam marking!). Points:
1. Your scheme prevents the sending of mobile-EREW (Exclusive-Read-
Exclusive-Write) variables out of scope - which is a good thing.
2. Mine didn't, although you couldn't actually make use of a received
TOKEN if the SHARED variable it was representing was out of scope.
But you could send it back again to a process where the SHARED
variable was in scope, which could then re-access it. This opened
a tiny security loophole, hinted at but not explained in the enclosed
mailing. There was a fix for this but, in the spirit of Fermat,
was omitted for brevity. The fix was in the implementation of the
TOKEN and in the SHARED variable - not in the syntax or semantics.
Sorry, still no time to explain!
3. In your produce/consume example, shouldn't the "[2]"s in the parameter
lists be omitted? When defining the network, shoudn't "consume(up,down)"
be "consume(down,up)"?
4. Your scheme hides the explicit TOKENs of my suggestion :-) ...
Anyway, here is the produce/consume example using the '94 suggestion - well,
it's better than marking ... and we are supposed to be on exam-strike :-)
PROC producer ([2]SHARED [rows][cols]INT image, -- EREW shared references
[2]TOKEN token, -- tokens for image
VAL INT valid, -- index of valid token
CHAN OF TOKEN in, out)
INITIAL INT ping IS valid, pong IS ping >< 1:
WHILE TRUE
-- invariant : token[ping] is VALID for image[ping]
-- invariant : token[pong] is INVALID
SEQ
PAR
SEQ
CLAIM image[ping] WITH token[ping]
... fill image[ping] from camera
out ! token[ping]
in ? token[pong]
ping, pong := pong, ping
:
PROC consumer ([2]SHARED [rows][cols]INT image, -- EREW shared references
[2]TOKEN token, -- tokens for image
VAL INT valid, -- index of valid token
CHAN OF TOKEN in, out)
INITIAL INT ping IS valid, pong IS ping >< 1:
WHILE TRUE
-- invariant : token[ping] is VALID for image[ping]
-- invariant : token[pong] is INVALID
SEQ
PAR
out ! token[ping]
SEQ
in ? token[pong]
CLAIM image[pong] WITH token[pong]
... process image[pong]
ping, pong := pong, ping
:
To set up the network, first declare the SHARED images:
[2]SHARED [rows][cols]INT image TOKEN token:
This declares an array of 2 SHARED images with corresponding tokens.
Initially, token[0] is valid for image[0] and token[1] for image[1].
Then, just a normal PAR:
CHAN OF TOKEN c, d:
PAR
producer (image, [token[0], INVALID], 0, c, d)
consumer (image, [INVALID, token[1]], 1, d, c)
where two [2]TOKEN arrays are constructed on-the-fly. The parallel useage
rules see token[0] and token[1] used as read/write data in separate parallel
processes and should pass it. The dynamic token validity checks (both on
the CLAIMs and on the token passing) will all pass at run-time.
And now ... it's lunch time ;-)
Peter.
=============================================================================
Date: Fri, 03 Jun 94 11:56:30 +0100
From: phw@xxxxxxxxx
To: occam3-talk@xxxxxxxxxxxxxx
Subject: Tokens and shared data
X-List: occam3-talk@xxxxxxxxxxxxxx
Reply-To: occam3-talk@xxxxxxxxxxxxxx
Sender: occam3-talk-request@xxxxxxxxxxxxxx
Precedence: list
Status: RO
Note to John Burren, DRAL (3/6/94):
(cut here)
-----------------------------------------------------------------------------
John,
Prompted by your note, I looked again at my WoTUG News (15) article [1]
on `securely managed pointers'. What you have suggested seems to
overcome very elegantly the problem of dangling pointers thrown up by
my suggestions and operates semantically at a higher level - i.e. it
is easier to understand!
Summarising: I proposed passing pointers so that a process could only
access a shared data-structure once it has obtained a pointer to it.
Only one copy of the pointer value exists at any time. The difficult
problem was to prevent this pointer value being passed out of the scope
of the data-structure to which it pointed. The `solution' I suggested
was not given in detail and, I suspect, might not stand too close
inspection!
The pointer acts as a `token', giving permission to the possesor to
operate on the shared data-structure. Thinking of these things
directly as TOKENs (rather than as POINTERs) may be a better idea.
A way to overcome the out-of-scope problem is to insist that the
process wanting to access the shared structure must be able to see it
(i.e. is in its scope) *and* posseses a valid token for it ... in my
outline, the process wanting to access the shared structure only needed
a valid pointer. I think the pointer proposal could be patched in the
light of this insight, but let's try using your terminolgy.
It might go something like this:
o Introduce a token-type into the language ... this is distinct from a
data-type (or channel-type or port-type or timer-type or module-type):
TOKEN a, b, c, d:
A TOKEN takes two values - valid and invalid. When valid, it will
be valid for a specific data-structure only. The tokens declared
above are all initialised to invalid.
[Implementation note: a TOKEN will be implemented by one word. A valid
token will contain the address of the data structure it is validating.
An invalid token will contain the address `not.a.structure' - this
is very similar to channels!]
o A second way to declare a token is to bind it (initially) to the
declaration of a data-structure that is going to be shared (securely!)
amongst parallel processes. Suppose we have a data-type called THING.
Then:
SHARED THING x TOKEN t:
declares a data variable x and a token variable t, initialising t to
be valid for x (i.e. putting the address of x into t).
o Usage rules:
o a SHARED variable may be freely shared amongst parallel processes
(even though they may all be modifying its value - see below);
o a TOKEN variable should always be marked as `read/write'. Two or
more parallel processes are not allowed to refer to it.
[Motivation: like channels, tokens are very hard to use without
causing a side-effect. As a consequence, only reference TOKEN
parameters or abbreviations should be allowed - no VAL TOKENs.]
o Channels may carry TOKEN values as (part of) their PROTOCOL.
o Only valid TOKEN values may be assigned or communicated. The
recipient TOKEN variable must be invalid prior to this and the
donor TOKEN variable is marked invalid afterwards. This may
involve run-time checks. This enforces a strong conservation
law for valid token values ... only one copy ever exists and
it can't get lost. We get the law:
(T0) two token variables cannot be simultaenously valid for
the same data-structure.
[Note: these are the same rules as given for pointers in [1]. The
law (T0) corresponds to the (P0') one given there.]
o To access a SHARED variable, a process must be in its scope AND
must possess a valid TOKEN for it. A simple syntax that enforces
this is:
CLAIM x WITH t
... process that uses/modifies x
Any attempt to access x outside the (indented) body of such a CLAIM
will be rejected by the compiler. Any attempt to use t inside the
body of such a CLAIM (e.g. to give it away!) will also be rejected
by the compiler. A run-time check needs to be made to ensure that
t is valid for x (i.e. t points to x).
Note that this CLAIM is not a synchronisation point! If t is not
valid for x, this is a run-time error. An ELSE-clause should not
be provided!! The claimant needs to know which shared variable
the token gives permission to use ... sometimes this may require
further information to be communicated to the claimant alongside
the token. By making the claimant name the variable being claimed,
we prevent processes following the token-pointer into a workspace
it should not be able to see ... this was the problem before with
just using pointers.
The method for working with shared variables is as follows:
SHARED THING x TOKEN t:
... declare local channels
PAR
... process A
... process B
... process C
Only one of the processes (say A) can use the TOKEN t (a consequence of
the normal parallel useage rules for shared read/write variables) and has,
therefore, initial permission to access x. The other processes must have
their own local TOKEN variables that, of course, cannot initially be used
to access x.
Permission to access x is then passed between the processes A, B and C
using TOKEN-carrying local channels. Only one process can have this
permission at any one time. We are quite safe ... incorrect alogorithms
will either not compile or will generate run-time errors (rather than
compile and run in a scheduling-dependent manner).
Note that SHARED data-structures, like channels, are used for communication
between parallel processes. Therefore, SHARED data-structures, like
channels, should only be declared in conjunction with the PAR-construct
that uses them ... i.e. SHARED declarations followed immediately by a SEQ
are as bad an offence as CHAN declarations followed immediately by a SEQ!
Following this reasoning, it may be safe and proper to allow a MODULE to
put SHARED data-structures into its interface (alongside TOKEN-carrying
and other channels) ... this needs some debate!
FINAL THOUGHTS
--------------
A good feature about this scheme is that it is architecturally neutral.
Restrictions in the placement of data variables for private-memory
T2/T4/T8/T9 architecures automatically prevent the mis-use of tokens
passed between processors. On the other hand, shared-memory architecures
can be safely and efficiently exploited ... without the need for special
hardware to maintain a consistent memory image across all processors.
I'll re-work the example of the shared buffer-pool mamager from [1] in
a separate posting with this new syntax. It raises a possibly nasty
problem of how - efficiently - to let the recipient of a buffer token
know which one from the pool it has been given permission to use?!!
It's also the case, sadly, that the TOKEN-implementation strategy given
above is not totally secure against abuse! But this is an implementation
detail that I think can be overcome with something only slightly more
sophisticated ... will ponder this some more!!
Peter Welch.
(3/6/94)
REFERENCES
[1] P.H.Welch: `Securely Managed Pointers', in WoTUG Newsletter No. 15,
pp. 35-40, July 1991.