The Cerberus C semantics [pdf]
cl.cam.ac.uk
cl.cam.ac.uk
Software that needs to be written in C, as opposed to in friendlier or more aggressively constrained languages, is that which needs to deal in hardware. Things like there's a value at absolute address k which you load from to indicate to some other part of the system that a thing has happened.
The domain is exclusively stuff that can be written in asm but it's cheaper and saner not to.
The pointer provenance strategy miscompiles enough of that domain to be unsafe to use. It interacts particularly poorly with the aliasing model that thwarts treating memory as an array of integers, or an array of atomic integers, or an array of simd types.
The end game of this "sound semantics" strategy, as favoured by WG14, is a language with zero use cases. You can't put it near hardware without fno-strict-aliasing and whatever flag turns off provenance based reasoning. You don't want to put it near anything else because C++ freestanding, D and rust are all faster and safer.
It's interesting work that can help provide sane semantics for fairly low level code. It's a real shame that it comes at the price of killing C.
edit: I read the chapters on memory and provenance. The authors are aware that provenance doesn't correspond to programs as written, and propose a few variations on it to try to open well judged escape hatches. As expected prior to writing the above rant. It's still miscompile by default when dealing with the real machine.
Pointer provenance does nothing to stop you from accessing stuff at a fixed address, it simply justifies things that current compilers already do and will not change. For example, even if you were to guess the address of a local, pointer provenance prevents you from changing it. This enables (really basic!) optimizations like moving variables into registers.
Type based alias analysis is a hack from separate compilation using compilers on limited hardware resources. It should be dropped as an unnecessary compromise to language expressivity, not leaned into as a law of nature.
The question of pointer provenance is really about trying to formalize a workable definition of "escape." This turns out to be far harder than it looks, because it turns out that converting a pointer to integer necessarily needs to be an escape, and all of a sudden, there are all sorts of hidden places that causes pointers to become integers that you never expected (such as storing a pointer in a stack variable, if memory is untyped).
I agree strict aliasing is a relic of the past that should be abolished ASAP, but that's quite different from pointer provenance.
Application level C++ developers want it too, as it makes things slightly faster without breaking anything that would get past code review.
My point of contention is with applying this to C. The main remaining uses are things like linux which can't be compiled as ISO C any more, instead requiring a bunch of compiler flags to opt out of things very like the provenance model.
I claim there are zero use cases for C with "strict aliasing" rules and the like, and adopting the application facing copy-ideas-from-C++ approach will/has killed the language. GNU C will persist for a while, ISO C serves noone well.
Can you elaborate? An mmap of prebuilt hash tables doesn’t work well in practice of the mmapped area contains pointers regardless of provenance, and an mmap of a hashtable that uses integer offsets doesn’t involve pointers.
The only real issue I see is if the mmap contains objects but isn’t itself laid out like an object in the language in question, and you need to generate a pointer to one of those objects. (So mmapping an array of structs that don’t contain pointers is fine, but mmapping a mess that contains integer offsets referencing various things in the mmap that don’t nicely line up like an array is harder.)
But I imagine that a pointer provenance system could have an operation that takes as input an mmap, an offset and a type and returns a pointer to the object with the type in question at the offset in question. It would check that the type makes sense (no pointers!) and could, if needed for the degree of safety require, also check for invalid aliasing.
A solution to both would be nice.
PNVI-ae-udi looks to be the one that compiler developers and the committee agree on, but we'll see if these efforts gain any more traction.
Though I'm reminded of a question after a talk around ~1990. Someone from Microsoft, having presented a C++ model, was asked (paraphrase): "So by this extraordinary effort, you have largely, but not fully, compensated for C++ having such a poorly designed <some form of semantics I no longer recall>?". There was a long pause, and then... "Yes."
[1] https://kframework.org/ [2] https://github.com/kframework/c-semantics/tree/master/semant...
Also, as I said on this item [2], Rust is no panacea. It's hard to argue this, since the overwhelming majority of programmers on HN are well and truly mentally oblivious due to poor education, but if your programming language does not have a semantics you cannot even begin to ask if your code is correct because the question itself doesn't make any sense. I am so exhausted at this state of affairs.
[1] https://cerberus.cl.cam.ac.uk/#%7B%220%22%3A%7B%221%22%3A%22...
AFAIK safe Rust is OK, but that's true that unsafe Rust has been pretty much “whatever LLVM will do with the IR that rustc generates”, but properly formalizing the semantic has been ongoing for years and has already started to give actionable results. The current state of things is still far from optimal, but at the same time you're always going to have an implementation of your programming language before you have a formal semantic, because nobody is ever going to use a language with a semantic but no implementation…
I appreciate what you're saying, however, hear me out. Suppose we had a language with a defined semantics and a useable implementation. We could use that language to implement, say Rust, and in so doing have a semantics for Rust, a semantics defined by its implementation. The point is, to be principled, we have to start somewhere. Make that language basic so that we are capable of providing a semantics. Now, granted, the "semantics" we generate for Rust in doing so will be necessarily pessimistic, i.e. overly determined. But then one could develop tooling to "prune" the implementation defined semantics somehow towards an idealized semantics. I don't think anyone has seriously pursued this avenue of thought.
Also, I must add, I appreciate your thoughtful elision from my quote. I need to stop getting worked up. But truly, software feels like it's perpetually in the dark ages. We have such incredible compute power thanks to the tireless effort of hardware engineers, and still we're programming with the equivalent of "stone knives and bear skins".
Whereas with Rust the point is to actually do something, including in this particular case Aria's Strict Provenance Experiment, which is basically "What if Rust insisted on full blown PNVI?". Obviously the answer is "Well that can't work" but like, how much. How much can't it work? Hence the experiment.
Hence why I hardly believe pointer provenance is going to be any different.
the basics of the rust typesystem were proven correct for a restricted rust subset in the rustbelt project.