Byron Cook, Satnam Singh, Ashutosh Gupta, Viktor Vafeiadis
Current C to gates synthesis tools do not support programs that make non-trivial use of dynamically-allocated heap (e.g. linked-list C programs that call malloc and free). The problem is that its...
Modular fine-grained concurrency verification (2009)
Traditionally, concurrent data structures are protected by a single mutual exclusion lock so that only one thread may access the data structure at any time. This coarse-grained approach makes it...
Proving That Non-Blocking Algorithms Don’t Block (2009)
Alexey Gotsman, Byron Cook, Matthew Parkinson, Viktor Vafeiadis
A concurrent data-structure implementation is considered nonblocking if it meets one of three following liveness criteria: waitfreedom, lock-freedom,orobstruction-freedom. Developers of nonblocking...
Deny-guarantee reasoning (2009)
Viktor Vafeiadis, Cambridge Cb Fd, Viktor Vafeiadis
ISSN 1476-2986Deny-guarantee reasoning (extended version and formalization in Isabelle) Rely-guarantee is a well-established approach to reasoning about concurrent programs that use parallel...
The Design of Distributed Programming Languages (2008)
Peter Sewell, John Billings, Steve Bishop, Matthew Fairbairn, Pierre Habouzit, Michael Hicks, ...
High-level programming languages For non-distributed, non-concurrent programming, they’re pretty good. We have ML (SML/OCaml), Haskell, Java, C#, with: • type safety • rich concrete types –...
Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, Viktor Vafeiadis
† INRIA Rocquencourt Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of...
Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, Viktor Vafeiadis
Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, Viktor Vafeiadis
Abstract Acute: High-Level Programming Language Design for Distributed Computation (2008)
Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, Viktor Vafeiadis
Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...
For Distributed Computation, Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, ...
Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...
Acute: High-Level Programming Language Design (2008)
For Distributed Computation, Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, ...
Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...
A marriage of rely/guarantee and separation logic (2007)
C Viktor Vafeiadis, Viktor Vafeiadis, Viktor Vafeiadis, Matthew Parkinson, Matthew Parkinson, Matthew Parkinson
A marriage of rely/guarantee
Modular safety checking for fine-grained concurrency (2007)
Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis
Abstract. Concurrent programs are difficult to verify because the proof must consider the interactions between the threads. Fine-grained concurrency and heap allocated data structures exacerbate this...
A marriage of rely/guarantee and separation logic (2007)
Viktor Vafeiadis, Matthew Parkinson
Abstract. In the quest for tractable methods for reasoning about concurrent algorithms both rely/guarantee logic and separation logic have made great advances. They both seek to tame, or control, the...
A Marriage of Rely/Guarantee and Separation (2007)
Logic Viktor Vafeiadis, Viktor Vafeiadis, Matthew Parkinson
In the quest for modular reasoning about shared-variable concurrent algorithms, two alternatives have emerged: rely/guarantee logic and separation logic. The former is very good at describing...
Modular safety checking for fine-grained concurrency (2007)
Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis
Abstract. Concurrent programs are difficult to verify because the proof must consider the interactions between the threads. Fine-grained concurrency and heap allocated data structures exacerbate this...
Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro, Viktor Vafeiadis, Maurice Herlihy, ...
A safety proof of a lazy concurrent list-based set implementation
Proving correctness of highlyconcurrent linearisable objects (2006)
We study a family of implementations for linked lists using finegrain synchronisation. This approach enables greater concurrency, but correctness is a greater challenge than for classical,...
Proving correctness of highlyconcurrent linearisable objects (2006)
We study a family of implementations for linked lists using finegrain synchronisation. This approach enables greater concurrency, but correctness is a greater challenge than for classical,...
Proving Correctness of Highly-Concurrent Linearisable Objects (2005)
Vafeiadis, Viktor, Herlihy, Maurice, Hoare, Tony, Shapiro, Marc
We study a family of implementations for linked lists using fine-grain synchronisation. This approach enables greater concurrency, but correctness is a greater challenge than for classical,...
Acute: high-level programming language design for distributed computation (2005)
Sewell, Peter, Leifer, James J., Wansbrough, Keith, Zappa Nardelli, Francesco, Allen-Williams, Mair, Habouzit, Pierre, ...
Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...
Acute: high-level programming language design for distributed computation (2005)
Sewell, Peter, Leifer, James J., Wansbrough, Keith, Zappa Nardelli, Francesco, Allen-Williams, Mair, Habouzit, Pierre, ...
Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...
Proving Correctness of Highly-Concurrent Linearisable Objects (2005)
Vafeiadis, Viktor, Herlihy, Maurice, Hoare, Tony, Shapiro, Marc
We study a family of implementations for linked lists using fine-grain synchronisation. This approach enables greater concurrency, but correctness is a greater challenge than for classical,...
Proving Correctness of Highly-Concurrent Linearisable Objects (2005)
Vafeiadis, Viktor, Herlihy, Maurice, Hoare, Tony, Shapiro, Marc
We study a family of implementations for linked lists using fine-grain synchronisation. This approach enables greater concurrency, but correctness is a greater challenge than for classical,...
Acute: high-level programming language design for distributed computation (2005)
Sewell, Peter, Leifer, James J., Wansbrough, Keith, Zappa Nardelli, Francesco, Allen-Williams, Mair, Habouzit, Pierre, ...
Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...
1 Introduction First Year Report (2005)
My initial project proposal was to enhance program safety by improving module
Sewell, Peter, Leifer, James J., Wansbrough, Keith, Allen-Williams, Mair, Zappa Nardelli, Francesco, Habouzit, Pierre, ...
This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have defined and implemented....
Sewell, Peter, Leifer, James J., Wansbrough, Keith, Allen-Williams, Mair, Zappa Nardelli, Francesco, Habouzit, Pierre, ...
This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have defined and implemented....
Sewell, Peter, Leifer, James J., Wansbrough, Keith, Allen-Williams, Mair, Zappa Nardelli, Francesco, Habouzit, Pierre, ...
This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have defined and implemented....
Acute: High-level programming language design for distributed computation (2004)
Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-williams, Pierre Habouzit, Viktor Vafeiadis
Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct...
Number Computer Laboratory, C Peter Sewell, Viktor Vafeiadis, Viktor Vafeiadis, Peter Sewell, Peter Sewell, ...
This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have defined and implemented.