Colloquium
Jade Alglave
University College London
Thursday May 2, 2013
3147 MEB
Refreshments 1:50 p.m.
Lecture 2:00 p.m.
Title: First steps in verifying concurrent programs running on weak memory
Jade Alglave
University College London
Thursday May 2, 2013
3147 MEB
Refreshments 1:50 p.m.
Lecture 2:00 p.m.
Title: First steps in verifying concurrent programs running on weak memory
Abstract
Multiprocessors are now so wide-spread that verification cannot ignore any longer the flavour of concurrency that they implement. Contrary to what most formal verification works assume, the execution model for concurrent programs is not Lamport's Sequential Consistency (SC), where an execution of a program corresponds to an interleaving of the instructions of the program.
Rather, multiprocessors such as Intel x86, IBM PowerPC and ARM implement weak memory models, which feature instruction reordering, store buffering and caching scenarios. In this talk, I would first present the formal models that we developed to describe the executions of concurrent programs on weak memory. I would then present two different ways of performing verification of concurrent software running on weak memory.
In the first one, we developed a method that allows us to perform weak memory verification using an SC verification tool. To do so, rather than rewriting a verification tool to make it weak memory aware, we modify its input. Given a program, we transform it into another program such that the SC executions of the new program are the weak executions of the original one. Then we give the new program as input to an SC verification tool: the bugs and proofs that the tool finds apply to weak memory.
In the second one, we take a more radical approach. We get rid of the notion of interleavings, or total orders, to describe executions. Rather, we see the executions of concurrent programs as partial orders. First, this is closer to the style adopted by several hardware vendors in their documentations (the most obvious being Sun and Alpha), and to the formal models we developed. Second, our experiments show that (in the context of bounded model-checking for now) this choice of representation leads to efficient verification: we were able to analyse relatively big fragments of the data-base software PostgreSQL, of the server software Apache, and of the Read-Copy-Update synchronisation mechanism of the Linux kernel.
Return to 2013 Events Calendar
Multiprocessors are now so wide-spread that verification cannot ignore any longer the flavour of concurrency that they implement. Contrary to what most formal verification works assume, the execution model for concurrent programs is not Lamport's Sequential Consistency (SC), where an execution of a program corresponds to an interleaving of the instructions of the program.
Rather, multiprocessors such as Intel x86, IBM PowerPC and ARM implement weak memory models, which feature instruction reordering, store buffering and caching scenarios. In this talk, I would first present the formal models that we developed to describe the executions of concurrent programs on weak memory. I would then present two different ways of performing verification of concurrent software running on weak memory.
In the first one, we developed a method that allows us to perform weak memory verification using an SC verification tool. To do so, rather than rewriting a verification tool to make it weak memory aware, we modify its input. Given a program, we transform it into another program such that the SC executions of the new program are the weak executions of the original one. Then we give the new program as input to an SC verification tool: the bugs and proofs that the tool finds apply to weak memory.
In the second one, we take a more radical approach. We get rid of the notion of interleavings, or total orders, to describe executions. Rather, we see the executions of concurrent programs as partial orders. First, this is closer to the style adopted by several hardware vendors in their documentations (the most obvious being Sun and Alpha), and to the formal models we developed. Second, our experiments show that (in the context of bounded model-checking for now) this choice of representation leads to efficient verification: we were able to analyse relatively big fragments of the data-base software PostgreSQL, of the server software Apache, and of the Read-Copy-Update synchronisation mechanism of the Linux kernel.
Return to 2013 Events Calendar