Partial order semantics for concurrent program verification
Lead Research Organisation:
University College London
Department Name: Computer Science
Abstract
Multiprocessor machines are now predominant, as most laptops, desktops,
servers, mobile phones and aircrafts routinely have multiple to many cores.
Unfortunately, concurrent programming is error-prone, which now affects
everyone given this trend towards more and more concurrency.
Let us mention for example a recent concurrency bug found in the PostgreSQL
database (see
http://archives.postgresql.org/pgsql-hackers/2011-08/msg00330.php). PostgreSQL
is one of the most popular database nowadays, and many websites rely on its
correct functioning. This bug was particularly difficult to observe (and
indeed is not fixed yet) because it only occurred on a multicore machine, and a
particular hardware platform, IBM Power.
Reproducing such bugs is as hard as observing them; thus testing can hardly
discover them. To prove a program free of errors, we would like to devise
automated techniques that analyse the code without executing it. Thus,
we can relieve programmers from the burden of writing the proofs of their
programs.
Yet, automatic verification of concurrent programs represents a challenge,
whether it aims at proving the full correctness of a program (e.g. a
program sorting a list actually sorts the list), or at checking specific
properties (e.g. the program is free of data races) short of full
correctness. We focus here on the latter: we would like to enhance
the scalability of tools checking that a concurrent program does not violate
certain safety-critical properties of interest.
We would like to show that scalable automatic verification can be achieved by
exploiting the rich history of partial orders for modeling concurrency.
servers, mobile phones and aircrafts routinely have multiple to many cores.
Unfortunately, concurrent programming is error-prone, which now affects
everyone given this trend towards more and more concurrency.
Let us mention for example a recent concurrency bug found in the PostgreSQL
database (see
http://archives.postgresql.org/pgsql-hackers/2011-08/msg00330.php). PostgreSQL
is one of the most popular database nowadays, and many websites rely on its
correct functioning. This bug was particularly difficult to observe (and
indeed is not fixed yet) because it only occurred on a multicore machine, and a
particular hardware platform, IBM Power.
Reproducing such bugs is as hard as observing them; thus testing can hardly
discover them. To prove a program free of errors, we would like to devise
automated techniques that analyse the code without executing it. Thus,
we can relieve programmers from the burden of writing the proofs of their
programs.
Yet, automatic verification of concurrent programs represents a challenge,
whether it aims at proving the full correctness of a program (e.g. a
program sorting a list actually sorts the list), or at checking specific
properties (e.g. the program is free of data races) short of full
correctness. We focus here on the latter: we would like to enhance
the scalability of tools checking that a concurrent program does not violate
certain safety-critical properties of interest.
We would like to show that scalable automatic verification can be achieved by
exploiting the rich history of partial orders for modeling concurrency.
Planned Impact
Verification of concurrent software is crucial to prevent safety-critical or
embedded devices to crash. Indeed, since these now routinely include multiple
cores, they rely on concurrent software for functioning.
This project will have impact on several communities: i) professional
programmers of concurrent software and ii) multiprocessors designers. Our
connections into the following companies constitute a way for the ideas to
impact industrial verification tools even in the short term.
IBM Austin is concerned with the design of multiprocessors. Jade has
collaborative links with Derek Williams, a lead engineer in Austin. As the
letter of support from Derek indicates, this proposal is of great relevance to
industries like IBM, which strongly suggests potential impact, should the
project be successful. Meeting regularly with Derek's team will allow us to
discuss our design choices, in particular on the models and semantics sides,
with them.
Microsoft has significant verification presence, through its
Cambridge, Redmond and Bangalore labs, which could possibly be impacted by the
project. As an example, Jade's PhD student was invited by Akash Lal (MSR
Bangalore) to do an internship this summer, following a pre-publication of Jade
with her Oxford colleagues on verifying concurrent software running on weak
memory.
We plan on interacting regularly with MSR researchers, through visits and phone
conference. This will be facilitated by the fact that Jade is a member of the
Programming Principles, Logic and Verification group at UCL, which has strong
connections to the Cambridge lab: Byron Cook is both professor in the same
group at UCL, and a researcher at MSR Cambridge.
Monoidics is a London-based SME that markets a program analysis
tool. As the letter of support from Cristiano Calcagno indicates, Monoidics is
very interested in verification in general, and an effective treatment of
concurrency in particular. The ability to meet with Cristiano's team will
allow us to discuss our design choices, in particular on the tool side.
The UK Government has made clear that they view cybersecurity as important,
from the Cabinet Office Cybersecurity Strategy document in 2009, through a
parliamentary briefing note ``Cybersecurity in the UK'' in 2011, to the
Cybersecurity Challenge launched in 2012.
Our engagement within the public sector will be facilitated by the presence of
the CyberSecurity institute as UCL, recognised by EPSRC and GCHQ at UCL. See
also the Host Organisation Statement.
We believe that this proposal is of particular relevance to the EPSRC thematic
area of ``Global Uncertainties'', in the core area ``Cyber
Security''. Within EPSRC's ICT theme, this proposal fits naturally within
three of the areas highlighted as growing in the portfolio, namely
``Programming Languages and Compilers'', ``Software
Engineering'', and ``Verification and Correctness''. Citing the
portfolio, ``the involvement of researchers working in this area in the
cross-ICT priorities, particularly the Many-core Architectures and Concurrency
in Distributed and Embedded Systems, is essential.''. Within this priority, we
believe our proposal to follow the line spelled in EPSRC's portfolio, of
``form[ing] the bridge between the abstraction layers of computing
systems.''
We highlight the practicality of our proposal, which we believe is crucial to
leading high-impact research in the area. This meets the following excerpt of
the portfolio: ``a lack of these implementation activities as part of
research proposals is holding back the development of the area, slowing
industrial uptake and impact, and threatening the continued strength of the
UK's position. [...] Growth in this area will be targeted towards research
that goes beyond early-stage proof-of-concept developments to include more
rigorous evaluations and validations, with the implementation work they
require.''
embedded devices to crash. Indeed, since these now routinely include multiple
cores, they rely on concurrent software for functioning.
This project will have impact on several communities: i) professional
programmers of concurrent software and ii) multiprocessors designers. Our
connections into the following companies constitute a way for the ideas to
impact industrial verification tools even in the short term.
IBM Austin is concerned with the design of multiprocessors. Jade has
collaborative links with Derek Williams, a lead engineer in Austin. As the
letter of support from Derek indicates, this proposal is of great relevance to
industries like IBM, which strongly suggests potential impact, should the
project be successful. Meeting regularly with Derek's team will allow us to
discuss our design choices, in particular on the models and semantics sides,
with them.
Microsoft has significant verification presence, through its
Cambridge, Redmond and Bangalore labs, which could possibly be impacted by the
project. As an example, Jade's PhD student was invited by Akash Lal (MSR
Bangalore) to do an internship this summer, following a pre-publication of Jade
with her Oxford colleagues on verifying concurrent software running on weak
memory.
We plan on interacting regularly with MSR researchers, through visits and phone
conference. This will be facilitated by the fact that Jade is a member of the
Programming Principles, Logic and Verification group at UCL, which has strong
connections to the Cambridge lab: Byron Cook is both professor in the same
group at UCL, and a researcher at MSR Cambridge.
Monoidics is a London-based SME that markets a program analysis
tool. As the letter of support from Cristiano Calcagno indicates, Monoidics is
very interested in verification in general, and an effective treatment of
concurrency in particular. The ability to meet with Cristiano's team will
allow us to discuss our design choices, in particular on the tool side.
The UK Government has made clear that they view cybersecurity as important,
from the Cabinet Office Cybersecurity Strategy document in 2009, through a
parliamentary briefing note ``Cybersecurity in the UK'' in 2011, to the
Cybersecurity Challenge launched in 2012.
Our engagement within the public sector will be facilitated by the presence of
the CyberSecurity institute as UCL, recognised by EPSRC and GCHQ at UCL. See
also the Host Organisation Statement.
We believe that this proposal is of particular relevance to the EPSRC thematic
area of ``Global Uncertainties'', in the core area ``Cyber
Security''. Within EPSRC's ICT theme, this proposal fits naturally within
three of the areas highlighted as growing in the portfolio, namely
``Programming Languages and Compilers'', ``Software
Engineering'', and ``Verification and Correctness''. Citing the
portfolio, ``the involvement of researchers working in this area in the
cross-ICT priorities, particularly the Many-core Architectures and Concurrency
in Distributed and Embedded Systems, is essential.''. Within this priority, we
believe our proposal to follow the line spelled in EPSRC's portfolio, of
``form[ing] the bridge between the abstraction layers of computing
systems.''
We highlight the practicality of our proposal, which we believe is crucial to
leading high-impact research in the area. This meets the following excerpt of
the portfolio: ``a lack of these implementation activities as part of
research proposals is holding back the development of the area, slowing
industrial uptake and impact, and threatening the continued strength of the
UK's position. [...] Growth in this area will be targeted towards research
that goes beyond early-stage proof-of-concept developments to include more
rigorous evaluations and validations, with the implementation work they
require.''
People |
ORCID iD |
| Jade Alglave (Principal Investigator) |
Publications
Alglave J
(2014)
Herding Cats Modelling, Simulation, Testing, and Data Mining for Weak Memory
in ACM Transactions on Programming Languages and Systems
Alglave J
(2014)
Computer Aided Verification
Alglave J
(2015)
GPU Concurrency Weak Behaviours and Programming Assumptions
in ACM SIGPLAN Notices
Lidbury C
(2015)
Many-core compiler fuzzing
| Description | I have developed extensions of my work on CPU chips that now apply to GPU chips and programming languages. These extensions have been instrumental during my visit to Nvidia during the summer of 2014 (see Secondments). Since 2015, I also have used my language (described in the paper Herding cats) to describe the standard defined by the HSA foundation (which comprises vendors such as AMD, ARM, Qualcomm, Samsung). Since 2017, my language is being used to describe official models such as the Linux kernel's, and ARMv8's. |
| Exploitation Route | Our findings are embodied in tools which are available on the web. Moreover we have already applied them successfully at Nvidia, with HSA, with Linux and ARM. |
| Sectors | Digital/Communication/Information Technologies (including Software),Education,Electronics,Energy,Environment,Manufacturing, including Industrial Biotechology |
| URL | http://www0.cs.ucl.ac.uk/staff/J.Alglave/ |
| Description | Since my PhD (awarded 2010) my research and tools have applied to products by IBM, and ARM amongst others. I spent the summer of 2014 at Nvidia Redmond and Santa Clara, directly applying the results of my research to their products. Together with colleagues, we developed a model for a future Nvidia chip. I since then wrote their documentation, which demonstrates an incredible impact: this whole line of work precisely started because the documentations for these chips were severely flawed. This shows that my line of research has reached the point where we are able to repair the flaws that initiated it. Similarly since end of 2015, I collaborate with the HSA consortium to model the GPU standard defined by them. Their official documentation features a core model written in my language, as well as an accompanying prose document written by me. We are since then working on extending the model to more advance features, in tandem with HSA. More recently, myself and others have produced the first official memory model of the Linux kernel, which has now been integrated to the kernel. Finally, following my help with formalising the official ARMv8 model, ARM has offered to host me for an indefinite period of time, as a secondment from my UCL position. |
| First Year Of Impact | 2010 |
| Sector | Digital/Communication/Information Technologies (including Software),Electronics |
| Impact Types | Economic |