Attempt at expressing location of resources and weak memory accesses

[gebner]

• loc_id is a logical location from which you can observe memory, on l p says that p is true at location l, locations can be e.g.:
  • a thread (i.e., on thrid (x |-> y) means that when thread number thrid reads the variable x it will reliably get y)
  • global memory (i.e., you will get y after doing a memory fence)
  • memory associated with an atomic variable (i.e., you will get y but only if you do an atomic read on the atomic variable first)
  • global memory on a GPU
• every thread is associated with a process (which is also a location), there can be multiple processes
  • every block in a GPU kernel is logically a process
  • we can axiomatize when it is safe to move resources between blocks/devices/processes
• slprops are stratified according to how easy it is to move them between locations:
  • placeless p means you can unconditionally move them anywhere, e.g., pure, inv, on, ghost references, etc.
  • is_sync p means you can unconditionally move them, but only to threads of the same process
  • is_send p means you can move them to threads of the same process, but only after a memory fence operation
• invariants require placeless slprops, fork requires is_send, mutex requires is_send

To check out the interface, a good place to look is the diff for Pulse.Lib.Core.fsti and Pulse.Lib.SendSync.fsti.

The formalization is very, uhhm, "flexifoundational". It basically sets loc_id = unit, and then everything could be proven. This is not even an empty guarantee, it shows that you can't prove false from these axioms.

Pain points:

• Basically every time you want to use an invariant, you need to write inv i (on l p) or some variation to make the slprop placeless. I'm playing with having a custom invariant module that automates this to some degree (i.e. better_inv i p would require is_sync p and in return you get is_sync (better_inv i p), which would be enough for mutexes etc.)
• Trades, sigh. We already have two versions of trades with different restrictions on the closure: trade and shift (which requires the closure to be duplicable). This approach would add a lot of other useful restrictions to the mix: sending a trade across threads requires an is_sync closure, sending a trade across devices requires a placeless closure, pulling a trade out of a later requires a timeless closure, etc. Obviously, some might want a duplicable+timeless+is_sync trade too... You can work around this a bit with on, but I foresee a plethora of trade variants.
• You need to write a lot of placeless/is_send/is_sync instances; they're usually trivial though.

Fun points:

• Using type classes for placeless/is_send/is_sync seems to work out nicely; or at least nicer than the SMT pattern setup for timeless.

There are still lots of admits everywhere, but this PR should be enough to give a general idea of how the approach works.