An unexpected perf feature

Posted May 23, 2013 4:34 UTC (Thu) by ebiederm (subscriber, #35028)
In reply to: An unexpected perf feature by Cyberax
Parent article: An unexpected perf feature

Talx86 can not accurately type programs encoded in assembly.

There are no dependent types for allowing the removal of bounds checks in array updates. Instead magic array macros must be used. (Not supporting general memory accesses is a signification failure in adding types to assembly language).

There is no support for multiprocessing.

There is no support for support for manual memory management. Talx86 requires a garbage collector.

Which means a large number of common kernel constructs can not be encoded in this assembler. We are unfortunately quite a ways from safe languages that can be used for kernel programming.

An unexpected perf feature

Posted May 23, 2013 4:39 UTC (Thu) by Cyberax (✭ supporter ✭, #52523) [Link]

Dependent types can be feasibly added and fat pointers are already supported in hardware (on a couple of exotic architectures, but still).

I don't see much problems with multithreading, though memory model formalization should be quite interesting.

Garbage collector of some sort seems inevitable in any case. Perhaps with some kind of region inference to help with short-lived allocations. In some limited cases it may be possible to use static proofs of correctness.