Peter Sewell's invited talk.

The golden age -- 1945 -- Maurice and friends building the ``first''
computer, with mercury line memory and so forth.

1960 -- start introducing nondeterminacy.

Nondeterminism of the first kind -- interleaving.
Nondeterminism of the second kind -- relaxed memory and weak consistency.

Q: Isn't two a generalisation of one?
A: It depends on the level.  At a u-arch level, it works, but at a programmer's
   level that might be too complicated.

Nondeterminism of the third kind -- loose specifications
Nondeterminism of the fourth kind -- nobody knows what's supposed to happen.

Q: Should we be frightened?
A: Yes.

Not a new problem?  Relaxed memory systems since 1972 (IBM
S370/158MP).  Most previous specifications seriously flawed.

That includes previous models published by the speaker.

Examples with a small number of threads.

Q: It's incredible it works, really.
A: Yes.
Q: Why does it work?
A: Partly that there's not really that much concurrency going on.
   Some of the problems are in odd corner cases; unclear how important
   they are in practice.  Especially, most of the bad cases only happen
   for racey code.  One particular problem is implementing higher-level
   models on top of existing hardware.

<lots of examples which I'm not going to transcribe, unless they get
interesting>

Observation: empirically checking hadware behaviour is unusual.

Their test case can show up the x86 store buffer very easily e.g. it
breaks Dekker's algorithm one time in 1000 (on some hardware).

Also need to think about compiler optimisations.

Q: Can you use this to do anything cool?
A: Yes, see all the lock-free algorithm work.

Eval: compare the model to the hardware.  Looks like it's pretty good.
Can see changes in microarchitecture.

Example showing that C++11 memory model allows reads from thin air.

Q: Is that a security problem?
A: Possibly; maybe low probability, but that's not all that reassuring.

Spec tries to rule out thin air reads, but fails to do so.  No real
idea how to get rid of them.

JMM: broken, in that it's much more cautious than any existing JVM.

Pretend that people program to the specification, but the spec isn't
there.  Develop software by testing.

Possible fix: emulators which actually explore the specification
space.

Q: This is a problem if CS is a branch of maths; not if it's a branch
   of engineering.
A: Yes, but bridges behave continuously, whereas software is discreet.
   Small changes to software are disastrous; bridges have safety
   margins.
Q: We need software to be error tolerant.
A: It tolerates some errors.
Q: Maybe specs should be partly probabilistic?
Q: Maybe.

Q: So what should a software vendor do, testing on POWER6, when POWER7
   might be different?
A: It would be nice if we had a simulator.
Q: Not quite true.  Steve Frand, Cormack Franigan, Adverserial memory model.
   Tries to break Java programs.  Breaks lots of things.
A: Yes, has been done for some memory models.
Q: But we still can't specify things?
A: Yes.
Q: And finding the ``worst'' case is hard, so they tend to find unlikely cases.

Q: Do you have any tips for finding odd corner cases?
A: Have a tool for making examples from ``non-SC cycles'' <?>
   Also have a tool which pretty much brute forces the rest of the
   stuff.