Thinking about state as a way of reasoning about synchronization seems like a good approach. But the problem is, the concerns I have about synchronization are often about execution: will it deadlock? Will there be lock contention? Reasoning purely about state leads me to write programs where the data is always correct but nothing can actually complete. Both state and execution are important, and they're kind of like matter and energy, seemingly unrelated concepts.
Einstein managed to show that energy and matter were actually two sides of the same coin: that a certain amount of matter was, in fact, equivalent to a certain amount of energy, if you chose the right units. Particle physicists took this and ran with it, coming up with the idea of symmetry breaking and explaining the circumstances it takes for the coin to flip. I need someone to do the same for multithreading. I want a theory of multithreading relativity that explains how given multithreading constructs act on execution and state, and what the symmetries are.
For instance, if you protect state with a mutex (in Java, a "synchronized()" block), then you can debug deadlocks by asking the system what threads own what locks. But you can also protect state by waiting for a notification event; this is a common way to implement a reader/writer pattern. The result is similar: the state is protected at the expense of some thread being blocked. But when a system deadlocks because every thread is waiting for a notification, there's no way to ask the system which thread was supposed to send it.
You'll never make a program hang by removing a synchronized(), but you might make a program hang by removing a notify(). On the other hand, you'll never make a program corrupt data by removing a notify(), but you might make a program corrupt data by removing a synchronized(). Is this a real symmetry?
Similarly, it's possible (but maybe not algorithmically possible) to look at code and see at least the hallmarks of deadlockability: for instance, code that takes nested locks out of order. Is there an equivalent analysis for code based on wait() and notify()?
In electrical engineering, it's possible to take any circuit based on voltage sources and impedances, and convert it (using the Thevenin and Norton theorems) to a different but equivalent circuit based on current sources and impedances, that will behave just the same to an outside observer. Doing this is often very useful for understanding how a circuit works. Is this possible for synchronization? Given some code implemented with certain synchronization tools, is it always possible to reimplement that code using different synchronization tools, such that the behavior will be the same? What do the rules of that conversion look like, and what will I learn about the underlying synchronization pattern by doing this? Exactly what "behavior" will prove to be invariant?