Crash-proofing - execution tokens 
Author Message
 Crash-proofing - execution tokens

Having kicked off with the idea of a crash-proof layer for ANS Forth,
how can we tackle the problem of EXECUTE, which is attempts to execute
the top value on the Data Stack, whether it's an execution token or not.

If we redefine EXECUTE, how can it tell whether a value is (or is
probably) an execution token (xt)?

Given an indirect-threaded Forth, a valid xt is fairly easy to recognise

Does anyone have any universal solutions to this problem?

Bye for now                                                      
                                           ____/  /  __  /   /   /   /   /
Chris Jakeman                             /      /  /  _/   /   /   /  /
                                         __/    /  / __    /   /   /_/
at Peterborough, a cathedral            /      /  /   /   /   /   /  \
city 80 miles north of London.       __/    __/  ____/    ___/ __/   _\  
Where do you come from?          
                              Forth Interest Group United Kingdom Chapter
Voice +44 (0)1733 753489      at http://www.*-*-*.com/



Tue, 18 Jan 2000 03:00:00 GMT  
 Crash-proofing - execution tokens


Quote:

>Having kicked off with the idea of a crash-proof layer for ANS Forth,
>how can we tackle the problem of EXECUTE, which is attempts to execute
>the top value on the Data Stack, whether it's an execution token or
>not.
>If we redefine EXECUTE, how can it tell whether a value is (or is
>probably) an execution token (xt)?
>Given an indirect-threaded Forth, a valid xt is fairly easy to
>recognise (but only if your Forth allows you to access code addresses

>Does anyone have any universal solutions to this problem?

I have a universal solution, but probably not one you'd like.  I set up
a system of full type checking.  When the system creates an execution
token it gives it type xt, and that's the only way you can get anything
that's type xt.  You can put it on the stack, move it to the return
stack, put it in a variable, take it out and execute it, and it will
have type xt and be OK.  Anything the system didn't think was an
execution token when it was created, won't execute.

The limitation for execution tokens, apart from the complexity and the
tremendous performance hit, is that you can't do much to manipulate
them.  You might for example want to do arithmetic or bitwise
operations on execution tokens.  When you destroy an execution token
that way, the system isn't smart enough to know that you've revived it
if you do the same operations in reverse.  TRUE XOR TRUE XOR will give
you back what you started with, but how can a simple type-checking
system keep track of everything you've done?  I wound up allowing only
a few operations on execution tokens, = so you can tell if two are the
same, and maybe < and > (although it may be that ' ROT ' SWAP < is true
on one system and false on another, and it isn't clear what you'd do
with the information anyway).

My system can potentially be completely crash-proof, but you lose a
lot.  I found that I didn't want to use it for general debugging, I
only used it for checking ANS compatibility after things were running.

Occasionally it would complain about things that ought to be OK.  I'd
have to check carefully to make sure I was right and it was wrong
(surprisingly often I missed environmental dependencies that I should
have noticed).  Then if it didn't seem worth it to revise the system,
I'd check that piece of code by hand and then write out its effects --
stack diagram etc -- so I could test the routines that depended on it.

It's been awhile.  I should go back and revise it.  I got discouraged
when it seemed like no one was interested.



Wed, 19 Jan 2000 03:00:00 GMT  
 Crash-proofing - execution tokens


Quote:
> ...
> My system can potentially be completely crash-proof, but you lose a
> lot.  I found that I didn't want to use it for general debugging, I
> only used it for checking ANS compatibility after things were running.

        On approach that would add some memory overhead would be to
introduce a level of indirection to the execution tokens: when something
that can be the source of an XT is defined, it is stored in an XT table,
and the XT is an index into the table rather than the executable address
itself.  Or possibly the negative of the index into the table, to make the
value even less likely as a random Top Of Stack.  In any event, the
current extent of the xt table would be stored at the base of the XT
table, and EXECUTE could make a range check before executing.  The memory
/ execution overhead trade-off is whether to save the XT index with the
dictionary entry (the index itself, and maybe an extra cell following
LAST, is sufficient for anonymous XT's, since if they are consumed without
being saved somewhere, they can't be recovered anyway), or whether to
search in the XT table for the executable address when generating an XT on
the stack.

Virtually,

Bruce R. McFarling, Newcastle, NSW



Thu, 20 Jan 2000 03:00:00 GMT  
 Crash-proofing - execution tokens


Quote:

>> ...
>> My system can potentially be completely crash-proof, but you lose a
>> lot.  I found that I didn't want to use it for general debugging, I
>> only used it for checking ANS compatibility after things were running.

>    On approach that would add some memory overhead would be to
>introduce a level of indirection to the execution tokens: when something
>that can be the source of an XT is defined, it is stored in an XT table,
>and the XT is an index into the table rather than the executable address
>itself.

  This is one of the things that have always puzzeled me about Forth - the
assumption that an address on the stack is actually an address and treated

  In my own Forth-like lanaguage I wrote a few years ago, all data was typed
(and so was the data on both stacks) and I didn't seen any problems with
that, as it tended to catch bugs.  

  Surely, for a development environment, having the extra overhead is a Good
Thing, and once things work fine in the development (or debug) environment,
then you can take the code and drop it into a release environment, without
the overhead of checks.  If it runs without tripping any of the checks, then
it should run fine without the checks.

  I do this all the time now in C, using assert() (which if enabled, will
check the conditional expression given it and abort the program if the
condition is false, giving the location of the failure).  Yes, when my
programs have been compiled in full debug mode, it runs slow and consumes
more memory, but if it runs correctly in that mode, I can then re-compile it
in release mode and not have to worry about the program crashing (well, not
that often in any case).

  Type checking could also be used to generate stack diagrams.  I've been
doing some work in this, taking phrases [1] of Forth-like code, and seeing
if I can generate a stack diagram by running through it.  In most cases this
is fairly easy, but problems arise when such words as '?DUP' are
encountered, but it may still prove useful in any case.

  -spc ("You either say GO or you say PRETEND."
                -- Chuck Moore, quoted from _Thinking FORTH_,
                   page 231, Prentice-Hall, publisher and no,
                   I'm not willing to sell it 8-)



Thu, 20 Jan 2000 03:00:00 GMT  
 Crash-proofing - execution tokens



Quote:
>    On approach that would add some memory overhead would be to
>introduce a level of indirection to the execution tokens: when
>something that can be the source of an XT is defined, it is stored in
>an XT table, and the XT is an index into the table rather than the
>executable address itself.  Or possibly the negative of the index into
>the table, to make the value even less likely as a random Top Of
>Stack.  In any event, the current extent of the xt table would be
>stored at the base of the XT table, and EXECUTE could make a range
>check before executing.  The memory / execution overhead trade-off is
>whether to save the XT index with the dictionary entry (the index
>itself, and maybe an extra cell following LAST, is sufficient for
>anonymous XT's, since if they are consumed without being saved
>somewhere, they can't be recovered anyway), or whether to search in
>the XT table for the executable address when generating an XT on the
>stack.

That looks perfectly workable.  I'm sorry I didn't think of it.  You
could save the user :NONAME things too, since you don't know ahead of
time whether they'll be saved or not.  

I don't see any problems.



Thu, 20 Jan 2000 03:00:00 GMT  
 Crash-proofing - execution tokens



Quote:
>Having kicked off with the idea of a crash-proof layer for ANS Forth,
>how can we tackle the problem of EXECUTE, which is attempts to execute
>the top value on the Data Stack, whether it's an execution token or not.

>If we redefine EXECUTE, how can it tell whether a value is (or is
>probably) an execution token (xt)?

This newsgroup gets you great feedback.
I had forgotten that :NONAME generates an xt - thanks JET.
Indexing is faster than a searchable list - thanks Bruce.

To sum up the proposal then - the xts generated by ' ['] FIND and
:NONAME are saved in a table and an offset into the table returned.
When EXECUTE (and possible CATCH too) executes, we do a range check on
the offset then jump into the table for the real xt.

I have a go at coding this now and worry about FORGET and MARKER and so
on.  Thanks again.

Bye for now                                                      
                                           ____/  /  __  /   /   /   /   /
Chris Jakeman                             /      /  /  _/   /   /   /  /
                                         __/    /  / __    /   /   /_/
at Peterborough, a cathedral            /      /  /   /   /   /   /  \
city 80 miles north of London.       __/    __/  ____/    ___/ __/   _\  
Where do you come from?          
                              Forth Interest Group United Kingdom Chapter
Voice +44 (0)1733 753489      at http://www.forth.org/fig/uk/homepage.htm



Fri, 21 Jan 2000 03:00:00 GMT  
 Crash-proofing - execution tokens

-marcel



Fri, 21 Jan 2000 03:00:00 GMT  
 Crash-proofing - execution tokens


Quote:

>To sum up the proposal then - the xts generated by ' ['] FIND and
>:NONAME are saved in a table and an offset into the table returned.
>When EXECUTE (and possible CATCH too) executes, we do a range check on
>the offset then jump into the table for the real xt.

Don't forget SEARCH-WORDLIST .  Definitely CATCH too.


Fri, 21 Jan 2000 03:00:00 GMT  
 Crash-proofing - execution tokens


Quote:


> >       One approach that would add some memory overhead would be to
> >introduce a level of indirection to the execution tokens: when
> >something that can be the source of an XT is defined, it is stored in
> >an XT table, and the XT is an index into the table rather than the
> >executable address itself. ...
> That looks perfectly workable. ...  You could save the user :NONAME
> things too, since you don't know ahead of time whether they'll be
> saved or not.  
> I don't see any problems.

        :NONAME's would be saved in the table (as a previous message
indicated, if there is a distinction between a development system and a
release system, the indirection abd table overhead would be recovered when
you went to the release system).  It's the dictionary that would not have
to have an index saved for a ":NONAME".  If a valid XT is saved in a
variable, and then fetched and executed, the XT will be in the proper
range for indices into the XT table, so everything will be fine.

        Of course, the above is not entirely bulletproof, because it is
possible that the value will be in range for an index into the XT table,
even if the range is -1 to -XT-Table-length.  Another approach is a shadow
stack that mirrors the datastack with type information.  If one of
the strengths of Forth is that seperated data & return stacks are more
frugal in memory usage, surely a shadow of the data stack should be as
much within the reach of a development system as the other types of memory
overhead.

Virtually,

Bruce R. McFarling, Newcastle, NSW



Fri, 21 Jan 2000 03:00:00 GMT  
 Crash-proofing - execution tokens



Quote:

>> In


Quote:

>    :NONAME's would be saved in the table (as a previous message
>indicated, if there is a distinction between a development system and
>a release system, the indirection abd table overhead would be
>recovered when you went to the release system).  It's the dictionary
>that would not have to have an index saved for a ":NONAME".  If a
>valid XT is saved in a variable, and then fetched and executed, the XT
>will be in the proper range for indices into the XT table, so
>everything will be fine.

Yes.

Quote:
>    Of course, the above is not entirely bulletproof, because it is
>possible that the value will be in range for an index into the XT
>table, even if the range is -1 to -XT-Table-length.  

One approach would be to use the actual table addresses.  Then you'd

likely to get a random correct number by accident than you would a
small offset number.  If you've generated the address as an address
some other way, you're probably already in trouble.

Quote:
>Another approach is a shadow stack that mirrors the datastack with
>type information.  If one of the strengths of Forth is that seperated
>data & return stacks are more frugal in memory usage, surely a shadow
>of the data stack should be as much within the reach of a development
>system as the other types of memory overhead.

I did that.  It works.  You need shadow stacks for the data and return
stack to hold type information.  I found it easiest to have another
shadow return stack to hold user data; whenever I executed something I
pushed a nest-sys onto it.  Then I could check return stack use without
actually crashing the system.  8-)  You need shadow ALLOT areas to hold
type information, in case you store it.  And you need to rewrite every
word that affects the stack, to handle its effect on the type stacks.
This is in reach for a development system, but it's a lot of work.

Your approach handles xt's elegantly, without a lot of work.



Fri, 21 Jan 2000 03:00:00 GMT  
 
 [ 10 post ] 

 Relevant Pages 

1. COMPILE, use for non execution tokens

2. Word gets its own execution token?

3. ANS standard execution token and data field

4. RFI: execution tokens

5. Execution tokens

6. Execution tokens and ANS FORTH

7. execution token in dpANS-6

8. Crash-proofing

9. crash-proofing -- stack-effect checking

10. Crash proofing a clip applic's input

11. Eiffel and Crash-Proof Computing

12. token.f: my simple C token subroutine

 

 
Powered by phpBB® Forum Software