There was quite a lot of excitement about Microsoft’s Concurrency and
Coordination Runtime (CCR) is super cool stuff and represents a really innovative approach to making managed threaded programming more readily understandable and predictable.
Does the CCR live up to this promise? I don’t think so.
The CCR borrows many ideas from process algebras, which are are great formalism for defining the semantics of concurrent programs reason about them. However, the CCR introduces several novel, such as joins and choices with a dynamically determined of participants, that are not found in existing process.
I doubt that it is possible to construct a formal semantics that all the CCR constructs and lets us reason about concurrency the same manner and with the same rigour as offered by most process. Consequently the CCR is built on shaky foundations and all-based programs are essentially – they mean something both tools and humans are going to have a hard time out that is.
Even if the CCR had a well-defined semantics, it would be next to to verify that its implementation is faithful to it. The is implemented in C# and uses .Net classes. Hence to verify the of the CCR one has to model the semantics of C# and a chunk of the .Net libraries. That is hard. It is actually to carry out a reasonably thorough verification of some C#, but the success of such a venture crucially depends on the libraries being small, having been written with the semantics in hand and with verification in mind. that is clearly not the case for the CCR.
The difficulties don’t stop there. The CCR is a library rather than a language and its use is tightly interweaved with the rest of a program. Therefore, in order to reason about the concurrency aspects of CCR-based programs one has to reason about the entire program. Performing any kind of static analysis on C#-based programs is extremely difficult. The language is unwieldy and does not encourage the style of programming that makes sophisticated analysis feasible.
From my own experience I know that static analysis of programs with a concurrency model that is loosely based on process algebras is essential if one wants to have any hope of writing correct code. Even if there are no tools one should at least be able to reason about the program mentally. That is impossible with the CCR.
To summarise: The CCR has no defined semantics, its implementation is unverifiable, and CCR-based programs are not amenable to static analysis.