Stefan-Marr.de

This post is a follow up on my first report on the TiC’10 summer school. It covers mainly the talks about X10 and formal aspects of concurrency.

Vijay Saraswat gave an overview about X10, Matthew Parkinson introduced separation logic and deny-guarantee reasoning, and Ganesan Ramalingam reported on Analysis and Verification of Concurrent Programs.

Vijay Saraswat: The X10 Language: Design and Implementation

The talk started with a brief description of the usual application scenarios IBM tries to address. They are looking for a language, which allows to program homogenous multi- or many-core systems as well as potentially heterogeneous cluster or HPC systems. The main goal is to design an expressive, productive and efficient programming model for application developers. The means to that end are a type system, static analysis, a comfortable debugger, and optimized standard libraries.

X10 is part of the PGAS family, but compared to UPC or Co-Array Fortran, X10 is an asynchronous PGAS (APGAS) language, which means that accesses over location boundaries are handled asynchronous by the runtime.

Some of the language properties, which were discussed, are briefly summarized below. As an APGAS language writes are only local. For remote writes you need to use a place-shift operation. The semantics of it is synchronous, but usually the implementation is asynchronous via messages. In that regard, Vijay also mentioned a tail-call like optimization to minimize the number of messages, which need to be exchanged. The atomic semantics is, well, rough. They use a per-place lock for atomics, but atomic operations on primitive values like integers are mapped to atomic operations provided by the underlying system, thus it is inherently ‘broken’, i.e., it is up to the programmer to ensure that different atomic blocks do not interfere with each other.

The implementation uses the notion of workers, which represent threads of the underlying system. There are 1 to n workers per place and activities are executed by workers. At the moment they use a model similar to Java’s fork/join, where the number of workers can grow over time. A problematic point is the implementation of the ‘when(C)’ construct, which currently requires to spawn new threads since the thread executing the activity which uses the ‘when’ construct will actually block on it. They will later change to a Cilk-like work-stealing system, which will allow to use a constant number of threads.

The place structure is static from the beginning, and currently a flat structure. In the future, this might be changed. Currently, they think about a hierarchical model as a better fit for GPGPUs. The plan is to explore two-level hierarchical places.

The design with workers and activates allows the compiler to coarsen up concurrency to remove the overhead of very fine-grained activities.

Another more flexible language construct they introduced recently is labeled finishes to allow the implementation of server-like programs where you do not want a pure hierarchical relation between asyncs and finishs but need more flexibility. Thus, an async can indicate on which finish it wants to announce its completion.

Matthew Parkinson: Deny-Guarantee Reasoning

The largest portion of his lectures was about the foundation for his own work. Thus, he was introducing separation logic. The goal is to have logic foundation to reason about programs, which can use pointer data structures, i.e., a heap like in usual object oriented programs. As far as I understood, this logic provides the means to establish statements about the behavior of programs. More precisely, it is possible to prove certain semantic assertions about their stacks and heaps.

One thing, which can be done, is to check whether the sets of memory locations modified by a program a disjoint, and thus, whether the program is race-free.

Rely-guarantee reasoning is a logic framework to reason about composed concurrent programs and is independent of separation logic. However, this logic is not able to capture the typical fork/join parallelism of many programs.

Deny-Guarantee reasoning is a reformulation of both, which explicitly supports dynamic parallelism, and thus, enables a formal reasoning about these kind of concurrent programs.

Well, I think I understand what it is useful for. The next thing I would need is a good textbook introducing all the basics very patiently. Might be necessary to prove that my barrier/phaser algorithm is actually correct :-/

Ganesan Ramalingam: Analysis & Verification of Concurrent Programs

Another Greek talk *sigh*. Anyway, lets see what it is good for: The goal of the work Mr. Ramalingam presented is to verify programs for some correctness criterion and for instance find concurrency bugs. To this end, they are using technique called concurrent shape analysis, which allows static verification in the presence of a dynamic heap and a statically unbounded number of threads by using abstract interpretation.

Before he goes into the details, he presents a typical stack example, and how it breaks if concurrency comes into play. To be able to reason about the correctness of the implementation a sequential specification of the stack is necessary. In a concurrent setting, this implies that the operations have to be linearizable in some form. The definition for that is: an interleaved execution is said to be linearizable iff it is equivalent to a legal sequential execution that preserves the order of non-overlapping operations.

Well, and then he goes on to explain the technique in detail.

In the second lecture, he starts with talking about serializability, similar to what is done in databases. His goal is to use the techniques presented earlier, to synthesize correct locking-schemes for originally sequential data-structures, while avoiding the trivial solution but providing an efficient scheme. The simplified idea is to compute a sequential proof, introduce the locks, and then afterwards eliminate redundant locks to achieve performance.

The third and last part of the summer school started with Ondrej Lhotak talking about pointer analysis. David Bacon presented a basic introduction to garbage collection and detailed description of the real-time Metronome GC. The last lecturer for this summer school was Patrick Cousot, who gave a very basic and thus understandable introduction to abstract interpretation.

Pointer Analysis

Ondrej’s lectures were focused on pointer analysis for C and Java-like languages. He introduced it as a static analysis for several problems like for instance optimization, call-graph construction, dependency analysis and optimization, cast elimination, side effect, and escape analysis. The major problem seems to be that it is a very broad subject with many different applications, and thus, many different techniques to do the analysis.

So, before applying pointer analysis the right abstraction for a specific problem has to be chosen. Usually, this kind of analysis will result in an over approximation of the actual problem. Under approximations are unsound and the exact points-to sets are not computable. Thus, a suitable over approximation has to be found which is exact enough for a specific question to be answered.

Just to recapitulate two examples, he introduced abstractions based on type filtering, i.e, points-to sets are calculated on the bases of types of the potential object during a program execution. Furthermore, he explained field sensitive abstractions. Here the main property of interest is the field to which an object is assigned and this information is used to calculate the points-to sets. More examples and more advance techniques like refinement demand-driven analysis are shown in the slide set which will hopefully appear on the summer school webpage.

Garbage Collection and the Metronome GC

David started his lectures by showing off a bit He showed a nice demo of what the Metronome system is able to achieve in terms of real-time constraints. Definitely very interesting and it fortifies my belief that a Java-like language will be the next system programming language succeeding C/C++.

Afterwards, he gave a short introduction to mark/sweep and semi-space collectors. Useful was his explanation about the actual semantics of StopTheWorld, parallel, concurrent, and incremental GCs supported with an illustration (should remember that one). BTW: The world needs a better book on garbage collection. I don’t like the one of Jones and Lins. It does not solve my problems

Eventually, he started explaining the Metronome-2 systems. The paging approach let me wonder whether there is anything an operating system is actually doing for a modern VM. Well there is, but is it enough to justify the additional trouble? Dreaming of Singularity… The second lesson was basically dedicated to synchronization issues and parallel/concurrent data structures like lock-free stacks and which strategies are out there to implement them. This was a nice addition to what we discussed during Yannis’ lectures and gave me some basic inspiration to implement a lock-free ring buffer for multiple writers and a single reader.

His explanation of all the details of the metronome algorithm and how the different phases interact was quite difficult, and well, not to easy to follow especially since I lost the overall picture from time to time. But well, it is a hard problem and a lot of engineering without a simple solution as it seems.

Abstract Interpretation

The last topic at the summer school was abstract interpretation and the lectures were given by Mr. Abstract Interpretation Patrick Cousot himself. Even so it is a theoretical topic, I liked his introduction. Probably for some of the people it was to basic, but since I never had looked at it before, for me it was the right level of detail and complexity to get an idea what abstract interpretation is actually about.

Unfortunately, my own notes are very spares, and I was not able to retrieve the slide set up to now. However, abstract interpretation tries to provide a sound approximation of the semantics of a computer program, to enable various kinds of static analysis. The main problem here is, similar to pointer analysis, to choose the right abstraction for a given problem.

The examples I recall could have fit into Summit’s presentation about bound computation of loops as well. He introduced ideas like step-wise approximation and other techniques. But, well, unfortunately my memory is too blurry to write something down here with certainty. Beside the introduction of the formal techniques, he also spent some time on how to implement them with Ocaml examples. He also made quite some advertisement for his product ASTRÉE, which originally was developed to analyze code for avionic systems. Well, if I can get my hands on his slides, I might add some more information about the content, but for the moment that’s it.

Where to go next Year?