Critique of the CCR

By: on May 17, 2006

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.



  1. projectshave says:

    Aside from research toys, no concurrent system meets your critique: “no defined semantics, its implementation is unverifiable, and CCR-based programs are not amenable to static analysis”. Erlang is dynamically-typed, which is much worse than the CCR (if static checking is your main concern).

    Is there something out there better than the CCR, which is not merely a research project?

  2. matthias says:

    My main point is that the CCR does not, and never will, live up to its promises. You are correct that there isn’t anything out there that is widely used and meets my criteria, yet. There is plenty of research going on that makes serious attempts at reasoning about concurrency based on solid mathematical foundations. Check out TyPiCal, or SLMC, for example. The CCR takes (next to) nothing from that, and adds nothing to it.

    The .Net type system does not help one iota in the static analysis of the concurrency aspects of programs. It is actually considerably easier to reason about concurrency in Erlang than in C# because a) concurrency is a key part of the Erlang language and hence its semantics, b) Erlang is quite a small language. Having said that, I did not mention Erlang in my post for a reason. Erlang wasn’t designed with static analysis in mind and as a consequence the language contains several features that make such analysis tricky, recent attempts such as Dialyzer notwithstanding.

  3. projectshave says:

    ‘Never’ is long time. There are a number of projects at Microsoft Research that do model checking on C# and MSIL. Check out Zing at MSR. There are several projects for Java, too. These tools will likely be available in 5+ yrs. I did model checking for cell networks 15 yrs ago. I think I know what I’m talking about.

    You say: “its implementation is unverifiable”. Is anything in your software stack verified or verifiable? I doubt it. Not your OS, compiler, hardware drivers, web software. I’ll bet you haven’t verified any of your own code, either. Yet you manage to write code without raging against other vendors. Why all the hate, dude?

    I don’t have anything to do with MS or CCR. You sound like a smart guy, but nearly everything in this post is wrong. If I can lead just one person out of the fog of ignorance, I’ll have done some good today. 😉 Cheers.

  4. matthias says:

    I am well aware of the model checking efforts at MSR, Zing included. It is important and promising work. The CCR does not take on board anything from it and adds nothing to it. It does not advance the knowledge in the area of reasoning about concurrent programs one bit.

    There is indeed next to nothing in common software stacks that is verified. The various research efforts you and I have been mentioning are starting to address that but they have a long way to go and their effectiveness is constrained by the target languages/platforms.

    Verifiability is a worthwhile goal to pursue, even if 100% verification of 100% of software is impossible. Thinking about it will, everything else being equal, lead to the better design and programs that are easier to understand and reason about by humans and computers alike. The research projects we listed take verification seriously. The CCR completely ignores it.

  5. Folks interested in static analysis on C# code should have a glance at the tool NDepend:

    NDepend analyses source code and .NET assemblies. It allows controlling the complexity, the internal dependencies and the quality of .NET code.

    NDepend provides a language (CQL Code Query Language) dedicated to query and constraint a codebase.

    It also comes from with advanced code visualization (Dependencies Matrix, Metric treemap, Box and Arrows graph…), more than 60 metrics, facilities to generate reports and to be integrated with mainstream build technologies and development tools.

    NDepend also allows to compare precisely different versions of your codebase.

Leave a Reply

Your email address will not be published.

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>