[$] An instruction-level BPF memory model

There are few topics as arcane as memory models, so it was a pleasant surprisewhen the double-length session on the BPF memory model at theLinux Storage,Filesystem, Memory Management, and BPF Summit turned out to beunderstandable. Paul McKenney led the session, although he was clear that thework he was presenting was also due to Puranjay Mohan, who unfortunately couldnot 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 hasalready 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 ofMcKenney's talk.