[$] An instruction-level BPF memory model

There are few topics as arcane as memory models, so it was a pleasant surprise
when the double-length session on the BPF memory model at the
Linux Storage,
Filesystem, Memory Management, and BPF Summit turned out to be
understandable. Paul McKenney led the session, although he was clear that the
work he was presenting was also due to Puranjay Mohan, who unfortunately could
not attend the summit.
BPF does not actually have a formalized memory model yet;
instead it has relied on a history of talks like this one and a general informal understanding.
Unfortunately, ignoring memory models does not make them go away, and this has
already caused at least one BPF-related bug on weakly-ordered architectures.
Figuring out what a formal memory model for BPF should define was the focus of
McKenney's talk.