Reasoning about concurrency has always been extremely difficult, and the need for workable theories is set to rise with the increasing appearance of multi-core processors.

The difficulty has never been one of describing what concurrent processes might do in a theoretically adequate way. Rather, the core problem is to find tractable ways of reasoning about concurrent programs. In his classic paper 1972 "Towards a Theory of Parallel Programming", Hoare spoke of the problem of controlling, or understanding, the "fantastic number of of combinations involved in arbitrary interleaving". The problem remains, and has only got worse with weak memory models, which give rise to even more combinations. (Note that the difficulty is not to describe those interleavings, but rather is to understand or even avoid them in reasoning.)

There have been significant advances on reasoning about (shared memory) concurrent programs, including the Owicki-Gries theory, temporal logic (Pnueli) , and rely(or assume)-guarantee method (Jones, Chandy, Misra). More recently, concurrent separation logic (O'Hearn, Brookes) and Boogie (Leino et al) have emerged as methods that provide for modular reasoning about concurrent processes in the presence of heap-allocated data structures.

However, what we see is a mishmash of specific techniques, and very specific advances whose limitations and whose fundamental assumptions are not well understood. For example, Boogie and concurrent separation logic both speak of "ownership", but it is not easy to connect them (their modes of expression being somewhat distant). A proper theory would lay bare the primitive assumptions that give rise to modular reasoning, giving Boogie and separation logic as instances and, perhaps, other, improved methods. Such a theory does not seem near at hand.

Furthermore, all of the best known proof methods can show stress under the simplest example programs. (By "stress" is meant that the specifications and proofs become complex out of proportion with the problem, and detached from reasoning intuition.)

To find smooth proof methods with clear and general and simple foundations is a challlenge for theorists. This challenge should also be matched with the test of proving actual programs. Even now, we would benefit from a clear understanding of where various methods do not work well.

The problems with interleaving show up most vividly in model checking and program analysis. Starting from an abstract model, one can often, in principle, enumerate a finite number of the possible interleavings. But that finite number can be too large to be enumerable in reasonable time, in practice.

Most of the approaches mentioned above have been applied in tools only to safety properties. Liveness raises a host of other issues. It has sometimes been supposed that liveness, by its very nature, requires global knowledge, in a way that is an impediment to scalable reasoning. But some researchers are actively pursuing local reasoning about liveness properties. Automatic verification techniques for liveness properties of programs are in their infancy (e.g., Terminator; Cook, Podelski, Rybalchenko), but are needed because they approximate responsiveness properties of systems.

There has been important work on identifying variations on the concept of "atomicity", as a way to simplify reasoning about the use of concurrent objects. Early work by Lamport, Herlihy and others focussed on the semantic level, in the identification of such concepts as serializability and linearizability. Proof systems for establishing such properties are lacking. There is much that remains to be done, in the foundations and in applications and in tools that check and exploit notions of atomicity.

Finally, in an almost disjoint line of development, there have appeared numerous models of concurrency expressed as calculi or with algebra. Examples are CSP, CCS, pi-calculus and Petri nets. These models were purposely described in a way that is removed from computers, and programs. That was a good choice, but it is somewhat of an embarrassment that they have not been more thoroughly connected to the verification methods, such as those mentioned above, for the code level.

Ideally, one would like to have a refinement method that started from an abstract description of a system (say, using a process calculus) and ending up with verified real code. Again ideally, such a method should combat the "fantastic combinations" problem with interleaving. And it should not rule out low-level concurrent programming based on, say, fine-grained locking or non-blocking primitives. There have been nods in this direction (e.g., by Abrial), but the area is wide open.

To sum up, although there has been important progress over th eyears, basic problems in concurrency remain, particularly on obtaining tractable reasoning and specification methods, and just as particularly on the revealing of the foundation of these methods.

With all this being said, the opposing position of Lamport - that modularity is a way to make proofs harder - should be kept in mind.