Re: a dozen cpu's on a chip

MooseFET wrote:
On May 13, 12:04 am, Martin Brown <|||newspam...@xxxxxxxxxxxxxxxxxx>
wrote:
MooseFET wrote:
On May 12, 8:12 am, John Larkin
<jjlar...@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx> wrote:
[....]
show off how tricky they can be. Something without pointers. Something
that is impossible to crash.
No nontrivial language can ever be proven to be imposible to crash.
Minimalist languages like Modula2 have been proved to be formally
correct

I would like to see this proof. I seriously doubt that there isn't an
error in it like the one pointed out by Godel in set theory. It may
also not be a proof at all. Many so called proofs are just arguments
that a proof could be done and not actual proofs. To be a proof all
the steps must be shown.

It is the output of ISO WG13 so you have to buy the (very) expensive ISO standard if you want to play with it. However, there are several compilers still available which implement ISO M2. Personally I don't like their choice of syntactic sugar, but I can see why they did things. I subscribed to another M2 dialect. By the time the full spec was published most industrial people had moved to other languages for purely commercial reasons.

The specification is in VDM-SL which can be checked by software tools. It isn't very easy to read though. A small piece is online as an example and is a bit out of date but gives the flavour.

http://freepages.modula2.org/downloads/process2.pdf

AFAIK it is one of only a handful of non-trivial languages with a complete formal language specification that has been machine checked.

and compilers that implement the formal specification exist.

Some problems with the Viper chip showed that hardware struggles with formal proof of correctness too.

The static testing possible with that strict Pascal like grammar catches
a very large proportion of common programming errors at (pre) compile
time. It is still possible to write something that will crash, but you
have to try a lot harder to do it.

I write a lot in Pascal. Although the strict type checking and more
obvious syntax does prevent 90% of mistakes, it still leaves the 10%.
Run time checking prevents some conditions from continuing to do
damage but the program still bombs.

Some of the better static analysis tools for Modula2 can see into the program and find very deep faults that would not be found in normal execution. Apparently reliable working libraries were found to have a few flaws when the most successful static testing tools became available.

If you include hung systems in crashed ones, the problem becomes much
harder (even though it started out as imposible).

Halting problems are notoriously difficult.

Ada's high integrity subset for safety critical work is another one.

Did you know that there was a mistake in the spec for ADA that allowed
"correct" compilers to produce two different results from the same
source code. I have the details around here somewhere. It was

No. Although I was never a great fan of Ada.

something very nonobvious about what type an expression had. It takes
some pages of coding to make the problem show.

I think it was John Barnes at Praxis that did the high integrity stuff.

I assume that the subset was made after this was discovered.

I suspect LISP comes pretty close to being impossible to crash, but when
you include practical implementations some of the OS impurities will
provide ample opportunity to bring the thing to its knees.

Since LISP isn't compiled it is a lot harder to imagine it killing a
system its self but the base interpreter can't be written in LISP so
the error would be there.

It is a common misconception that Lisp is always interpretted. I was involved long ago in the development of a Common Lisp Compiler. There are incremental Lisp compilers which may look from the outside like interpretters but generate fast native code. The whole compiler and its libraries was written in Lisp and bootstrapped with a Lisp interpretter onto new hardware. Only the deepest layer of OS interface was done in assembler it ran on the Mac and later on the PC.

For my money any routine that attempts to read from uninitiallised
memory, or write to memory it doesn't own should be terminated with a
page fault there and then (unless the location has been pre-defined as
memory mapped I/O).

Ownership should be strictly enforced for this to work. On the
various X86 machines the hardware does exist that could allow the OS
to lock things down. It would make the call process a lot slower but
in critical systems it may be worth it.

OS/2 was pretty good in this respect. Step out of line and your process gets swatted before it can do any harm.

I think that hardware designers could do a lot to improve matters.
Having a call-return stack, a parameter stack, return value area, and
local variables area all independant and enforced in hardware would
make it much harder to mess things up.

Limiting address range each process is allowed to access will do.

When a pass by reference is done, the reference could contain the
permissions and size information so that the called routine would be
restricted to only writing where the callee wants it to.

You do have to be careful you don't create something that is unweildly. x86 has an array BOUND instruction but I can't recall ever seeing it used in anger. The Modula2 solution was to have pragmas that allowed development code to insert preambles and postambles to defend against stack overflow, numeric faults, page faults etc and a kernel to return a traceback or postmortem dump that would identify the failing code. The traceback still worked in prodcuction code but the testing was disabled.

The first PC compilers with these capabilites were around in the mid 1980's distributed by Logitech (now better know for its mouse).

Regards,
Martin Brown
** Posted from http://www.teranews.com **
.

Relevant Pages

  • Re: How Common Lisp sucks
    ... smattering of scripting languages around the edges). ... using different compilers on every ... SBCL/x86 virtual machine with a program compiled for the clisp virtual ... None of this is meant to detract from lisp. ...
    (comp.lang.lisp)
  • Re: merits of Lisp vs Python
    ... intelligent machines you need another path, that is what has not been ... Lisp compilers will generate better and better code. ... languages like C where much of the work has been done. ...
    (comp.lang.lisp)
  • Re: Is octave good to do image processing?
    ... But in any case I consider it untrue that a Lisp program is more ... modern languages and compilers are completely cache unaware. ... compilers that allow you to exploit the full power of your hardware. ... You know what languages hardware drivers are written in by the ...
    (comp.dsp)
  • Re: Why dont we have "C" machines? (was Re: [OT] Re: Should *most* memory be release back to the sys
    ... written either in assembler or other "system programming" languages like ... But now most operating systems are written in C, most compilers ... single task OSes, and multitasking OSes. ... OS (assuming that a lisp machine is the thing where you basically run ...
    (comp.lang.ruby)
  • Re: New Computer Language Shootout?
    ... In Lisp functions, variables and macros usually have longish names. ... compilers, I think. ... learned from the lisp culture and I use it in all the languages I ...
    (comp.lang.lisp)