What intermediate representations can be used to reason about concurrency?

Question

I am trying to better understand what would be required for a compiler to be able to make intelligent choices regarding concurrency on behalf of the programmer. I realize that there are many difficult aspects of this problem for instance:

• Ensuring that there are no race conditions

• Ensuring that the code to be run concurrently won't have side effects that impact the semantic meaning of the code

• Deciding whether the overhead from spinning up threads is worthwhile given the degree of parallelism available in the code

My understanding is that the two major intermediate representations used in modern compilers are static single assignment for procedural and object oriented languages and continuations passing style for functional languages. Reasoning about any of the problems listed above seems difficult using these intermediate forms. Even languages that should in theory have the best chance at automatic parallelization (pure functional languages like Haskell with a guarantee of no side effects) have made limited progress on this front.

So my question is really what intermediate representations have been used to try and tackle this problem? Are there other representations that have been used in academic research that I am not aware of that are better suited to this task? Is this problem one that fundamentally has to be resolved by the compiler front end by manipulating the abstract syntax tree before compilation reaches an intermediate representation?

Answer 1

One would assume that modeling concurrency explicitly in the intermediate representation (IR) was a necessary requirement. So one answer would be, "any IR used for sequential programs with the addition of some concurrency operations", e.g., "fork and join", "parallel x y". Adding these makes it possible to reason about some kinds of concurrency, but not necessarily easily. Nor is it obvious how to ensure certain properties (data-race freeness) without going all the way to a fully functional representation (which makes it hard to model parallelism usefully).

Arguably Colored Petri Nets (CPNs) are a good choice for representing programs with concurrency. (Tokens in CPNs are "colored" [have a type] and can carry values; "transitions" into states can perform arbitrary arithmetic on incoming tokens to produce a possibly differently colored token with computed value in the "place"). If you think about places as being computed results and transitions as modelling operators (including a special one to access memory), this gives you what amounts to a data flow graph with which to model programs. You can easily use this to give a formal interpretation to classic compiler representations such as triples [operator,input1,input2,output].

There are lots of tools to analyze such CPN graphs, including computing properties such as deadlock-freeness, boundedness of token counts in places, etc. Heirarchical CPNs let you model functions and procedures and the notion of "calls".

What these representations do not clearly do, is make it easy to reason about where one could parallelize an application. Trivially, two subcomputations can be parallel if they side-effect no shared operands ( which is why some folks love functional programs/representations). If your program representation models a shared memory, you can model it as monolith and get the usual set of troubles about reasoning about interactions on the shared memory, including aliased addressing, etc. One way to avoid this is to treat memory as isolated chunks with the larger program state being some (tree-like) assemblage of these; you can arguably pass these chunks around in your intermediate representation. There is no interaction between two parallel computations if they don't share chunks (e.g., memory subtrees).