ABSTRACT. Modern multiprocessors exhibit behaviours described as weak memory models. In recent work we proposed an axiomatic generic framework to describe these, and instantiated it for SC, TSO/Intel x86, IBM Power, ARM, and C++ restricted to release-acquire atomics. This foundational work was accompanied by empirical studies on two levels: first, extensive testing on ARM hardware revealed a behaviour later acknowledged as a bug by ARM; second, using a new static analysis tool called mole, more than 1500 software packages were scrutinised.

In this talk a brief overview of the work published in TOPLAS and PLDI will be provided, followed by a detailed account of mole. The talk will discuss both the design of mole as well as the results obtained.

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. In this talk I will present a logic for reasoning about release/acquire fences as defined in C11 memory model. The logic itself is an extension of relaxed separation logic.

ABSTRACT. Power is a RISC architecture developed by IBM, Freescale, and several other companies and implemented in a series of POWER processors. The architecture features a relaxed memory model providing very weak guarantees with respect to the ordering and atomicity of memory accesses.

Due to these weaknesses, some programs that are correct under sequential consistency (SC) show undesirable effects when run under Power. We say that these programs are not robust against the Power memory
model. Formally, a program is robust if every computation under Power has the same data and control dependencies as some SC computation.

Our contribution is a decision procedure for robustness of concurrent programs against the Power memory model. It is based on three ideas. First, we reformulate robustness in terms of the acyclicity of a happens-before relation. Second, we prove that among the computations with cyclic happens-before relation there is one in a certain normal form. Finally, we reduce the existence of such a normal-form computation to a
language emptiness problem. Altogether, this yields a PSpace algorithm for checking robustness against Power. We complement it by a matching lower bound to show PSpace-completeness.
 

Joint work with Egor Derevenetc.

ABSTRACT. I will report on ongoing work to investigate the relaxed memory model proposed by the recent OpenCL 2.0 standard. The OpenCL memory model draws heavily on the one used by C/C++, but also extends it in interesting and subtle ways, by adding such GPU-specific concepts as thread hierarchies, memory hierarchies, and synchronisation barriers. In my talk, I will describe a draft formalisation of the OpenCL memory model that my coauthors and I have written in the ".cat" format, and also how the Herd memory-model simulator has been extended to allow our formalisation to be tested for faithfulness.

ABSTRACT. Graphics processing units (GPUs) are specialized highly concurrent microprocessors. Traditionally, these chips have been used for accelerating graphics rendering. However, since the advent of general purpose GPU programming frameworks such as Nvidia's CUDA, they have found their way into many
applications, especially scientific and embedded computing.

To enable precise reasoning about GPU programs, a formal memory model is desirable. A necessary first step toward building a model is the thorough
testing of the hardware. The model cannot be based on the vendor documentation alone, as it typically contains little detail and is at times ambiguous.

In this talk, I will describe our approach to testing GPU memory models, and will discuss some of our testing results.

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).