FMOℤ 2016

Program

Abstracts

Rob van Glabbeek

Ensuring Liveness Properties of Distributed Systems
(A Research Agenda)

Often fairness assumptions need to be made in order to establish liveness properties of distributed systems, but in many situations these lead to false conclusions.

This talk presents a research agenda aiming at laying the foundations of a theory of concurrency that is equipped to ensure liveness properties of distributed systems without making fairness assumptions. This theory will encompass process algebra, temporal logic and semantic models, as well as treatments of real-time. The agenda also includes developing a methodology that allows successful application of this theory to the specification, analysis and verification of realistic distributed systems, including routing protocols for wireless networks.

Contemporary process algebras and temporal logics fail to make distinctions between systems of which one has a crucial liveness property and the other does not, at least when assuming justness, a strong progress property, but not assuming fairness. Setting up an alternative framework involves giving up on identifying strongly bisimilar systems, inventing new induction principles, developing new axiomatic bases for process algebras and new congruence formats for operational semantics, and creating new treatments of time and probability.

Even simple systems like fair schedulers or mutual exclusion protocols cannot be accurately specified in standard process algebras (or Petri nets) in the absence of fairness assumptions. Hence the work involves the study of adequate language or model extensions, and their expressive power.

Paper available at http://theory.stanford.edu/~rvg/abstracts.html#agenda

Ralf Huuck

How to Make Software Engineers Use Software Model Checking

Software verification and software model checking is typically firmly in the realm of research labs or academia. The use of formal verification techniques is considered by industry as scary and impractical for real world software engineering. In this talk we present our experience from developing software analysis tools based on model checking, abstract interpretation and SMT solving and applying them to industrial software development processes. Currently, our software analysis tools are proverbial push-button and used by hundreds of companies and tens of thousands of software developers across the world. This has not been without challenges and lessons of which we share some in this presentation.

Larissa Meinicke

An algebra of synchronous atomic steps

This research started with an attempt to provide an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an interpretation of the more abstract algebra. Many of the core properties needed for rely/guarantee reasoning can be shown to hold in the abstract algebra where their proofs are simpler and hence allow a higher degree of automation. Moreover, the realisation that the synchronisation mechanisms of standard process algebras, such as CSP and CCS/SCCS, can be interpreted in our abstract algebra gives evidence of its unifying power. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support.

Rajeev Gore and Dirk Pattinson

Formal Verification/Synthesis of Complex Vote-counting Algorithms

We describe two strands of our current work. The first is our work on formalising vote-counting algorithms and their specifications in HOL, and then using HOL to verify that the algorithm is correct amongst other properties. The second is an orthogonal approach where we specify the process of vote-counting via a set of logical rules and then automatically extract an algorithm for vote-counting using Coq.

Graeme Smith

Verifying concurrent objects on weak memory models

Concurrent objects are those designed to be accessed simultaneously by more than one thread. A number of tool-supported proof methods exist for verifying such objects. This talk will discuss approaches to adapting one such method to the context of weak memory models. Weak memory models allow instructions in a program to appear as if they occurred out of order. They are standard in both high-level programming languages (to allow compiler optimisations) and multi-core architectures (to improve efficiency at run-time).

June Andronick

Interrupts in OS code: let’s reason about them.
Yes, this means concurrency

Existing modelled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where it runs the flight control software of a high-assurance quadcopter. To provide low latency, the eChronos OS runs with interrupts enabled and provides a preemptive scheduler. In terms of verification, this means that concurrency reasoning is required, which significantly increases the complexity: application and OS instructions may be interleaved with interrupt handler instructions. In our work we explicitly model the effect of interrupts and their handling by the hardware and OS. We provide a general formal model of the interleaving between OS code, application code and interrupt handlers. We then instantiate this model to formalise the scheduling behavior of the eChronos OS, and prove the main scheduler property: the running task is always the highest-priority runnable task.

Mark Utting

A Weakest-Precondition Semantics for Whiley

Whiley is a verification-friendly programming language that employs extended static checking to eliminate many errors at compile time. It is a hybrid object-oriented and functional programming language, and is intended for programming small embedded applications. This talk describes a weakest precondition semantics for the Whiley programming language, The semantics is a simple definitional extension of the standard refinement calculus. The calculus can be used to reason about simple object-oriented systems and provides a good basis for mapping Whiley into the Boogie verification language.

Lindsay Groves and Brijesh Dongol

Linking correctness conditions for concurrent objects
and contextual trace refinement

Correctness of concurrent objects is defined in terms of safety properties such as linearizability, sequential consistency, and quiescent consistency, and progress properties such as wait-, lock-, and obstruction-freedom. These properties, however, only refer to the behaviours of the object in isolation, which does not tell us what guarantees these correctness conditions on concurrent objects provide to their client programs. This paper investigates the links between safety and progress properties of concurrent objects and a form of trace refinement for client programs, called contextual trace refinement. In particular, we show that linearizability together with a minimal notion of progress are sufficient properties of concurrent objects to ensure contextual trace refinement, but sequential consistency and quiescent consistency are both too weak. Our reasoning is carried out in the action systems framework with procedure calls, which we extend to cope with non-atomic operations.

Yang Zhao

Model Checking Cache Coherence in System-Level Code

Cache coherence is a key consistency requirement between the shared main memory and individual caches for a multiprocessor framework. Several months ago, we started a project to verify the cache coherence of a system-level C codebase (50,000+ lines), which runs in an environment that does not provide hardware-level guarantees, requiring programmers to ensure correct cache coherence manually through explicit FLUSH and INVALIDATE operations.

After initial evaluation and comparison of many model checking tools, we believe that SPIN is the most suitable one. However, pure model checking is not sufficiently scalable to verify such a large codebase. Therefore, we are currently investigating a hybrid model checking solution with some static analysis techniques to reduce the model size via abstraction and program slicing, and restrict the interleavings explored.

In this talk, we will share our model checking experiences. In particular, we will discuss (1) our evaluation of different model checking tools, (2) the Promela model we use to verify the cache coherence, (3) initial model checking experience for verifying the coherence in concurrent quicksort algorithm, and (4) the automatic model extraction from large codebase in C.