CONSEQUENCER: Sequentialization-based Verification of Concurrent Programs with FIFO channels

The steady exponential increase in processor performance
has reached the inevitable turning point, at which it is no longer feasible to
increase the clock speeds of individual processors. To achieve
higher performance, processors now contain several cores that work in parallel.
Consequently, concurrency has become an important aspect across many
areas within computer science, such as algorithms, data structures, programming
languages, software engineering, testing, and verification.
Concurrent programs consist of several computations or threads that are
active at the same time and communicate through some control mechanism, such as
locks and shared variables, or message passing. Concurrent programming is difficult:
programmers do not only have to guarantee the correctness
of the sequential execution of each individual thread, they must also consider
nondeterministic interferences from other threads. Due to these complex
interactions, considerable resources are spent to repair buggy concurrent
software.

Testing remains
the most used (and often the only known) paradigm in industry to find errors,
even though the inherently nondeterministic nature of the concurrent
schedules causes errors that manifest rarely and are difficult to reproduce and repair.
Testing is not effective in detecting such concurrency errors, as all
possible executions of the programs have to be explored explicitly.
Consequently, testing needs to be complemented by automated verification tools that
enable detection of errors without explicitly (i.e. symbolically) exploring executions.

On the other hand, the state of the art for concurrent program verification lags behind that for sequential programs.
Here, researchers have successfully explored a wide range of techniques and
tools to analyse real-world sequential software.
A recently proposed approach for symbolic verification of concurrent programs
called sequentialization, consists in translating the concurrent program
into an equivalent sequential program so that
verification techniques or tools that were originally designed for
sequential programs can be reused without any changes.

This technique has been successfully used to discover bugs in existing software
and has been implemented in several tools (e.g., Corral by Microsoft Research).
However, existing sequentialization schemas do not support weak memory models,
or distributed programs that use message passing.

In this proposal we address these weaknesses and plan the development of automated verification tools that enable detection of errors in concurrent programs in a systematic and symbolic way. More specifically, we will develop the theory, models and algorithms that underpin sequentialization of concurrent programs that use FIFO channels. This will enable us to capture within a single framework (1) concurrent programs that communicate through shared memory, for the variety of (weak) memory models that are implemented in today's computer architectures, and (2) distributed programs which use a message-passing communication style (i.e., the two most commonly used programming models for concurrency).

A key deliverable of this project will be a set of automatic code-to-code translators, called ConSequencer, for C programs that use Pthread (for shared variables) and MPI (for distributed programs). This will serve as a concurrency plugin for any program verification tool designed for sequential programs. We will evaluate our solutions on publicly available benchmarks using a range of robust sequential verification tools for the C language.

Part of the proposed research is foundational in nature and
thus the primary pathway to impact for the obtained knowledge
will be through academic publications.
We have identified key international conferences and journals that we will target for
dissemination. They cover the academic communities where our results will be of
most interest.

In addition to the traditional academic publications,
we will also build a project website that will contain
all relevant information about this project (tools, papers, benchmarks,
evaluation, etc.). A strong focus here will be on providing enough details so
that (1) all experiments can be independently repeated, and (2) all
translations can be independently re-implemented. In particular, we plan to
make all translations available as open-source software.

A key deliverable of this project will be an automatic code-to-code translator
called CONSEQUENCER that sequentializes C programs that use
Pthreads (for multi-threaded programs with shared variables) and
MPI (for distributed programs).
We will make CONSEQUENCER available in different
versions, to target different audiences: as a complete black-box verification
tool (i.e., coupled with a sequential verification backend), aimed at
software developers; as an stand-alone concurrency pre-processor, aimed at
practical verification experts; and in source form, aimed at verification researchers and
tool developers. Third, we will participate in competitions for software
verification tools. Such competitions have recently emerged as
both an important driver to shape practical research in program verification
and a good channel for disseminating research results in a condensed form. Our
experience from the last two SV-COMP competitions indicates that a
good competition result translates into immediate impact on the field. Fourth,
and finally, we will contribute further benchmarks for such competitions, in
the form of programs produced by our sequentialization translations. Here, the
impact is longer term and less direct, as it provides incentives to the
developers of sequential verification tools to take the characteristics of
these programs into account.

The technology proposed in this project can be applied to verify
hardware-software designs or applications on advanced computer architectures.
We plan to build on the successful existing
collaborations of ESS with ARM and Imagination. Obviously, the partly
foundational nature of the research, and the small scale of the project, will
make an immediate impact on industrial practice (e.g., in form of industrial
tool applications) difficult. However, the results of this project will serve
to get industrial interest and hence their support. Feedback from these initial
industrial collaborations will also help the PI developing a follow-on project,
which will be a larger and longer-term proposal with direct industrial
involvement.

Another application of this research is in security, as many attacks exploit
errors in the software implementing the security protocols. The PI is a member
of the GCHQ-supported Centre of Excellence in CyberSecurity Research in
Southampton, and will work through this with the Research Institute in
Automated Program Analysis and Verification and with national security
agencies.

The final pathway to impact is through education of the young researcher and
students. The researcher will benefit by working with the PI and the two
PhD students. He or she will gain detailed knowledge about verification of
concurrent systems and model checking technology, which are areas with a high
demand for (but with low supply of) experts in the UK. The
researcher will also gain experience in supervising research students, which
will be beneficial for a potential further academic career. The PhD students
will benefit by working with the researcher, which will help them in the timely
completion of their PhD programme.