4 ms·

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://cerberu

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

tialaramex 3y ago
As I understand it, the larger purpose of this work is as part of efforts to persuade WG14 to pick actual provenance semantics, presumably a PNVI-ae variant. As just a TR, the same as with the original thesis, it doesn't do anything. 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.
- pjmlp 3y ago
  I doubt they would get persuaded, as much as they have been into anything related to improving C's safety.
  - jcranmer 3y ago
    From what I understand, the C committee is very interested in adopting pointer provenance semantics, but they also tend to operate at the speed of molasses and this is of course a research-hard problem.
    - pjmlp 3y ago
      Well, in 50 years they have hardly bothered to add any kind of fat pointer as suggested by Dennis Ritchie, Walter Bright and others, struct based vocabulary types for string and arrays, annotations like SAL. Hence why I hardly believe pointer provenance is going to be any different.
      - tialaramex 3y ago
        Last I looked WG14 intended to knock together a TS for provenance in the C23 timeframe (so, this year). Of course a TS might go nowhere, vendors could ignore it, it might be a dead end, but I don't believe WG14 produced a TS of sane array types, or fat pointers.
nullifidian 3y ago

tialaramex 3y ago

As I understand it, the larger purpose of this work is as part of efforts to persuade WG14 to pick actual provenance semantics, presumably a PNVI-ae variant. As just a TR, the same as with the original thesis, it doesn't do anything. 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.

pjmlp 3y ago
I doubt they would get persuaded, as much as they have been into anything related to improving C's safety.
- jcranmer 3y ago
  From what I understand, the C committee is very interested in adopting pointer provenance semantics, but they also tend to operate at the speed of molasses and this is of course a research-hard problem.
  - pjmlp 3y ago
    Well, in 50 years they have hardly bothered to add any kind of fat pointer as suggested by Dennis Ritchie, Walter Bright and others, struct based vocabulary types for string and arrays, annotations like SAL. Hence why I hardly believe pointer provenance is going to be any different.
    - tialaramex 3y ago
      Last I looked WG14 intended to knock together a TS for provenance in the C23 timeframe (so, this year). Of course a TS might go nowhere, vendors could ignore it, it might be a dead end, but I don't believe WG14 produced a TS of sane array types, or fat pointers.

nullifidian 3y ago