ABSTRACT. We present a methodology for the verified compilation of high-level managed languages like Java or C# whose intermediate representations provide support for shared-memory synchronization and automatic (concurrent) memory management. Ensuring the correctness of compilers for these languages is challenging because high-level actions are translated into sequences of non-atomic actions with compiler-injected snippets of potentially racy code; the behavior of this code depends not only the actions of other threads, but also on out-of-order reorderings performed by the processor. A naïve correctness proof of the compiler would require reasoning over all possible thread interleavings that can arise during execution, an impractical and non-scalable exercise.

To address this challenge, we define a refinement-based proof methodology that precisely relates concurrent code expressed at different abstraction levels, cognizant throughout of the relaxed memory semantics of the underlying processor. Our technique allows the compiler writer to reason compositionally about the atomicity of low-level concurrent code used to implement managed services. We validate the effectiveness of our approach by demonstrating the verified compilation of the non-trivial components comprising a realistic concurrent garbage collector, including racy write barriers and memory allocators.

ABSTRACT. We survey our research on concolic testing of concurrent programs. Based on concrete and symbolic executions of a concurrent program, our testing techniques derive inputs and schedules such that the execution space of the program under investigation is systematically explored. We will focus on con2colic testing which introduces interference scenarios. Interference scenarios capture the flow of data among different threads and enable a unified representation of path and interference constraints.

ABSTRACT. The Linux kernel has long run correctly on systems with weak memory models, in fact, none of the systems supporting Linux feature a sequentially consistent memory model.  Therefore, the Linux kernel provides a number of primitives that provide various ordering guarantees, including split counters, memory allocators, locking primitives, memory-barrier primitives, atomic operations, and read-copy update (RCU).  Given that  RCU is relatively unfamiliar, this talk will give a brief RCU overview.

However, all of this weak ordering does pose a validation challenge, especially in recent years.  The second half of this talk will therefore focus on validation challenges specific to the Linux kernel, how the Linux kernel community approaches validation and what more might be possible.

ABSTRACT.  

In this talk, I will try to answer two key questions regarding the 2011 C/C++ memory model: (1) What high-level principles can programmers use to reason about their programs? (2) What source-to-source transformations can optimising compilers soundly perform?

ABSTRACT. We address the problems of verification and fence inference in infinite-state concurrent programs running on relaxed memory models such as TSO and PSO. The talk surveys techniques using predicate abstraction as well as techniques based on numerical domains with refinement propagation. We show how these techniques can be effectively applied to verify challenging concurrent algorithms, including state of the art concurrent work-stealing queues.

ABSTRACT. We developed a novel Functional Object-Oriented PARallel framework (FOOPAR) for analyzable high-level high-performance computing in Scala. Central to this framework are Distributed Memory Parallel Data structures, i.e., collections of data distributed in a shared nothing system together with parallel operations on these data.

In this position paper we shortly present FOOPAR’s design and focus on its properties w.r.t. analyzability and correctness. We prove the correctness and safety of one communication algorithm and show how specification testing (via ScalaCheck) can be used to bridge the gap between proof and implementation.

ABSTRACT. The third round of the Kurt Gödel Research Prize Fellowships Program, under the title: Connecting Foundations and Technology, aims at supporting young scholars in early stages of their academic careers by offering highest fellowships in history of logic, kindly supported by the John Templeton Foundation. Young scholars being less or exactly 40 years old at the time of the commencement of the Vienna Summer of Logic (July 9, 2014) will be awarded one fellowship award in the amount of EUR 100,000, in each of the following categories:

• Logical Foundations of Mathematics,
• Logical Foundations of Computer Science, and
• Logical Foundations of Artificial Intelligence

The following three Boards of Jurors were in charge of choosing the winners:

• Logical Foundations of Mathematics: Jan Krajíček, Angus Macintyre, and Dana Scott (Chair).
• Logical Foundations of Computer Science: Franz Baader, Johann Makowsky, and Wolfgang Thomas (Chair).
• Logical Foundations of Artificial Intelligence: Luigia Carlucci Aiello, Georg Gottlob (Chair), and Bernhard Nebel.

http://fellowship.logic.at/

ABSTRACT. The aim of the FLoC Olympic Games is to start a tradition in the spirit of the ancient Olympic Games, a Panhellenic sport festival held every four years in the sanctuary of Olympia in Greece, this time in the scientific community of computational logic. Every four years, as part of the Federated Logic Conference, the Games will gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At the Award Ceremonies, the competition organizers will have the opportunity to present their competitions to the public and give away special prizes, the prestigious Kurt Gödel medals, to their successful competitors. This reinforces the main goal of the FLoC Olympic Games, that is, to facilitate the visibility of the competitions associated with the conferences and workshops of the Federated Logic Conference during the Vienna Summer of Logic.

This award ceremony will host the

• 3rd Confluence Competition (CoCo 2014);
• Configurable SAT Solver Challenge (CSSC 2014);
• Ninth Max-SAT Evaluation (Max-SAT 2014);
• QBF Gallery 2014; and
• SAT Competition 2014 (SAT-COMP 2014).

ABSTRACT. We describe a proof system for concurrent programs built on top of the Boogie framework. The proof system combines key features of several proof techniques, including separation-logic, the Owicki-Gries and rely-guarantee techniques, and movers, reduction, and abstraction in the style of our own earlier work on the QED proof system.

We have been using a concurrent mark-sweep garbage collector as a case study to drive the proof system and tool design. The top-level functional specification for the garbage collector is to appear invisible to application threads. We explain how we refine this top-level specification down to a concurrent implementation described at the level of individual memory accesses. We highlight challenges we encountered while carrying out a proof spanning such a large abstraction gap and how features of our proof system help us address them.