Critique of the CCR

By: on May 17, 2006

There was quite a lot of excitement about Microsoft’s [Concurrency and
Coordination Runtime
(CCR)](http://channel9.msdn.com/ShowPost.aspx?PostID=143582) when it
surfaced back in December. Recently several people asked me my opinion
about this technology.

According to the above link the 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](http://en.wikipedia.org/wiki/Process_calculi), which are are
a great formalism for defining the semantics of concurrent programs
and reason about them. However, the CCR introduces several novel
constructs, such as joins and choices with a dynamically determined
number of participants, that are not found in existing process
algebras.

I doubt that it is possible to construct a formal semantics that
captures all the CCR constructs and lets us reason about concurrency
in the same manner and with the same rigour as offered by most process
algebras. Consequently the CCR is built on shaky foundations and all
CCR-based programs are essentially meaningless – they mean *something*
but both tools and humans are going to have a hard time figuring out
what that is.

Even if the CCR had a well-defined semantics, it would be next to
impossible to verify that its implementation is faithful to it. The
CCR is implemented in C# and uses .Net classes. Hence to verify the
correctness of the CCR one has to model the semantics of C# and a
substantial chunk of the .Net libraries. That is hard. It is actually
possible to carry out a reasonably thorough verification of some C#
libraries, 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.

FacebookTwitterGoogle+

5 Comments

  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:
    http://www.NDepend.com

    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.

Post a comment

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=""> <strike> <strong>