Stream: general

Topic: memory safety

Soni L. (Dec 03 2024 at 00:19):

is the JIT memory-safe?

Chris Fallin (Dec 03 2024 at 00:59):

Can you clarify what you mean? Memory-safe with respect to what API or action?

Chris Fallin (Dec 03 2024 at 01:00):

In general, you can JIT-compile code that loads or stores to any memory address, so if you invoke that code, the answer is necessarily "no". However the invocation itself is unsafe; if you consider the compiler itself as some abstract function from IR to machine-code bytes, that API is fully safe; it's "just" a computation.

Soni L. (Dec 03 2024 at 01:04):

so why not maintain memory safety all the way from the frontend down to the assembler. in particular, applying optimizations while maintaining memory safety.

Soni L. (Dec 03 2024 at 01:06):

(like yeah you can't maintain memory safety in the machine code layer, but you should be able to in every other layer above that including the assembler)

Soni L. (Dec 03 2024 at 01:07):

(tho, using this definition of memory safety, we can say that there are no memory-safe programming languages today)

Chris Fallin (Dec 03 2024 at 01:13):

I'm not really sure what you mean. I've worked on formal verification of Cranelift; are you talking about translation validation? Are you talking about memory safety of the compilation process itself? It would be useful to understand what you are thinking when you say "memory safety"; it's not just a buzzword, it is a nuanced term that can mean different things in different contexts.

Soni L. (Dec 03 2024 at 01:14):

well, ultimately memory safety comes from typing and constraint checking. so, we should maintain full typing all the way from the frontend down to the assembler. no compiler we know of does this today.

Soni L. (Dec 03 2024 at 01:15):

ofc, it may be necessary to peel layers off types while dealing with some of those lower-level constructs, but the relevant passes, the assembler, etc should still be able to constraint check the entire thing.

Chris Fallin (Dec 03 2024 at 01:16):

OK, you're talking about type-preserving compilation. Yes, that'd be really neat. As I'm sure you're aware, it's a research challenge, especially if you want a formal proof (even in a translation-validation sense, i.e., a witness object for one compilation as opposed to a forall-proof ahead of time) of the correspondence.

Chris Fallin (Dec 03 2024 at 01:17):

You'd also probably want something like dependent typing, or at least refinement typing, to encode invariants that JIT producers routinely make use of -- once you lock the hatches and say everything must be typesafe, you need a way to put all the system invariants in the types

Chris Fallin (Dec 03 2024 at 01:18):

I'd welcome you to study this, produce a set of solutions, and write the three PhD theses that would result from all of the ideas necessary to make it practical :-)

Soni L. (Dec 03 2024 at 01:19):

peeling the type layers is usually done with unsafe in rust, where you translate (e.g. transmute) one set of types into a different set of types, each enforcing the constraints in different ways (this is often done with e.g. lifetimes)

Soni L. (Dec 03 2024 at 01:20):

but yes we understand that's an escape hatch

Last updated: Dec 23 2024 at 12:05 UTC