OSDev.org

Hi

Most of the memory managers in today's interpreted/jitted/AOTed languages like Java, .NET etc. are coded in native languages which are inherently type unsafe.

I was wondering if there is any way by which i can write a memory manager and garbage collector in a _completely_ type safe way?

I have banged my head for hours on this, and could not find a solution that is completely type safe - and hence verifiable and hence dependable.

i intend to reduce the % of trusted components from my implementation - as the general trend goes - more verifiable -> more dependable and secure(well not exactly, but kind of).

Type-safe garbage collection is an area of active research. It is not achievable without creating a new language with a new type system that is specialized for the task at hand. The kind of logic proofs and math involved in this kind of research is way over my head -- it's something I would like to learn if I ever get my Master's degree.

If you're interested, there are a few research papers out there on the topic. Here is one of the first links I found:

http://www.cs.princeton.edu/sip/projects/garbage/

BTW, I think this belongs in "OS Design & Theory".

Is that even math in that paper
That should be enough to keep me engaged for days.

what i understand from all the references, is that doing a type safe GC in Java as of now seems impossible, since we will have to make changes to java bytecode.

is that correct, or am i missing something?

Thanks

I'm not sure -- I haven't had the time to wade through all the greek letters in those papers. I'm guessing that changing the bytecode isn't really going to help. Instead, a new higher-level language is needed with a new type system that can express the abstract operations performed by a GC. I think the idea is that a compiler for this new language would produce code, as well as metadata that can be used as a proof that the code is type-safe according to the rules of the new language. Formal proofs are required to show that the language itself is "safe" in this sense.

What about LLVM?

What about it? It's an intermediate instruction format. As I said, code by itself (whether bytecode, native code, or otherwise) isn't sufficient to prove whether a GC implementation is type-safe.

Right, I just pointed it out because they seem to put some kind of type information on their intermediate code. Forgive my ignorance, I haven't learned formal proofs of programs yet.

You could try D http://www.digitalmars.com/d/index.html
http://en.wikipedia.org/wiki/D_programming_language

As much as I like D, Phobos and the language itself don't seem stable enough for use on bare metal.

Also, I don't see how its garbage collector (which you must disable at the bare-metal level) helps create a type-safe memory manager.

I don't know much about creating a memory manager or using a language on bare metal but I read a document about type safe os and it mentions a couple of things that is type safe and that D has.

http://svn.dsource.org/projects/titan/t ... SafeOS.pdf

http://cyclone.thelanguage.org/

I couldn't find any mention of D in that paper, nor of using Clay to implement type-safe memory management code.



Thanks for the link -- that looks interesting, especially the part about regions.

It sounds like they were able to implement a simple stop & copy GC using Cyclone, but that it required a certain amount of hacking.

From here:

I never said it mentioned D, but i mentions a couple of type safe features that Clay has that (if understand them correct) D also has. I also never said it implement type safe memory management code, I thought if you had a type safe language you could write type safe memory management code.

Yes, if the type system is expressive enough, but for languages like Java, C#, and D, it's not.

Think of it like this -- type safety is really just being used a proxy for memory safety. What we really want to avoid at the end of the day is leaked memory, reading from or writing to memory that doesn't belong to our program, etc. All that type safety means is that the language enforces a certain kind of consistency -- any operation you can express must follow certain rules. Type systems in conventional GC'd languages are geared towards guaranteeing basic memory safety -- that is, if you follow the rules, your program is type-safe, and because the type system is designed properly, it is also memory-safe.

The problem with GCs and memory managers is that they do things to untyped memory all the time. There are relationships and characteristics of those memory regions manipulated by a GC or MM that are not possible to formalize using a conventional type system (as the OP has discovered).

Try writing a type-safe GC or memory manager and you'll see what the problem is, even if it's difficult to put into words.