3 ms·

The Cerberus C semantics [pdf]

54 points by matt_d 3y ago

mncharity 3y ago
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/ https://kframework.org/ [2] https://github.com/kframework/c-semantics/tree/master/semantics/c https://github.com/kframework/c-semantics/tree/master/semant...
JonChesterfield 3y ago
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.
- carbotaniuman 3y ago
  With provenance, it's important to remember that this is less about adopting a new model that allows miscompilations, and more about addressing current, already existing miscompilations. 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.
  - JonChesterfield 3y ago
    Mem2reg works fine on variables whose addresses have not escaped. Compilers do extensive alias analysis anyway, because even given an oracle that says double* does not alias long*, you still want to work out which double*s can alias. 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.
    - sanxiyn 3y ago
      Without pointer provenance, all addresses escape. Just cast integer to pointer. I agree strict aliasing is a relic of the past that should be abolished ASAP, but that's quite different from pointer provenance.
    - jcranmer 3y ago
      > Mem2reg works fine on variables whose addresses have not escaped. 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).
- samth 3y ago
deltasepsilon 3y ago
I think the importance of this work is best illustrated by a simple example [1]. If that link doesn't work, go to https://cerberus.cl.cam.ac.uk/ https://cerberus.cl.cam.ac.uk/ select File->Popl 2019 and pick the second example (basic_local_yx) and run the sim (hit forward). The experimental data is interesting, specifically that from CompCert. This project allows work towards a certified optimizing compiler, assuming you can decide on a semantics. 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%220%22%2C%222%22%3A%220%22%2C%223%22%3A%221%22%2C%22t%22%3A%220%22%2C%22p%22%3A%221%22%2C%22blockedPopoutsThrowError%22%3A%220%22%2C%22closePopoutsOnUnload%22%3A%220%22%2C%22showPopoutIcon%22%3A%221%22%2C%22showMaximiseIcon%22%3A%220%22%2C%22showCloseIcon%22%3A%220%22%2C%22responsiveMode%22%3A%22onload%22%2C%22tabOverlapAllowance%22%3A0%2C%22reorderOnTabMenuClick%22%3A%220%22%2C%22tabControlOffset%22%3A10%7D%2C%224%22%3A%7B%225%22%3A5%2C%226%22%3A10%2C%227%22%3A150%2C%228%22%3A20%2C%229%22%3A300%2C%22u%22%3A15%2C%22a%22%3A200%7D%2C%22b%22%3A%7B%22c%22%3A%22Close%22%2C%22d%22%3A%22Maximise%22%2C%22e%22%3A%22Minimise%22%2C%22f%22%3A%229%22%2C%22popin%22%3A%22pop%20in%22%2C%22tabDropdown%22%3A%22additional%20tabs%22%7D%2C%22g%22%3A%5B%7B%22l%22%3A%222%22%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22g%22%3A%5B%7B%22l%22%3A%223%22%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22k%22%3A33.333333333333336%2C%22g%22%3A%5B%7B%22l%22%3A%224%22%2C%22m%22%3A50%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22s%22%3A0%2C%22g%22%3A%5B%7B%22l%22%3A%225%22%2C%22h%22%3A%22source%22%2C%22o%22%3A%22provenance_basic_global_yx.c%22%2C%22n%22%3A%221%22%2C%22t%22%3A%220%22%7D%5D%7D%2C%7B%22l%22%3A%224%22%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22m%22%3A50%2C%22s%22%3A0%2C%22g%22%3A%5B%7B%22l%22%3A%225%22%2C%22h%22%3A%22tab%22%2C%22i%22%3A%7B%22tab%22%3A%22Console%22%2C%22h%22%3A%22tab%22%7D%2C%22o%22%3A%22Console%22%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%7D%5D%7D%5D%7D%2C%7B%22l%22%3A%224%22%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22k%22%3A33.333333333333336%2C%22s%22%3A0%2C%22g%22%3A%5B%7B%22l%22%3A%225%22%2C%22h%22%3A%22tab%22%2C%22i%22%3A%7B%22tab%22%3A%22Memory%22%2C%22h%22%3A%22tab%22%7D%2C%22o%22%3A%22Memory%22%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%7D%5D%7D%2C%7B%22l%22%3A%224%22%2C%22k%22%3A33.33333333333333%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22s%22%3A0%2C%22g%22%3A%5B%7B%22l%22%3A%225%22%2C%22h%22%3A%22tab%22%2C%22n%22%3A%221%22%2C%22o%22%3A%22Experimental%20Data%22%2C%22i%22%3A%7B%22tab%22%3A%22Experimental%22%2C%22args%22%3A%5B%5D%2C%22h%22%3A%22tab%22%7D%2C%22t%22%3A%220%22%7D%5D%7D%5D%7D%5D%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22q%22%3A%5B%5D%2C%22maximisedItemId%22%3A%7B%7D%2C%22title%22%3A%22provenance_basic_global_yx.c%22%2C%22source%22%3A%22%23include%20%3Cstdio.h%3E%5Cn%23include%20%3Cstring.h%3E%20%5Cnint%20y%3D2%2C%20x%3D1%3B%5Cnint%20main()%20%7B%5Cn%20%20int%20*p%20%3D%20%26x%20%2B%201%3B%5Cn%20%20int%20*q%20%3D%20%26y%3B%5Cn%20%20printf(%5C%22Addresses%3A%20p%3D%25p%20q%3D%25p%5C%5Cn%5C%22%2C(void*)p%2C(void*)q)%3B%5Cn%20%20if%20(memcmp(%26p%2C%20%26q%2C%20sizeof(p))%20%3D%3D%200)%20%7B%5Cn%20%20%20%20*p%20%3D%2011%3B%20%20%2F%2F%20does%20this%20have%20undefined%20behaviour%3F%5Cn%20%20%20%20printf(%5C%22x%3D%25d%20y%3D%25d%20*p%3D%25d%20*q%3D%25d%5C%5Cn%5C%22%2Cx%2Cy%2C*p%2C*q)%3B%5Cn%20%20%7D%5Cn%7D%5Cn%22%7D https://cerberus.cl.cam.ac.uk/#%7B%220%22%3A%7B%221%22%3A%22... [2] https://news.ycombinator.com/item?id=33096395 https://news.ycombinator.com/item?id=33096395

54 points by matt_d 3y ago

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/ https://kframework.org/ [2] https://github.com/kframework/c-semantics/tree/master/semantics/c https://github.com/kframework/c-semantics/tree/master/semant...

JonChesterfield 3y ago

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.

carbotaniuman 3y ago
With provenance, it's important to remember that this is less about adopting a new model that allows miscompilations, and more about addressing current, already existing miscompilations. 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.
- JonChesterfield 3y ago
  Mem2reg works fine on variables whose addresses have not escaped. Compilers do extensive alias analysis anyway, because even given an oracle that says double* does not alias long*, you still want to work out which double*s can alias. 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.
  - sanxiyn 3y ago
    Without pointer provenance, all addresses escape. Just cast integer to pointer. I agree strict aliasing is a relic of the past that should be abolished ASAP, but that's quite different from pointer provenance.
  - jcranmer 3y ago
    > Mem2reg works fine on variables whose addresses have not escaped. 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).
samth 3y ago

deltasepsilon 3y ago

I think the importance of this work is best illustrated by a simple example [1]. If that link doesn't work, go to https://cerberus.cl.cam.ac.uk/ https://cerberus.cl.cam.ac.uk/ select File->Popl 2019 and pick the second example (basic_local_yx) and run the sim (hit forward). The experimental data is interesting, specifically that from CompCert. This project allows work towards a certified optimizing compiler, assuming you can decide on a semantics. 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%220%22%2C%222%22%3A%220%22%2C%223%22%3A%221%22%2C%22t%22%3A%220%22%2C%22p%22%3A%221%22%2C%22blockedPopoutsThrowError%22%3A%220%22%2C%22closePopoutsOnUnload%22%3A%220%22%2C%22showPopoutIcon%22%3A%221%22%2C%22showMaximiseIcon%22%3A%220%22%2C%22showCloseIcon%22%3A%220%22%2C%22responsiveMode%22%3A%22onload%22%2C%22tabOverlapAllowance%22%3A0%2C%22reorderOnTabMenuClick%22%3A%220%22%2C%22tabControlOffset%22%3A10%7D%2C%224%22%3A%7B%225%22%3A5%2C%226%22%3A10%2C%227%22%3A150%2C%228%22%3A20%2C%229%22%3A300%2C%22u%22%3A15%2C%22a%22%3A200%7D%2C%22b%22%3A%7B%22c%22%3A%22Close%22%2C%22d%22%3A%22Maximise%22%2C%22e%22%3A%22Minimise%22%2C%22f%22%3A%229%22%2C%22popin%22%3A%22pop%20in%22%2C%22tabDropdown%22%3A%22additional%20tabs%22%7D%2C%22g%22%3A%5B%7B%22l%22%3A%222%22%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22g%22%3A%5B%7B%22l%22%3A%223%22%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22k%22%3A33.333333333333336%2C%22g%22%3A%5B%7B%22l%22%3A%224%22%2C%22m%22%3A50%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22s%22%3A0%2C%22g%22%3A%5B%7B%22l%22%3A%225%22%2C%22h%22%3A%22source%22%2C%22o%22%3A%22provenance_basic_global_yx.c%22%2C%22n%22%3A%221%22%2C%22t%22%3A%220%22%7D%5D%7D%2C%7B%22l%22%3A%224%22%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22m%22%3A50%2C%22s%22%3A0%2C%22g%22%3A%5B%7B%22l%22%3A%225%22%2C%22h%22%3A%22tab%22%2C%22i%22%3A%7B%22tab%22%3A%22Console%22%2C%22h%22%3A%22tab%22%7D%2C%22o%22%3A%22Console%22%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%7D%5D%7D%5D%7D%2C%7B%22l%22%3A%224%22%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22k%22%3A33.333333333333336%2C%22s%22%3A0%2C%22g%22%3A%5B%7B%22l%22%3A%225%22%2C%22h%22%3A%22tab%22%2C%22i%22%3A%7B%22tab%22%3A%22Memory%22%2C%22h%22%3A%22tab%22%7D%2C%22o%22%3A%22Memory%22%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%7D%5D%7D%2C%7B%22l%22%3A%224%22%2C%22k%22%3A33.33333333333333%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22s%22%3A0%2C%22g%22%3A%5B%7B%22l%22%3A%225%22%2C%22h%22%3A%22tab%22%2C%22n%22%3A%221%22%2C%22o%22%3A%22Experimental%20Data%22%2C%22i%22%3A%7B%22tab%22%3A%22Experimental%22%2C%22args%22%3A%5B%5D%2C%22h%22%3A%22tab%22%7D%2C%22t%22%3A%220%22%7D%5D%7D%5D%7D%5D%2C%22n%22%3A%220%22%2C%22t%22%3A%220%22%2C%22o%22%3A%22%22%2C%22q%22%3A%5B%5D%2C%22maximisedItemId%22%3A%7B%7D%2C%22title%22%3A%22provenance_basic_global_yx.c%22%2C%22source%22%3A%22%23include%20%3Cstdio.h%3E%5Cn%23include%20%3Cstring.h%3E%20%5Cnint%20y%3D2%2C%20x%3D1%3B%5Cnint%20main()%20%7B%5Cn%20%20int%20*p%20%3D%20%26x%20%2B%201%3B%5Cn%20%20int%20*q%20%3D%20%26y%3B%5Cn%20%20printf(%5C%22Addresses%3A%20p%3D%25p%20q%3D%25p%5C%5Cn%5C%22%2C(void*)p%2C(void*)q)%3B%5Cn%20%20if%20(memcmp(%26p%2C%20%26q%2C%20sizeof(p))%20%3D%3D%200)%20%7B%5Cn%20%20%20%20*p%20%3D%2011%3B%20%20%2F%2F%20does%20this%20have%20undefined%20behaviour%3F%5Cn%20%20%20%20printf(%5C%22x%3D%25d%20y%3D%25d%20*p%3D%25d%20*q%3D%25d%5C%5Cn%5C%22%2Cx%2Cy%2C*p%2C*q)%3B%5Cn%20%20%7D%5Cn%7D%5Cn%22%7D https://cerberus.cl.cam.ac.uk/#%7B%220%22%3A%7B%221%22%3A%22... [2] https://news.ycombinator.com/item?id=33096395 https://news.ycombinator.com/item?id=33096395