Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches

verdagon.dev

Post reply on HN
Print view View original

111–120 of 143 posts

Re: Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches

#111

Post by ryao »

bitbasher wrote: post #68

I'm kinda torn. It seems there are only three approaches. 1. laissez-faire / manual memory management (c, c++, etc) In this approach, the programmer decides everything. 2. dictatorship / garbage collection (java, go, etc) In this approach, the runtime decides everything. 3. deterministic / lifetime memory management (rust, c with arenas, etc) In this approach, the problem determines everything.

There is another option, which is to use a sound static analyzer that can prove the absence of memory safety issues like astree, and fix things that cause it to complain until it stops complaining:

https://www.absint.com/astree/index.htm

For those who think static analyzers cannot do that, notice the word “sound”. This is a different type of static analyzer than the more common ones that do not catch everything.

Sadly, there is no open source option that works across a broad range of software. NASA’s IKOS is open source for example, but it does not support multithreading and some other things that I do not recall offhand, which makes it unable to catch all memory safety bugs in software using the features that it does not support. For now, people who want to use sound static analyzers need to use closed source tools or restrict themselves to a subset of what C/C++ can do so they can use IKOS:

https://github.com/NASA-SW-VnV/ikos

Re: Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches

#112

Post by eklitzke »

I don't understand why they say that reference counting is "slow". Slow compared to what? Atomic increments/decrements to integers are one of the fastest operations you can do on modern x86 and ARM hardware, and except in pathological cases will pretty much always be faster than pointer chasing done in a traditional mark and sweep VMs.

This isn't to say reference counting is without problems (there are plenty of them, inability to collect cyclical references being the most well known), but I don't normally think of it as a slow technique, particularly on modern CPUs.

Re: Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches

#113

Post by diath »

the__alchemist wrote: post #79
constantcrying wrote: post #78

Earlier quoted context omitted.

>I've seen usually involve pointers. If only C++ had a thing called "references", which conveniently also used the "&" symbol and are a way to do exactly this without pointers. https://en.cppreference.com/w/cpp/language/reference

I stand corrected on C++. Can you think of any other languages? Of the ones I listed, I use all of, and am continuously frustrated by this limitation.

Most low-level languages support this, references in C++, pointers in C, ref keyword in C# and Dlang, and so on. It's mostly higher-level languages that do not support such things because it's in the VM semantics that dictate how objects are passed (i.e. in Lua tables are passed by reference, non-table values are passed by copy).

Re: Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches

#114

Post by immibis »

MMM++ is a variation of standard malloc/free. You can still UAF, but only to another object of the same type, which may or may not prevent an exploit.

Something that's missing is full-on formal verification where you write unrestricted C code and then mathematically prove it doesn't have any bugs. Nobody does this because proving a C program is correct is harder than mining a bitcoin block by hand, but it's useful to anchor one end of the safety/freedom spectrum. Many other approaches (such as borrow checking) can also be viewed as variants of this where you restrict the allowed program constructs to ones that are easier to prove things about.

Re: Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches

#115

Post by dang »

alexisread wrote: post #24

Previous discussion: https://news.ycombinator.com/item?id=40146615 https://news.ycombinator.com/item?id=41974185

Thanks! Macroexpanded:

Borrow Checking, RC, GC, and the Eleven (!) Other Memory Safety Approaches - https://news.ycombinator.com/item?id=41974185 - Oct 2024 (1 comment)

Borrow Checking, RC, GC, and the Eleven () Other Memory Safety Approaches - https://news.ycombinator.com/item?id=40146615 - April 2024 (68 comments)

Re: Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches

#116

Post by voxl »

ryao wrote: post #111
bitbasher wrote: post #68

I'm kinda torn. It seems there are only three approaches. 1. laissez-faire / manual memory management (c, c++, etc) In this approach, the programmer decides everything. 2. dictatorship / garbage collection (java, go, etc) In this approach, the runtime decides everything. 3. deterministic / lifetime memory management (rust, c with arenas, etc) In this approach, the problem determines everything.

There is another option, which is to use a sound static analyzer that can prove the absence of memory safety issues like astree, and fix things that cause it to complain until it stops complaining: https://www.absint.com/astree/index.htm For those who think static analyzers cannot do that, notice the word “sound”. This is a different type of static analyzer than the more common ones that do not catch everything. Sadl…

Even in their own list of features "Memory Safety" does not pop up, and none of the listed features indicate to me that they would entail memory safety. Academics aren't publishing droves of work on separation logic for a problem that can be solved by 1980s static analyzers.

Re: Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches

#117

Post by lilyball »

I don't see any mention of epoch-based garbage collection (see crossbeam https://docs.rs/crossbeam/latest/crossbeam/epoch/index.html). Generational References sounds like a related concept but it's not the same. I'm also surprised nobody's mentioned that one lance corporal goat yet.

Re: Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches

#118

Post by akkad33 »

mastax wrote: post #50
naasking wrote: post #40

More people need to read up on C#'s ref's: https://em-tg.github.io/csborrow/ These kinda-sorta fall under borrow checking or regions, just without any annotations. Then again, Ada/Spark's strategy also technically falls under Tofte-Talpin regions: https://www.cs.cornell.edu/people/fluet/research/substruct-r...

Yeah C# is very well designed for gradually introducing low level concepts for performance.

Also F#

Re: Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches

#119

Post by neonsunset »

akkad33 wrote: post #118
mastax wrote: post #50

Earlier quoted context omitted.

Yeah C# is very well designed for gradually introducing low level concepts for performance.

Also F#

As of now - F# needs more work w.r.t. support for [] types and byrefs. There's a reason ref lifetime analysis in Roslyn is quite a sophisticated part of its implementation even if most developers aren't aware of it.

F# has other cool features like `inline` bindings and [] function attributes but I found it more difficult to work with for systems programming when attempting to stay within safe constructs.

But if you don't need byrefs, ref structs and spans, then regular pointer-based or even array-based code is quite pleasant to write, for example https://benchmarksgame-team.pages.debian.net/benchmarksgame/...

With that said - F# is an incredible language, but for systems programming you are likely to get better results in C#. I hope eventually someone contributes subsequent spec and compiler work to change this (and if you think you have time and could try it - please do! it's a nice small community).

Re: Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches

#120

Post by akkad33 »

neonsunset wrote: post #119
akkad33 wrote: post #118

Earlier quoted context omitted.

Also F#

As of now - F# needs more work w.r.t. support for [ ] types and byref s. There's a reason ref lifetime analysis in Roslyn is quite a sophisticated part of its implementation even if most developers aren't aware of it. F# has other cool features like `inline` bindings and [ ] function attributes but I found it more difficult to work with for systems programming when attempting to stay within safe constructs. But if yo…

Doesn't F# have byrefs, inrefs and outrefs. How are they different from C# refs? Asking as someone with surface level knowledge of both languages https://learn.microsoft.com/en-us/dotnet/fsharp/language-ref...
Post reply on HN