Multicore and more

During the past week Adam attended the UPMARC Multicore Computing Summer School 2012. A wide range of topics were covered, including verified microkernels, a structured approach to aliasing in OO languages and an effect-tracking approach to deterministic execution of object-oriented code. A particular highlight was the lecture series by Martin Vechev. There, a method for "Machine-Assisted Concurrent Programming" was presented where conservative overapproxmations (based on abstract interpretation) are used not only to prove correctness of programs but also to introduce changes in the programs which remedy defects detected during verification. For example, this can be used to automatically introduce atomic sections and fences in concurrent code.