Warp wrote:
> Invisible <voi### [at] devnull> wrote:
>> Their approach seems to be to "verify" each program before it runs, 
>> checking that it doesn't do any "bad" things.
> 
>   That's impossible. It can be proven that it's an unsolvable problem,
> exactly for the same reason as the halting problem is unsolvable. There's
> no way for any program to check if a piece of code is executed and how.

This isn't quite true. If you restrict the forms of programs you accept 
to something you can verify, then you can do this pretty easily. It is, 
for example, why people are willing to run java applets in their browser.

While it's true the halting problem prevents you from knowing whether 
any arbitrary TM will halt, it doesn't prevent you from knowing whether 
any arbitrary regular expression will halt, for example. If you 
eliminate the instructions that let you write to arbitrary parts of 
memory you don't own, then it's not too hard to check your language 
works fine.

It's also the case that hardware doesn't 100% solve the problem either. 
You have to (a) trust the hardware not to be buggy, and (b) trust the OS 
to correctly set up the hardware.

>   It's also impossible for it to know, for example, the addresses of all
> pointers by simply examining the program (for example the address of a
> pointer could be calculated from user input).

No, because the OS won't install a program that calculates the address 
of a pointer calculated from user input. Basically, you use C# or one of 
the other .NET languages, that compiles down to a strongly-typed 
assembly language. Then, before you run the program, you gather up all 
the strongly typed assembler,

>> Presumably verifying whether a program does or does not do something 
>> "bad" is formally equivilent to the halting problem, so I imagine they 
>> apply some arbitrary set of restrictions to simplify the problem.
> 
>   Those restrictions could seriously hinder compiler optimizations.

Actually, it turns out the compiler can do a *much* better job, because 
it can track the usage of a whole bunch of stuff that's hard to track 
when you allow arbitrary pointers.

> For example accessing the nth element of an array can usually be done
> with a simple CPU opcode. However, if the system restricts this because
> it cannot prove what that n might contain, it means that the compiler
> cannot generate the single opcode for accessing that array, but must
> perform something much more complicated to keep the system happy.

Right. They actually check this, and discover it's about a 4% overhead 
to do the checks in software. And it's about a 6% overhead to do the 
checks in hardware.  Where Is Your God Now?  Mwa ha ha ha!  ;-)

And it's about a 33% overhead to actually put processes in different 
address spaces and enforce that they can't change the VM mapping by 
taking away the ring-0 instructions, compared to checking at compile 
time that you don't go out of bounds and enforcing at runtime where you 
can't check at compile time, once you count up TLB misses, TLB flushes, 
frobbing stacks around during an interrupt, etc.

>   Ah, but that's the trend nowadays: Computers get faster and the amount
> of RAM grows exponentially with time. There's no need for highly optimized
> code.

You should read the papers. *Because* the input is actually structured, 
they can compile the stuff and throw away (for example) fields and 
methods that aren't used, include a GC that's specific to the problem 
being solved (e.g., a higher-overhead real-time GC only for real-time 
programs), and they get a tremendous efficiency boost.

-- 
Darren New / San Diego, CA, USA (PST)
  Ever notice how people in a zombie movie never already know how to
  kill zombies? Ask 100 random people in America how to kill someone
  who has reanimated from the dead in a secret viral weapons lab,
  and how many do you think already know you need a head-shot?

Post a reply to this message