On 5 Feb 2025, at 19:03, Marc Nieper-Wißkirchen <marc.nie...@gmail.com> wrote:
>> I don’t see how this is the case. The implementation would somehow need to >> both inline the helper-proc (in order to do the re-ordering optimization you >> were worried about when you introduced the reference-barrier procedure) but >> also discard the reference-barriering nature of the mention of ‘key’. This >> seems very unlikely. > > It should be possible to prove the correctness of a program formally. > For that, "very unlikely" is not enough. It’s up to the compiler to do this correctly (or not), of course. > That said, all semantics suggested so far have another problem, which > I haven't mentioned yet: A reference barrier on the key in the > unbroken case is useless. The GC can break an ephemeron if, under the > assumption that it is broken, the key will not be kept alive. > > I am going to post a "real life" example soon (I am currently ill, and > my brain is not fully working) so that we have some concrete code to > test potential syntax against. Okay, please do. I’m a bit confused by this. Get well soon! Daphne
