Port late master additions to weak_mem

Since the paper has been published, I made a few small additions to master as questions came up in discussions or as the standard library changed:

• https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/505d86a5fbb85abd4e5fada1853136ac690a60bf: &mut T <-> &mut Cell<T>
• https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/ff244cf1b7deabfd9bc1e4eae0bc48db6aedbe77: Box<T> <-> Box<Cell<T>>
• https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/7da18513b7d41b50cc58cd08136115d59d42828e: impl<T> Send for JoinHandle<T>
• e6a4bef4: Faking a &&mut.

@haidang @jjourdan which of these still need porting to weak_mem?

JH already ported the Cell's equivalence. That Join is thread independent is new and needs ported. I'll check it.

Ported :).

marked the checklist item https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/7da18513b7d41b50cc58cd08136115d59d42828e: impl<T> Send for JoinHandle<T> as completed

marked the checklist item https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/ff244cf1b7deabfd9bc1e4eae0bc48db6aedbe77: Box<T> <-> Box<Cell<T>> as completed

marked the checklist item https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/505d86a5fbb85abd4e5fada1853136ac690a60bf: &mut T <-> &mut Cell<T> as completed

Awesome!

I will reopen this when I do more stuff in master.

closed

We could also merge weak_mem at some point. If your additions have nothing to do with concurrency, then it is very likely that you won't feel the difference.

TBH I am not too excited at the prospect of waiting 40min whenever I have to compile that thing...^^

Yeah ok. That's something we should investigate, btw. This is not normal that the wp_* tactics are taking so much time here.

I added another one: Faking a shared mutable ref. (I was not able to derive that from the shared box, unfortunately).

reopened

changed the description

Ported just by copy&pasting :). What do you mean with the FIXME in the proof?

marked the checklist item e6a4bef4: Faking a &&mut. as completed

Thanks!

What do you mean with the FIXME in the proof?

I should be able to replace (uniq_bor β ty) by (&uniq{β} ty) but somehow that does not work.

closed