[HN Gopher] The Cerberus C semantics [pdf]
       ___________________________________________________________________
        
       The Cerberus C semantics [pdf]
        
       Author : matt_d
       Score  : 6 points
       Date   : 2023-05-12 19:07 UTC (3 hours ago)
        
 (HTM) web link (www.cl.cam.ac.uk)
 (TXT) w3m dump (www.cl.cam.ac.uk)
        
       | mncharity wrote:
       | Here's the earlier K framework[1]'s kcc[2] C rewrite semantics.
       | 
       | 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...
        
       | JonChesterfield wrote:
       | I've read the abstract, noted the enthusiasm for pointer
       | provenance and the doctoral advisor, and jumped to my usual
       | conclusion on this stuff.
       | 
       | 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.
        
       ___________________________________________________________________
       (page generated 2023-05-12 23:02 UTC)