Iris Workshop 2019 (original) (raw)

The first edition of the Iris workshop will be held in Aarhus and it will be focused on Iris-related research to allow for in-depth talks and discussions. There will be a two-day long program with talks on Monday 28 October and Tuesday 29 October. Participants are encouraged to stay 1-3 days longer if they can, for more informal discussions and interaction.

Invited speakers

• Dan Frumin (Radboud University, The Netherlands): Compositional Non-Interference for Fine-Grained Concurrent Programs
• Bart Jacobs (KU Leuven, Belgium): Specifying I/O using Abstract Nested Hoare Triples
• Ralf Jung (MPI-SWS, Germany): Logical Atomicity in Iris: The Good, the Bad, and the Ugly
• Gregory Malecha (Bedrock Systems, USA): Iris in Industry
• François Pottier (Inria, France): Playing spy games in Iris

Program

The workshop will take place at Department of Computer Science, Aarhus University, Aabogade 40, Building 5794, 8200 Aarhus N.

Monday 28 October

• 09:30 - 10:30: Ralf Jung (MPI-SWS, Germany): Logical Atomicity in Iris: The Good, the Bad, and the Ugly[abstract] [slides]
  One major use-case of Iris is giving modular specifications to concurrent data structures and algorithms. However, this begs the question: what is the right specification? For concurrent variants of established sequential data structures, one widely accepted specification is linearizability: the concurrent variant should behave as if each operation would take effect atomically. Unfortunately, linearizability is an extra-logical notion: when working inside the Iris program logic, there is no way to make use of the fact that some data structure is linearizable.
  To remedy this, the original Iris paper (based on prior work on TaDA) proposed a form of program specification dubbed "logically atomic Hoare triples". These triples provide a simple way to turn a specification of a sequential data structure (say, a stack) into a concurrent variant of the same specification, stipulating that each operation must "behave atomically". This enables clients of logically atomic triples to make use of the invariant rule, the key proof rule in Iris to reason about an atomic step of execution.
  Since then, we have managed to simplify the encoding of logical atomicity in Iris, and we have implemented that encoding in Coq to enable interactive machine-checked proofs of both logically atomic data structures and clients in the usual Iris style. In this talk, I will introduce logical atomicity and its encoding in Iris. I will talk about what works nicely (the "good"), what is not supported by the formalism (the "bad"), and what is still less ergonomic in Coq than we would like (the "ugly").
• 10:30 - 11:00: Coffee break
• 11:00 - 11:30: Amin Timany (KU Leuven, Belgium): Aneris: A Logic for Node-Local, Modular Reasoning of Distributed Systems[abstract]
  Building network-connected programs and distributed systems is a powerful way to provide availability in a digital, always-connected era. However, with great power comes great complexity. Reasoning about distributed systems is well-known to be difficult.
  In this paper we present Aneris, a novel framework based on separation logic supporting modular, node-local reasoning about concurrent and distributed systems. The logic is higher-order, concurrent, with higher-order store and network sockets, and is fully mechanized in the Coq proof assistant. We use our framework to verify an implementation of a load balancer that uses multi-threading to distribute load amongst multiple servers and an implementation of the two-phase-commit protocol with a replicated logging service as a client. The two examples certify that Aneris is well-suited for both horizontal and vertical modular reasoning.
• 11:30 - 12:00: Jonas Kastberg Hinrichsen (ITU, Denmark): Actris: Session-Type Based Reasoning in Separation Logic[abstract]
  Message passing is a useful abstraction to implement concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functional correctness of programs that use a combination of the aforementioned features. Actris combines the power of modern concurrent separation logics with a first-class protocol mechanism—based on session types—for reasoning about message passing in the presence of other concurrency paradigms. We show that Actris provides a suitable level of abstraction by proving functional correctness of a variety of examples, including a distributed merge sort, a distributed load-balancing mapper, and a variant of the map-reduce model, using relatively simple specifications. Soundness of Actris is shown using a continuation-passing style (CPS) interpretation of its protocol mechanism into the Iris framework. We mechanised the theory of Actris, together with tactics for symbolic execution of programs, as well as all examples in the paper, in the Coq proof assistant.
• 12:00 - 12:30: Rodolphe Lepigre (MPI-SWS, Germany): Extending Iris with Prophecy Variables[abstract]
  In this talk, I will present a recent addition to the Iris framework: prophecy variables. Prophecy variables can be used to predict what will happen later in the execution of a program, while reasoning about its current state. They were first introduced by Abadi and Lamport in the nineties, but were never formally integrated into a Hoare-style program logic before. Thanks to the addiction of prophecy variables we are now able to verify logical atomicity (a relative of linearizability that will be presented by Ralf) for concurrent data structures like RDCSS or the Herlihy-Wing queue in Iris. These data structures are tricky because the linearization points of their operations (i.e., the precise point in their execution at which they appear to take effect) can sometimes only be identified after the fact (it may depend on future events). And as we will see that is the kind of situation where prophecy variables can help. This is joint work with Ralf Jung, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer and Bart Jacobs.
• 12:30 - 14:00: Lunch
• 14:00 - 15:00: François Pottier (Inria, France): Playing spy games in Iris[abstract]
  I will discuss the specification and proof in Iris of a "local generic solver", that is, an on-demand, incremental, memoizing least fixed point computation algorithm. Although the solver uses long-lived mutable internal state for several purposes, including memoization and "spying", it is apparently pure: no side effects are mentioned in its specification. The proof uses prophecy variables, which it exploits both directly and in the proof of a restricted infinitary conjunction rule. This is joint work with Paulo Emílio de Vilhena and Jacques-Henri Jourdan.
• 15:00 - 15:30: Léo Stefanesco (IRIF, France): Parsimonious steps toward termination in Iris[abstract]
  I will report on an early work whose purpose is reasoning about termination in Iris. This is achieved by constructing a weak simulation between the program and an abstract transition system. The weakness of the simulation comes from the fact that our weakest precondition is defined as the guarded fixpoint of a least fixpoint. This is joint work with Amin Timany and Lars Birkedal.
• 15:30 - 16:00: Coffee break
• 16:00 - 16:30: Philippa Gardner (Imperial College, UK): Compositional Reasoning for the Termination of Fine-grained Concurrent Programs
• 16:30 - 17:30: Gregory Malecha (Bedrock Systems, USA): Iris in Industry[abstract]
  BedRock Systems is developing a trustworthy software foundation for the connected world. To achieve this goal, we are applying formal methods pervasively across our stack ranging from a capability-based micro-hypervisor to a VMM and auxiliary components. Tackling software at this scale leads to interesting engineering difficulties. We have recently embraced Iris to serve as the foundation for our reasoning, but many challenges still remain. In this talk, I discuss some of those challenges. On the language side of things, BedRock Systems is using C++ and we have developed a tool (based on Clang) to convert C++ programs into abstract syntax trees which we ascribe semantics to axiomatically. To make reasoning about our programs more tractable, we have (and are) developing automation to improve the verification experience, especially for the non-concurrent portions of our code. At the system level, we are seeking to leverage Iris's logic to modularize the way that application programs reason about capabilities across the entire system. Doing this requires reasoning about multiple address and capability spaces as well as the interaction between trusted and untrusted code. Beyond the purely technical problems, BedRock's Systems' embrace of formal methods means that we have the opportunity, and the obligation, to train systems developers to write verifiable code and the specifications to go along with it. While we don't expect developers to immediately be able to verify sophisticated concurrent algorithms initially, we are working on representative examples to build a cookbook of verification recipes that can be more easily understood, applied, and automated.
• 18:30 - 21:30: Conference dinner at No. 16 (Europaplads 16, Aarhus)

Tuesday 29 October

• 09:30 - 10:30: Dan Frumin (Radboud University, The Netherlands): Compositional Non-Interference for Fine-Grained Concurrent Programs[abstract]
  We present SeLoC: a relational separation logic for verifying non-interference of fine-grained concurrent programs in a compositional way. SeLoC is more expressive than previous approaches, both in terms of the features of the target programming language, and in terms of the logic. The target programming language supports dynamically allocated references (pointers), higher-order functions, and fine-grained fork-based concurrency with low-level atomic operators like compare-and-set. The logic provides an invariant mechanism to establish protocols on data that is not protected by locks. This allows us to verify programs that were beyond the reach of previous approaches.
  A key technical innovation in SeLoC is a relational version of weakest preconditions to track information flow using separation logic resources. On top of these weakest preconditions we build a type system-like abstraction, using invariants and logical relations. SeLoC has been mechanized on top of the Iris framework in the Coq proof assistant.
• 10:30 - 11:00: Coffee break
• 11:00 - 11:30: Glen Mével (Inria, France): Iris for Multicore OCaml[abstract]
  I will present some preliminary work on instantiating the Iris framework for the Multicore OCaml language.
• 11:30 - 12:00: Armaël Guéneau (Inria, France): Formal verification of an incremental cycle detection algorithm[abstract]
  In this talk, I will present the analysis of a state-of-the-art incremental cycle detection algorithm due to Bender, Fineman, Gilbert, and Tarjan. The algorithm maintains subtle invariants, and features a non trivial asymptotic, amortized complexity bound. I will detail how we exploit Separation Logic with Time Credits to simultaneously verify the correctness and the worst-case amortized complexity of the modified algorithm. This is joint work with Arthur Charguéraud, Jacques-Henri Jourdan and François Pottier.
• 12:00 - 12:30: Andrew Appel (Princeton, USA): Recent developments in the Verified Software Toolchain[abstract]
  The Verified Software Toolchain has a powerful and expressive program logic for the C programming language, proved sound with a machine-checked proof in Coq w.r.t. the operational semantics of CompCert C, and with a capable proof-automation system. I will summarize several recent developments in the VST project: Improved proof automation (Wang and Appel), modularity and linking (Beringer and Appel), funspec subsumption (Beringer and Appel), Cbench (Wiedijk) verifications (Appel), floating point, I/O reasoning (Mansky and Appel), foundational connection to CertiKOS operating system (Mansky, Honore, and Appel), foundational shared-memory concurrency (Cuellar, Giannarakis, Madiot, Mansky, Beringer, Appel), assertions-as-annotatoins (Wang and Cao), connection to Certicoq (Korkut and Appel).
• 12:30 - 14:00: Lunch
• 14:00 - 15:00: Bart Jacobs (KU Leuven, Belgium): Specifying I/O using Abstract Nested Hoare Triples[abstract]
  We propose a separation logic-based approach for modular specification and verification of the I/O behavior of a program. The approach uses higher-order separation logic predicates to express "abstract nested Hoare triples" that abstractly associate a precondition and a postcondition with an I/O action. The approach supports verifying higher-level I/O actions built on top of lower-level ones, as well as "virtual I/O" actions that in fact just manipulate memory.
• 15:00 - 15:30: Aina Linn Georges (Aarhus University, Denmark): Implementing a Capability Machine model into Iris[abstract]
  Capabilities exist at multiples levels of abstraction, with the shared tagline: “an unforgeable token of authority”. At the machine level, a capability gives authority over a piece of memory. Lau Skorstensgaard et. al. [1][2] developed methods for reasoning about capability machines; in [1] they define a logical relation for a capability machine with local capabilities, and present a calling convention that enforces local state encapsulation and well-bracketed control flow. I will present the formalisation of such a model into Iris. I will show the embedding of a capability machine language (in which programs lie in memory) into Iris, and the formalisation of the Logical Relation to reason about programs in that language.
  [1] Skorstengaard L., Devriese D., Birkedal L. (2018) Reasoning About a Machine with Local Capabilities. Programming Languages and Systems. ESOP 2018.
  [2] Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. 2019. StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities. Proc. ACM Program. Lang. 3, POPL, Article 19 (January 2019)
• 15:30 - 16:00: Coffee break
• 16:00 - 16:30: Paolo Giarrusso (TUDelft, The Netherlands): Step-Indexed Logical Relations for (guarded) Dependent Object Types[abstract]
  The metatheory of the Scala core type system (DOT), first established recently, is still hard to extend, like other systems combining subtyping and forms of dependent types. Soundness of important Scala features remains an open problem in theory and in practice. To address some of these issues, we have mechanized in Coq a semantic soundness proof for a DOT variant called guarded DOT, and discuss both additional expressivity and additional restrictions. This is challenging, because in DOT variables can be in scope in their own type, objects can define mutually recursive and impredicative type members, and can contain evidence of subtyping relations that must be sound. We address these challenges by novel applications of step-indexing, as supported by the Iris program logic.
• 16:30 - 17:00: Hai Dang (MPI-SWS, Germany): RustBelt Relaxed[abstract]
  The original RustBelt made the significant simplifying assumption that the language is sequentially consistent. We adapt RustBelt to account for the relaxed-memory operations that concurrent Rust libraries actually use, in the process uncovering a data race in the Arc library. We will focus the discussion on how to reason about resource reclamation under relaxed memory, using variants of cancellable invariants that are improved with a logical construction we call synchronized ghost state.

Organizers

• Lars Birkedal (Aarhus University, Denmark)
• Robbert Krebbers (Delft University of Technology, The Netherlands)
• Sofia Rasmussen (Local organization)

Practical information

Travel by airplane to Aarhus

• Aarhus Airport, Tirstrup (AAR). The airport situated closest to Aarhus, but it is small and has only few connections. Transportation time to the city of Aarhus is approximately 45 minutes by bus 925x, which departs 20 minutes after each arrival.
• Billund Airport (BLL). A slightly bigger airport, with more connections. The transportation time by bus 912x is approximately one hour and a half to the city of Aarhus. The bus departs almost every hour.
• Copenhagen Airports (CPH). A large airport with lots of connections. You can continue to Aarhus by domestic flights or by train. Flight time to Aarhus Airport is 40 minutes, but train is often easier. The direct train from Copenhagen Airport to central Aarhus is about three and a half hours.

Travel by train to Aarhus

There are frequent trains from Copenhagen to Aarhus and also many from Hamburg (and thus the European train network). You can use the Journey Planner to schedule your trip. Danish rail services are called DSB.

Accommodation in Aarhus

We recommend that you find accommodation in the city center or in the north of the city. At the computer science department we usually book the following hotels:

• Lower-budget:Cabinn or Wake Up
• Mid-budget:The Mayor
• Higher-budget:Scandic City

Registration

Registration is free, but you should register online at https://events.au.dk/iris2019. The deadline is 11 October.

About Aarhus

With approximately 300.000 inhabitants, Aarhus is the second largest city in Denmark. It was founded by the Vikings in the 8th century, and is located in a natural bay along a small river and surrounded by forests. Aarhus is often referred to as "the youngest and brightest city in Denmark” because of its large student population, almost 1/5 of the residents are students. The young population and the fact that the city is the unofficial "capital of west Denmark" means that Aarhus has a large concentration of attractions, shopping and city life.

What to see and do in Aarhus:

• ARoS Aarhus Art Museum. One of the biggest museums in the northern part of Europe. Enjoy the permanent and temporary exhibitions or take a walk in Your Rainbow Panorama with a scenic view of the city.
  Address: Aros Allé 2, 8000 Aarhus C.
• The Old Town. A Danish Open Air Museum / The Old Town ("Den Gamle By") was founded in 1909 as the world's first open-air museum of urban history and culture. Take a tour in the city as it looked from the 16th century and forward.
  Address: Viborgvej 2, 8000 Aarhus C.
• Tropical Houses at the Botanical Garden. The Greenhouses will give you an educational and sensuous experience strolling through the beautiful and varied sceneries, and you will find plants from most parts of the world. There is a free admission to the Greenhouses and the café serves great food at fair prices.
  Address: Møllevejen 10, 8000 Aarhus C.
• DOKK1. The city's new impressive library which is located at the waterfront in the city center. Here you will find much more than just books.
• Harbors, forests and beaches. If the weather behaves, Aarhus also has a lot of outdoor attractions/activities. They obviously include strolling the harbors, forests and beaches on both the north and south side of the city. On the south side of the city close to the Queens summer residence Marselisborg you will find Marselisborg Habor with nice restaurants and the Marselisborg forest extending along the ocean and beaches.
• Cafés along the river or in the Latin Quarter. Most of these cafés turn into regular bars towards midnight and there are several clubs downtown.

The website Visit Aarhus provides lots of information about Aarhus.