View: session overviewtalk overviewside by side with other conferences

09:00-10:30 Session 125J
Location: Blavatnik LT2
Automated verification of linearizability
Correctness of Concurrent Objects under Weak Memory Models
SPEAKER: Robert Colvin

ABSTRACT. Reasoning about the correctness of concurrent objects on weak memory models supported by modern multicore architectures is complicated. Traditional notions such as linearizability do not directly apply as the effect of an operation can become visible after the operation call has returned.

In this paper we develop a theory for correctness of concurrent objects under weak memory models. Central to our definitions is the concept of observations which determine when effects of operations become visible, and hence determine the semantics of objects, under a given memory model. The resulting notion of correctness, called object refinement, is generic as it is parameterised by the memory model under consideration. Our theory enforces the minimal constraints on the placing of observations and on the semantics of objects that underlie object refinement. Object refinement is suitable as a reference for correctness when proving new proof methods for objects under weak memory models to be sound and complete.

10:30-11:00Coffee Break
11:00-12:30 Session 127J
Location: Blavatnik LT2
Challenges of specifying concurrent program components

ABSTRACT. The purpose of this paper is to review some of the challenges of formally specifying components of concurrent programs in a manner suitable for refining them to an implementation. We present some approaches to devising specifications, in some cases investigating different forms of specification suitable for different contexts. Our focus is on shared variable concurrency rather than event-based process algebras.

Programming Without Refinement

ABSTRACT. To derive a program for a given specification R means to find an artifact P that satisfies two conditions: P is executable in some programming language; and P is correct with respect to R. Refinement-based program derivation achieves this goal in a stepwise manner by enhancing executability while preserving correctness until we achieve complete executability. In this paper, we argue that it is possible to invert these properties, and to derive a program by enhancing correctness while preserving executability (i.e. proceeding from one executable program to another) until we achieve absolute correctness. Of course, this latter process is possible only if we know what it means to enhance correctness.

Ordering strict partial orders to model behavioural refinement

ABSTRACT. Software is now ubiquitous and involved in complex interactions with the human users and the physical world in so-called cyber-physical systems (CPS) where the management of time is a major issue. Separation of concerns is a key asset in the development of these ever more complex systems. Two different kinds of separation exist : a first one corresponds to the different steps in a development leading from the abstract requirements to the system implementation and is qualified as vertical. It matches the commonly used notion of refinement. A second one corresponds to the various components in the system architecture at a given level of refinement and is called horizontal. Refinement has been studied thoroughly for the data, functional and concurrency concerns while our work focuses on the time modeling concern. This contribution aims at providing a formal construct for the verification of vertical separation in time models, through the definition of an order between strict partial orders used to relate the different instants in asynchronous systems. This work has been conducted using the proof assistant Agda and is connected to a previous work on the asynchronous language CCSL, which has also been modeled using the same tool.

12:30-14:00Lunch Break
14:00-15:30 Session 128J
Location: Blavatnik LT2
A more relaxed way to make concrete: uses of heuristic search to discover implementations
SPEAKER: John Clark

ABSTRACT. Over the past decades we have developed formal frameworks to refine specifications into more detailed representations. These handle both deterministic and probabilistic specifications. We also have developed means for relaxing formality when the occasion demands it (retrenchment).  In this talk I will explore approaches to inferring programs from test data (derived from a specification), particularly involving  the use of genetic programming (GP). I will pay particular attention to quantum artifacts, e.g. discussing how GP can find Shor's Quantum Discrete Fourier Transform circuits.  Such approaches generally work by 'homing in' on an appropriate program, using deviation of results from specified results as guidance. This can produce programs that are either right or nearly right. I'll do a round trip with evolutionary computation and indicate the use of GP in unearthing formal specification fragments from test traces for traditional programs (using mutation approaches to get rid of uninteresting potential invariants inferred).

15:30-16:00Coffee Break
16:00-18:00 Session 130I
Location: Blavatnik LT2
Refining Santa: An Excercise in Efficient Synchronization

ABSTRACT. The Santa Claus Problem is an intricate exercise for concurrent programming. This paper outlines the refinement step to develop a highly efficient implementation with concurrent objects, starting from a very simple specification. The efficiency of the implementation is compared to three other languages.

a Theory of Lazy Imperative Timing

ABSTRACT. We present a theory of lazy imperative timing.

19:15-21:30 Workshops dinner at Magdalen College

Workshops dinner at Magdalen College. Drinks reception from 7.15pm, to be seated by 7:45 (pre-booking via FLoC registration system required; guests welcome).