Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8, Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell, July 2017. Draft. [ bib | project page | pdf ]
ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits. In particular, the model was originally non-multicopy-atomic: writes could become visible to some other threads before becoming visible to all --- but this has not been exploited in production implementations, the corresponding potential hardware optimisations are thought to have insufficient benefits in the ARM context, and it gives rise to subtle complications when combined with other ARMv8 features. The ARMv8 architecture has therefore been revised: it now has a multicopy-atomic model. It has also been simplified in other respects, including more straightforward notions of dependency, and the architecture now includes a formal concurrency model.

In this paper we detail these changes and discuss their motivation. We define two formal concurrency models: an operational one, simplifying the Flowing model of Flur et al., and the axiomatic model of the revised ARMv8 specification. The models were developed by an academic group and by ARM staff, respectively, and this extended collaboration partly motivated the above changes. We prove the equivalence of the two models. The operational model is integrated into an executable exploration tool with new web interface, demonstrated by exhaustively checking the possible behaviours of a loop-unrolled version of a Linux kernel lock implementation, a previously known bug due to unprevented speculation, and a fixed version.

 
Engineering with Logic: Rigorous Specification and Validation for TCP/IP and the Sockets API, Steve Bishop, Matthew Fairbairn, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough, February 2017. Draft. [ bib | project page | pdf ]
 
Mixed-size Concurrency: ARM, POWER, C/C++11, and SC. Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. In POPL 2017. [ bib | doi | project page | pdf ]
Previous work on the semantics of relaxed shared-memory concurrency has only considered the case in which each load reads the data of exactly one store. In practice, however, multiprocessors support mixed-size accesses, and these are used by systems software and (to some degree) exposed at the C/C++ language level. A semantic foundation for software, therefore, has to address them.

We investigate the mixed-size behaviour of ARMv8 and IBM POWER architectures and implementations: by experiment, by developing semantic models, by testing the correspondence between these, and by discussion with ARM and IBM staff. This turns out to be surprisingly subtle, and on the way we have to revisit the fundamental concepts of coherence and sequential consistency, which change in this setting. In particular, we show that adding a memory barrier between each instruction does not restore sequential consistency. We go on to extend the C/C++11 model to support non-atomic mixed-size memory accesses.

This is a necessary step towards semantics for real-world shared-memory concurrent code, beyond litmus tests.

 
The missing link: explaining ELF static linking, semantically. Stephen Kell, Dominic P. Mulligan, and Peter Sewell. In OOPSLA 2016. [ bib | doi | project page | pdf | http ]
Beneath the surface, software usually depends on complex linker behaviour to work as intended. Even linking hello_world.c is surprisingly involved, and systems software such as libc and operating system kernels rely on a host of linker features. But linking is poorly understood by working programmers and has largely been neglected by language researchers.

In this paper we survey the many use-cases that linkers support and the poorly specified linker speak by which they are controlled: metadata in object files, command-line options, and linker-script language. We provide the first validated formalisation of a realistic executable and linkable format (ELF), and capture aspects of the Application Binary Interfaces for four mainstream platforms (AArch64, AMD64, Power64, and IA32). Using these, we develop an executable specification of static linking, covering (among other things) enough to link small C programs (we use the example of bzip2) into a correctly running executable. We provide our specification in Lem and Isabelle/HOL forms. This is the first formal specification of mainstream linking. We have used the Isabelle/HOL version to prove a sample correctness property for one case of AMD64 ABI relocation, demonstrating that the specification supports formal proof, and as a first step towards the much more ambitious goal of verified linking. Our work should enable several novel strands of research, including linker-aware verified compilation and program analysis, and better languages for controlling linking.

 
An operational semantics for C/C++11 concurrency. Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell. In OOPSLA 2016. [ bib | doi | pdf | http ]
The C/C++11 concurrency model balances two goals: it is relaxed enough to be efficiently implementable and (leaving aside the “thin-air” problem) it is strong enough to give useful guarantees to programmers. It is mathematically precise and has been used in verification research and compiler testing. However, the model is expressed in an axiomatic style, as predicates on complete candidate executions. This suffices for computing the set of allowed executions of a small litmus test, but it does not directly support the incremental construction of executions of larger programs. It is also at odds with conventional operational semantics, as used implicitly in the rest of the C/C++ standards.

Our main contribution is the development of an operational model for C/C++11 concurrency. This covers all the features of the previous formalised axiomatic model, and we have a mechanised proof that the two are equivalent, in Isabelle/HOL. We also integrate this semantics with an operational semantics for sequential C (described elsewhere); the combined semantics can incrementally execute programs in a small fragment of C.

Doing this uncovered several new aspects of the C/C++11 model: we show that one cannot build an equivalent operational model that simply follows program order, sequential consistent order, or the synchronises-with order. The first negative result is forced by hardware-observable behaviour, but the latter two are not, and so might be ameliorated by changing C/C++11. More generally, we hope that this work, with its focus on incremental construction of executions, will inform the future design of new concurrency models.

 
Clarifying Unspecified Values, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2089, http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2089.htm, September 2016. [ bib | project page | html ]
 
Clarifying Pointer Provenance, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2090, http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2090.htm, September 2016. [ bib | project page | html ]
 
Clarifying Trap Representations, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2091, http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2091.htm, September 2016. [ bib | project page | html ]
 
Into the depths of C: elaborating the de facto standards. Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N.M. Watson, and Peter Sewell. In PLDI 2016, PLDI 2016 Distinguished Paper award. [ bib | doi | project page | pdf | http ]
C remains central to our computing infrastructure. It is notionally defined by ISO standards, but in reality the properties of C assumed by systems code and those implemented by compilers have diverged, both from the ISO standards and from each other, and none of these are clearly understood.

We make two contributions to help improve this error-prone situation. First, we describe an in-depth analysis of the design space for the semantics of pointers and memory in C as it is used in practice. We articulate many specific questions, build a suite of semantic test cases, gather experimental data from multiple implementations, and survey what C experts believe about the de facto standards. We identify questions where there is a consensus (either following ISO or differing) and where there are conflicts. We apply all this to an experimental C implemented above capability hardware. Second, we describe a formal model, Cerberus, for large parts of C. Cerberus is parameterised on its memory model; it is linkable either with a candidate de facto memory object model, under construction, or with an operational C11 concurrency model; it is defined by elaboration to a much simpler Core language for accessibility, and it is executable as a test oracle on small examples.

This should provide a solid basis for discussion of what mainstream C is now: what programmers and analysis tools can assume and what compilers aim to implement. Ultimately we hope it will be a step towards clear, consistent, and accepted semantics for the various use-cases of C.

 
Clarifying the C memory object model, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2012, http://www.cl.cam.ac.uk/~pes20/cerberus/notes64-wg14.html, March 2016. [ bib | project page | html ]
 
C memory object and value semantics: the space of de facto and ISO standards, David Chisnall, Justus Matthiesen, Kayvan Memarian, Kyndylan Nienhuis, Peter Sewell, and Robert N. M. Watson. ISO SC22 WG14 N2013, http://www.cl.cam.ac.uk/~pes20/cerberus/notes30.pdf, March 2016. [ bib | project page | pdf ]
 
What is C in practice? (Cerberus survey v2): Analysis of Responses, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2014, http://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html, March 2016. [ bib | project page | html ]
 
What is C in practice? (Cerberus survey v2): Analysis of Responses -- with Comments, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2015, http://www.cl.cam.ac.uk/~pes20/cerberus/analysis-2016-02-05-anon.txt, March 2016. [ bib | project page | txt ]
 
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. Jean Pichon-Pharabod and Peter Sewell. In POPL 2016. [ bib | doi | project page | pdf ]
Despite much research on concurrent programming languages, especially for Java and C/C++, we still do not have a satisfactory definition of their semantics, one that admits all common optimisations without also admitting undesired behaviour. Especially problematic are the “thin-air” examples involving high-performance concurrent accesses, such as C/C++11 relaxed atomics. The C/C++11 model is in a per-candidate-execution style, and previous work has identified a tension between that and the fact that compiler optimisations do not operate over single candidate executions in isolation; rather, they operate over syntactic representations that represent all executions.

In this paper we propose a novel approach that circumvents this difficulty. We define a concurrency semantics for a core calculus, including relaxed-atomic and non-atomic accesses, and locks, that admits a wide range of optimisation while still forbidding the classic thin-air examples. It also addresses other problems relating to undefined behaviour.

The basic idea is to use an event-structure representation of the current state of each thread, capturing all of its potential executions, and to permit interleaving of execution and transformation steps over that to reflect optimisation (possibly dynamic) of the code. These are combined with a non-multi-copy-atomic storage subsystem, to reflect common hardware behaviour.

The semantics is defined in a mechanised and executable form, and designed to be implementable above current relaxed hardware and strong enough to support the programming idioms that C/C++11 does for this fragment. It offers a potential way forward for concurrent programming language semantics, beyond the current C/C++11 and Java models.

 
Modelling the ARMv8 architecture, operationally: concurrency and ISA. Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. In POPL 2016. [ bib | doi | project page | pdf ]
In this paper we develop semantics for key aspects of the ARMv8 multiprocessor architecture: the concurrency model and much of the 64-bit application-level instruction set (ISA). Our goal is to clarify what the range of architecturally allowable behaviour is, and thereby to support future work on formal verification, analysis, and testing of concurrent ARM software and hardware.

Establishing such models with high confidence is intrinsically difficult: it involves capturing the vendor's architectural intent, aspects of which (especially for concurrency) have not previously been precisely defined. We therefore first develop a concurrency model with a microarchitectural flavour, abstracting from many hardware implementation concerns but still close to hardware-designer intuition. This means it can be discussed in detail with ARM architects. We then develop a more abstract model, better suited for use as an architectural specification, which we prove sound w.r.t. the first.

The instruction semantics involves further difficulties, handling the mass of detail and the subtle intensional information required to interface to the concurrency model. We have a novel ISA description language, with a lightweight dependent type system, letting us do both with a rather direct representation of the ARM reference manual instruction descriptions.

We build a tool from the combined semantics that lets one explore, either interactively or exhaustively, the full range of architecturally allowed behaviour, for litmus tests and (small) ELF executables. We prove correctness of some optimisations needed for tool performance.

We validate the models by discussion with ARM staff, and by comparison against ARM hardware behaviour, for ISA single- instruction tests and concurrent litmus tests.

 
The Sail instruction-set semantics specification language, Kathryn E. Gray, Peter Sewell, Christopher Pulte, Shaked Flur, and Robert Norton-Wright, 2016. http://www.cl.cam.ac.uk/~pes20/sail/. [ bib | http ]
 
An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors . Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell. In MICRO 2015. [ bib | doi | pdf ]
Weakly consistent multiprocessors such as ARM and IBM POWER have been with us for decades, but their subtle programmer-visible concurrency behaviour remains challenging, both to implement and to use; the traditional architecture documentation, with its mix of prose and pseudocode, leaves much unclear.

In this paper we show how a precise architectural envelope model for such architectures can be defined, taking IBM POWER as our example. Our model specifies, for an arbitrary test program, the set of all its allowable executions, not just those of some particular implementation. The model integrates an operational concurrency model with an ISA model for the fixed-point non-vector user-mode instruction set (largely automatically derived from the vendor pseudocode, and expressed in a new ISA description language). The key question is the interface between these two: allowing all the required concurrency behaviour, without overcommitting to some particular microarchitectural implementation, requires a novel abstract structure.

Our model is expressed in a mathematically rigorous language that can be automatically translated to an executable test-oracle tool; this lets one either interactively explore or exhaustively compute the set of all allowed behaviours of intricate test cases, to provide a reference for hardware and software development.

 
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems. Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, and Peter Sewell. In SOSP 2015. [ bib | doi | project page | pdf ]
Systems depend critically on the behaviour of file systems, but that behaviour differs in many details, both between implementations and between each implementation and the POSIX (and other) prose specifications. Building robust and portable software requires understanding these details and differences, but there is currently no good way to systematically describe, investigate, or test file system behaviour across this complex multi-platform interface.

In this paper we show how to characterise the envelope of allowed behaviour of file systems in a form that enables practical and highly discriminating testing. We give a mathematically rigorous model of file system behaviour, SibylFS, that specifies the range of allowed behaviours of a file system for any sequence of the system calls within our scope, and that can be used as a test oracle to decide whether an observed trace is allowed by the model, both for validating the model and for testing file systems against it. SibylFS is modular enough to not only describe POSIX, but also specific Linux, OSX and FreeBSD behaviours. We complement the model with an extensive test suite of over 21000 tests; this can be run on a target file system and checked in less than 5 minutes, making it usable in practice. Finally, we report experimental results for around 40 configurations of many file systems, identifying many differences and some serious flaws.

 
Not-Quite-So-Broken TLS: Lessons in Re-Engineering a Security Protocol Specification and Implementation. David Kaloper-Mersinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell. In USENIX Security 2015. [ bib | project page | pdf | http ]
Transport Layer Security (TLS) implementations have a history of security flaws. The immediate causes of these are often programming errors, e.g. in memory management, but the root causes are more fundamental: the challenges of interpreting the ambiguous prose specification, the complexities inherent in large APIs and code bases, inherently unsafe programming choices, and the impossibility of directly testing conformance between implementations and the specification.

We present nqsb-TLS, the result of our re-engineered approach to security protocol specification and implementation that addresses these root causes. The same code serves dual roles: it is both a specification of TLS, executable as a test oracle to check conformance of traces from arbitrary implementations, and a usable implementation of TLS; a modular and declarative programming style provides clean separation between its components. Many security flaws are thus excluded by construction.

nqsb-TLS can be used in standalone applications, which we demonstrate with a messaging client, and can also be compiled into a Xen unikernel (a specialised virtual machine image) with a TCB that is 4% of a standalone system running a standard Linux/OpenSSL stack, with all network traffic being handled in a memory-safe language; this supports applications including HTTPS, IMAP, Git, and Websocket clients and servers.

 
Rigorous Architectural Modelling for Production Multiprocessors, S. Flur, K. Gray, G. Kerneis, D. Mulligan, C. Pulte, S. Sarkar, and P. Sewell, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference. [ bib ]
Processor architectures are critical interfaces in computing, but they are typically defined only by prose and pseudocode documentation. This is especially problematic for the subtle concurrency behaviour of weakly consistent multiprocessors such as ARM and IBM POWER: the traditional documentation does not define precisely what programmer-observable behaviour is (and is not) allowed for concurrent code; it is not executable as a test oracle for pre-Silicon or post-Silicon hardware testing; it is not executable as an emulator for software testing; and it is not mathematically rigorous enough to serve as a foundation for software verification.

We present a rigorous architectural envelope model for IBM POWER multiprocessors, and similar work in progress for ARM, that aims to support all of these for small-but-intricate test cases, integrating an operational concurrency model with an ISA model for the sequential behaviour of a substantial fragment of the user-mode instruction set (largely automatically derived from the vendor pseudocode, and expressed in a new ISA description language). The key question is the interface between these two: we have to allow all the required relaxed-memory behaviour, without overcommitting to some particular microarchitectural model. Our models can be automatically translated into executable code, which, combined with front-ends for concurrency litmus tests and ELF executables, can interactively or exhaustively explore all the allowed behaviours of small test cases.

 
Cerberus: towards an Executable Semantics for Sequential and Concurrent C11, Kayvan Memarian, Kyndylan Nienhuis, Justus Matthiesen, James Lingard, and Peter Sewell, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference. [ bib | project page ]
C remains central to our computing infrastructure but still lacks a clear and complete semantics. Programmers lack tools to explore the range of behaviours they should expect; compiler development lacks test oracles; and formal verification and analysis must make (explicitly or implicitly) many choices about the specific C they target.

We describe Cerberus, a semantics for a substantial fragment of C11. Its thread-local semantics is factored via an elaboration into a simpler Core language, to make it conceptually and mathematically tractable. This is integrated with an operational model for C11 concurrency, with a mechanised proof of equivalence to the axiomatic C11 model of Batty et al. The front-end includes a parser that closely follows the C11 standard grammar and a typechecker. Cerberus is executable, to explore all behaviours or single paths of test programs, and it supports proof, as shown by a preliminary experiment in translation validation for the front-end of Clang, for very simple programs. This is a step towards a clear, consistent, and unambiguous semantics for C.

 
Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation, David Kaloper Meršinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference. [ bib | project page ]
Transport Layer Security (TLS) implementations have a history of security flaws. The immediate causes of these range from simple programming errors, such as memory management, to subtle violations of the protocol logic. Deeper causes can be seen in the challenges of interpreting the ambiguous prose specification, the complexities inherent in large APIs and code bases, unsafe performance-oriented programming choices, and the impossibility of directly testing conformance between implementations and the specification.

We present nqsb-TLS, the result of our re-engineering approach to improve the quality of security protocol implementations. The same code serves dual roles: it is both a specification of TLS, executable as a test oracle to check conformance of traces from arbitrary implementations, and a secure and usable executable implementation of TLS. nqsb-TLS employs a modular and declarative programming style that also allows it to be compiled into a Xen unikernel (a specialised virtual machine image) with a TCB that is 2.5% of a standalone system running a standard Linux/OpenSSL stack, with all network traffic being handled in a memory-safe language.

nqsb-TLS focuses on protocol-level interoperability, and makes no effort to be compatible with existing (and often poorly designed) library APIs such as OpenSSL. The higher-level API in nqsb-TLS makes it harder to misuse the library, and is demonstrated via several unikernel applications ranging over HTTPS, IMAP, Git, Websocket clients and servers.

 
The Problem of Programming Language Concurrency Semantics. Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. In ESOP 2015. [ bib | doi | pdf ]
Despite decades of research, we do not have a satisfactory concurrency semantics for any general-purpose programming language that aims to support concurrent systems code. The Java Memory Model has been shown to be unsound with respect to standard compiler optimisations, while the C/C++11 model is too weak, admitting undesirable thin-air executions. Our goal in this paper is to articulate this major open problem as clearly as is currently possible, showing how it arises from the combination of multiprocessor relaxed-memory behaviour and the desire to accommodate current compiler optimisations. We make several novel contributions that each shed some light on the problem, constraining the possible solutions and identifying new difficulties.

 
Lem: Reusable Engineering of Real-world Semantics. Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. In ICFP 2014. [ bib | doi | project page | pdf ]
Recent years have seen remarkable successes in rigorous engineering: using mathematically rigorous semantic models (not just idealised calculi) of real-world processors, programming languages, protocols, and security mechanisms, for testing, proof, analysis, and design. Building these models is challenging, requiring experimentation, dialogue with vendors or standards bodies, and validation; their scale adds engineering issues akin to those of programming to the task of writing clear and usable mathematics. But language and tool support for specification is lacking. Proof assistants can be used but bring their own difficulties, and a model produced in one, perhaps requiring many person-years effort and maintained over an extended period, cannot be used by those familiar with another.

We introduce Lem, a language for engineering reusable large-scale semantic models. The Lem design takes inspiration both from functional programming languages and from proof assistants, and Lem definitions are translatable into OCaml for testing, Coq, HOL4, and Isabelle/HOL for proof, and LaTeX and HTML for presentation. This requires a delicate balance of expressiveness, careful library design, and implementation of transformations - akin to compilation, but subject to the constraint of producing usable and human-readable code for each target. Lem's effectiveness is demonstrated by its use in practice.

 
POPL 2014 Program Chair's Report. Peter Sewell. SIGPLAN Notices, 49(4):10--26, July 2014. [ bib | doi | pdf ]
This note describes the POPL 2014 paper selection process and its rationale.

 
Lem, Dominic Mulligan, Thomas Tuerk, Scott Owens, Kathryn E. Gray, and Peter Sewell, 2014. http://www.cl.cam.ac.uk/~pes20/lem/. [ bib | project page | http ]
 
Principles of POPL. Derek Dreyer, John Field, Roberto Giacobazzi, Michael Hicks, Suresh Jagannathan, Mooly Sagiv, Peter Sewell, and Phil Wadler. SIGPLAN Notices, 48(4S):12--16, July 2013. [ bib | doi ]
 
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. J. ACM, 60(3):22:1--22:50, June 2013. [ bib | doi | project page | pdf ]
In this article, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation on x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behavior of the hardware, the effects of compiler optimization on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified compilation both essential and challenging.

We describe ClightTSO, a concurrent extension of CompCert’s Clight in which the TSO-based memory model of x86 multiprocessors is exposed for high-performance code, and CompCertTSO, a formally verified compiler from ClightTSO to x86 assembly language, building on CompCert. CompCertTSO is verified in Coq: for any well-behaved and successfully compiled ClightTSO source program, any permitted observable behavior of the generated assembly code (if it does not run out of memory) is also possible in the source semantics. We also describe some verified fence-elimination optimizations, integrated into CompCertTSO.

 
A Tutorial Introduction to the ARM and POWER Relaxed Memory Models, Luc Maranget, Susmit Sarkar, and Peter Sewell., October 2012. Draft. [ bib | pdf ]
ARM and IBM POWER multiprocessors have highly relaxed memory models: they make use of a range of hardware optimisations that do not affect the observable behaviour of sequential code but which are exposed to concurrent programmers, and concurrent code may not execute in the way one intends unless sufficient synchronisation, in the form of barriers, dependencies, and load-reserve/store-conditional pairs, is present. In this tutorial we explain some of the main issues that programmers should be aware of, by example. The material is based on extensive experimental testing, discussion with some of the designers, and formal models that aim to capture the architectural intent (though we do not speak for the vendors). To keep this tutorial as accessible as possible, we refer to our previous work for those details.

 
Fences in Weak Memory Models (Extended Version) . Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. Formal Methods in System Design, 40(2):170--205, April 2012. [ bib | doi | pdf ]
We present a class of relaxed memory models, defined in Coq, parameterised by the chosen permitted local reorderings of reads and writes, and by the visibility of inter- and intra-processor communications through memory (e.g. store atomicity relaxation). We prove results on the required behaviour and placement of memory fences to restore a given model (such as Sequential Consistency) from a weaker one. Based on this class of models we develop a tool, diy, that systematically and automatically generates and runs litmus tests. These tests can be used to explore the behaviour of processor implementations and the behaviour of models, and hence to compare the two against each other. We detail the results of experiments on Power and a model we base on them.

 
An Axiomatic Memory Model for POWER Multiprocessors. Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. In CAV 2012. [ bib | doi | pdf ]
The growing complexity of hardware optimizations employed by multiprocessors leads to subtle distinctions among allowed and disallowed behaviors, posing challenges in specifying their memory models formally and accurately, and in understanding and analyzing the behavior of concurrent software. This complexity is particularly evident in the IBM Power Architecture, for which a faithful specification was published only in 2011 using an operational style. In this paper we present an equivalent axiomatic specification, which is more abstract and concise. Although not officially sanctioned by the vendor, our results indicate that this axiomatic specification provides a reasonable basis for reasoning about current IBM POWER multiprocessors. We establish the equivalence of the axiomatic and operational specifications using both manual proof and extensive testing. To demonstrate that the constraint-based style of axiomatic specification is more amenable to computer-aided verification, we develop a SAT-based tool for evaluating possible outcomes of multi-threaded test programs, and we show that this tool is significantly more efficient than a tool based on an operational specification.

 
Synchronising C/C++ and POWER. Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams. In PLDI 2012. [ bib | doi | project page | errata | pdf ]
Shared memory concurrency relies on synchronisation primitives: compare-and-swap, load-reserve/store-conditional (aka LL/SC), language-level mutexes, and so on. In a sequentially consistent setting, or even in the TSO setting of x86 and Sparc, these have well-understood semantics. But in the very relaxed settings of IBM, POWER, ARM, or C/C++, it remains surprisingly unclear exactly what the programmer can depend on.

This paper studies relaxed-memory synchronisation. On the hardware side, we give a clear semantic characterisation of the load-reserve/store-conditional primitives as provided by POWER multiprocessors, for the first time since they were introduced 20 years ago; we cover their interaction with relaxed loads, stores, barriers, and dependencies. Our model, while not officially sanctioned by the vendor, is validated by extensive testing, comparing actual implementation behaviour against an oracle generated from the model, and by detailed discussion with IBM staff. We believe the ARM semantics to be similar.

On the software side, we prove sound a proposed compilation scheme of the C/C++ synchronisation constructs to POWER, including C/C++ spinlock mutexes, fences, and read-modify-write operations, together with the simpler atomic operations for which soundness is already known from our previous work; this is a first step in verifying concurrent algorithms that use load-reserve/store-conditional with respect to a realistic semantics. We also build confidence in the C/C++ model in its own terms, fixing some omissions and contributing to the C standards committee adoption of the C++11 concurrency model.

 
Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER. Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, and Peter Sewell. In POPL 2012. [ bib | doi | project page | errata | pdf ]
The upcoming C and C++ revised standards add concurrency to the languages, for the first time, in the form of a subtle *relaxed memory model* (the *C++11 model*). This aims to permit compiler optimisation and to accommodate the differing relaxed-memory behaviours of mainstream multiprocessors, combining simple semantics for most code with high-performance *low-level atomics* for concurrency libraries. In this paper, we first establish two simpler but provably equivalent models for C++11, one for the full language and another for the subset without consume operations. Subsetting further to the fragment without low-level atomics, we identify a subtlety arising from atomic initialisation and prove that, under an additional condition, the model is equivalent to sequential consistency for race-free programs.

We then prove our main result, the correctness of two proposed compilation schemes for the C++11 load and store concurrency primitives to Power assembly, having noted that an earlier proposal was flawed. (The main ideas apply also to ARM, which has a similar relaxed memory architecture.)

This should inform the ongoing development of production compilers for C++11 and C1x, clarifies what properties of the machine architecture are required, and builds confidence in the C++11 and Power semantics.

 
False Concurrency and Strange-but-true Machines . Peter Sewell. In CONCUR 2012, Invited talk abstract. [ bib | doi | pdf ]
Concurrency theory and real-world multiprocessors have developed in parallel for the last 50 years, from their beginnings in the mid 1960s. Both have been very productive: concurrency theory has given us a host of models, calculi, and proof techniques, while engineered multiprocessors are now ubiquitous, from 2-8 core smartphones and laptops through to servers with 1024 or more hardware threads. But the fields have scarcely communicated, and the shared-memory interaction primitives offered by those mainstream multiprocessors are very different from the theoretical models that have been heavily studied.

 
Tales from the Jungle. Peter Sewell. In ICFP 2012, Invited talk abstract. [ bib | doi ]
We rely on a computational infrastructure that is a densely interwined mass of software and hardware: programming languages, network protocols, operating systems, and processors. It has accumulated great complexity, from a combination of engineering design decisions, contingent historical choices, and sheer scale, yet it is defined at best by prose specifications, or, all too often, just by the common implementations. Can we do better? More specifically, can we apply rigorous methods to this mainstream infrastructure, taking the accumulated complexity seriously, and if we do, does it help? My colleagues and I have looked at these questions in several contexts: the TCP/IP network protocols with their Sockets API; programming language design, including the Java module system and the C11/C++11 concurrency model; the hardware concurrency behaviour of x86, IBM POWER, and ARM multiprocessors; and compilation of concurrent code.

In this talk I will draw some lessons from what did and did not succeed, looking especially at the empirical nature of some of the work, at the social process of engagement with the various different communities, and at the mathematical and software tools we used. Domain-specific modelling languages (based on functional programming ideas) and proof assistants were invaluable for working with the large and loose specifications involved: idioms within HOL4 for TCP, our Ott tool for programming language specification, and Owens's Lem tool for portable semantic definitions, with HOL4, Isabelle, and Coq, for the relaxed-memory concurrency semantics work. Our experience with these suggests something of what is needed to make full-scale rigorous semantics a commonplace reality.

 
CompCert-TSO release, Version 1.12, Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell, August 2011. http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/index.html. [ bib | project page | .html ]
 
Ott release, version 0.20.3, Peter Sewell and Francesco Zappa Nardelli, August 2011. http://www.cl.cam.ac.uk/~pes20/ott/. [ bib | project page | http ]
 
Fundamentals of Computing Research: a perspective from the ground, Peter Sewell, February 2011. Briefing note for EPSRC ICT team, with input from Anuj Dawar, Chris Hankin, Tom Melham, Faron Moller, Peter O'Hearn, and Phil Wadler. 6pp. [ bib ]
 
Responses to FoC Questions, Peter O'Hearn, February 2011. Briefing note for EPSRC ICT team, with contributions and input from Anuj Dawar, Philippa Gardner, Chris Hankin, Tom Melham, Faron Moller, Andrew Pitts, Uday Reddy, Peter Sewell, and Philip Wadler. 11pp. [ bib ]
 
Lem: A Lightweight Tool for Heavyweight Semantics. Scott Owens, Peter Böhm, Francesco Zappa Nardelli, and Peter Sewell. In ITP 2011, (Rough Diamond) 7pp. [ bib | doi | project page | http ]
 
Understanding POWER Multiprocessors. Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. In PLDI 2011. [ bib | doi | project page | pdf ]
Exploiting today's multiprocessors requires high-performance and correct concurrent systems code (optimising compilers, language runtimes, OS kernels, etc.), which in turn requires a good understanding of the observable processor behaviour that can be relied on. Unfortunately this critical hardware/software interface is not at all clear for several current multiprocessors.

In this paper we characterise the behaviour of IBM POWER multiprocessors, which have a subtle and highly relaxed memory model (ARM multiprocessors have a very similar architecture in this respect). We have conducted extensive experiments on several generations of processors: POWER G5, 5, 6, and 7. Based on these, on published details of the microarchitectures, and on discussions with IBM staff, we give an abstract-machine semantics that abstracts from most of the implementation detail but explains the behaviour of a range of subtle examples. Our semantics is explained in prose but defined in rigorous machine-processed mathematics; we also confirm that it captures the observable processor behaviour, or the architectural intent, for our examples with an executable checker. While not officially sanctioned by the vendor, we believe that this model gives a reasonable basis for reasoning about current POWER multiprocessors.

Our work should bring new clarity to concurrent systems programming for these architectures, and is a necessary precondition for any analysis or verification. It should also inform the design of languages such as C and C++, where the language memory model is constrained by what can be efficiently compiled to such multiprocessors.

 
Litmus: running tests against hardware. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. In TACAS 2011. [ bib | doi | pdf | http ]
Shared memory multiprocessors typically expose subtle, poorly understood and poorly specified relaxed-memory semantics to programmers. To understand them, and to develop formal models to use in program verification, we find it essential to take an empirical approach, testing what results parallel programs can actually produce when executed on the hardware. We describe a key ingredient of our approach, our litmus tool, which takes small 'litmus test' programs and runs them for many iterations to find interesting behaviour. It embodies various techniques for making such interesting behaviour appear more frequently.

 
Relaxed-Memory Concurrency and Verified Compilation. Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. In POPL 2011. [ bib | doi | project page | pdf ]
In this paper, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation above x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behaviour of the hardware, the effects of compiler optimisation on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified (or verifying) compilation both essential and challenging.

We define a concurrent relaxed-memory semantics for ClightTSO, an extension of CompCert's Clight in which the processor's memory model is exposed for high-performance code. We discuss a strategy for verifying compilation from ClightTSO to x86, which we validate with correctness proofs (building on CompCert) for the most interesting compiler phases.

 
Mathematizing C++ Concurrency. Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. In POPL 2011. [ bib | doi | pdf ]
Shared-memory concurrency in C and C++ is pervasive in systems programming, but has long been poorly defined. This motivated an ongoing shared effort by the standards committees to specify concurrent behaviour in the next versions of both languages. They aim to provide strong guarantees for race-free programs, together with new (but subtle) relaxed-memory atomic primitives for high-performance concurrent code. However, the current draft standards, while the result of careful deliberation, are not yet clear and rigorous definitions, and harbour substantial problems in their details.

In this paper we establish a mathematical (yet readable) semantics for C++ concurrency. We aim to capture the intent of the current (`Final Committee') Draft as closely as possible, but discuss changes that fix many of its problems. We prove that a proposed x86 implementation of the concurrency primitives is correct with respect to the x86-TSO model, and describe our Cppmem tool for exploring the semantics of examples, using code generated from our Isabelle/HOL definitions.

Having already motivated changes to the draft standard, this work will aid discussion of any further changes, provide a correctness condition for compilers, and give a much-needed basis for analysis and verification of concurrent C and C++ programs.

 
Multi-Core Memory Models and Concurrency Theory (Dagstuhl Seminar 11011). Hans-Juergen Boehm, Ursula Goltz, Holger Hermanns, and Peter Sewell. Dagstuhl Reports, 1(1):1--26, 2011. [ bib | doi | pdf ]
This report documents the programme and the outcomes of Dagstuhl Seminar 11011 "Multi-Core Memory Models and Concurrency Theory".

 
Robin Milner 1934--2010: verification, languages, and concurrency. Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, and Peter Sewell. In POPL 2011. [ bib | doi ]
 
ppcmem, Jade Alglave, Luc Maranget, Pankaj Pawan, Susmit Sarkar, Peter Sewell, Derek Williams, and Francesco Zappa Nardelli, 2011. http://www.cl.cam.ac.uk/~pes20/ppcmem/. [ bib | http ]
 
N3196: Omnibus Memory Model and Atomics Paper, P. McKenney, M. Batty, C. Nelson, H. Boehm, A. Williams, S. Owens, S. Sarkar, P. Sewell, T. Weber, M.Wong, L. Crowl, and B. Kosnik. ISO JTC1/SC22/WG21 -- The C++ Standards Committee. Working Paper, November 2010. [ bib ]
 
Ott or Nott. Stephanie Weirich, Scott Owens, Peter Sewell, and Francesco Zappa Nardelli. In WMM 2010, 2pp. [ bib | project page | pdf ]
Ott: This talk discusses the experience of using Ott for programming language design. Or Nott? We reflect on the limitations of Ott, and on what other (New Ott?) tool support a working semanticist might want in an ideal world.

 
N3132: Mathematizing C++ Concurrency: The Post-Rapperswil Model, M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. ISO JTC1/SC22/WG21 - The C++ Standards Committee. Working Paper, August 2010. [ bib ]
 
N3125: Omnibus Memory Model and Atomics Paper, P. McKenney, M. Batty, C. Nelson, H. Boehm, A. Williams, S. Owens, S. Sarkar, P. Sewell, T. Weber, M.Wong, and L. Crowl. ISO JTC1/SC22/WG21 - The C++ Standards Committee. Working Paper, August 2010. [ bib ]
 
x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors. Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. Communications of the ACM, 53(7):89--97, July 2010. (Research Highlights). [ bib | doi | pdf | http ]
Exploiting the multiprocessors that have recently become ubiquitous requires high-performance and reliable concurrent systems code, for concurrent data structures, operating system kernels, synchronisation libraries, compilers, and so on. However, concurrent programming, which is always challenging, is made much more so by two problems. First, real multiprocessors typically do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory models, varying in subtle ways between processor families, in which different hardware threads may have only loosely consistent views of a shared memory. Second, the public vendor architectures, supposedly specifying what programmers can rely on, are often in ambiguous informal prose (a particularly poor medium for loose specifications), leading to widespread confusion.

In this paper we focus on x86 processors. We review several recent Intel and AMD specifications, showing that all contain serious ambiguities, some are arguably too weak to program above, and some are simply unsound with respect to actual hardware. We present a new x86-TSO programmer's model that, to the best of our knowledge, suffers from none of these problems. It is mathematically precise (rigorously defined in HOL4) but can be presented as an intuitive abstract machine which should be widely accessible to working programmers. We illustrate how this can be used to reason about the correctness of a Linux spinlock implementation and describe a general theory of data-race-freedom for x86-TSO. This should put x86 multiprocessor system building on a more solid foundation; it should also provide a basis for future work on verification of such systems.

 
Nomadic Pict: Programming Languages, Communication Infrastructure Overlays, and Semantics for Mobile Computation . Peter Sewell, Pawel Wojciechowski, and Asis Unyapoth. ACM Transactions on Programming Languages and Systems (TOPLAS), 32(4):1--63 (and electronic appendix, 33pp), 2010. [ bib | doi | project page | pdf ]
Mobile computation, in which executing computations can move from one physical computing device to another, is a recurring theme: from OS process migration, to language-level mobility, to virtual machine migration. This article reports on the design, implementation, and verification of overlay networks to support reliable communication between migrating computations, in the Nomadic Pict project. We define two levels of abstraction as calculi with precise semantics: a low-level Nomadic π calculus with migration and location-dependent communication, and a high-level calculus that adds location-independent communication. Implementations of location-independent communication, as overlay networks that track migrations and forward messages, can be expressed as translations of the high-level calculus into the low. We discuss the design space of such overlay network algorithms and define three precisely, as such translations. Based on the calculi, we design and implement the Nomadic Pict distributed programming language, to let such algorithms (and simple applications above them) to be quickly prototyped. We go on to develop the semantic theory of the Nomadic π calculi, proving correctness of one example overlay network. This requires novel equivalences and congruence results that take migration into account, and reasoning principles for agents that are temporarily immobile (e.g., waiting on a lock elsewhere in the system). The whole stands as a demonstration of the use of principled semantics to address challenging system design problems.

 
Ott: Effective Tool Support for the Working Semanticist. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. Journal of Functional Programming, 20(1):70--122, January 2010. Invited submission from ICFP 2007. [ bib | doi | project page | pdf ]
Semantic definitions of full-scale programming languages are rarely given, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics – usually either LaTeX for informal mathematics or the formal mathematics of a proof assistant – make it much harder than necessary to work with large definitions. We present a metalanguage specifically designed for this problem, and a tool, Ott, that sanity-checks such definitions and compiles them into proof assistant code for Coq, HOL, and Isabelle/HOL, together with LaTeX code for production-quality typesetting, and OCaml boilerplate. The main innovations are (1) metalanguage design to make definitions concise, and easy to read and edit; (2) an expressive but intuitive metalanguage for specifying binding structures; and (3) compilation to proof assistant code. This has been tested in substantial case studies, including modular specifications of calculi from the TAPL text, a Lightweight Java with Java JSR 277/294 module system proposals, and a large fragment of OCaml (OCamllight, 310 rules), with mechanised proofs of various soundness results. Our aim with this work is to enable a phase change: making it feasible to work routinely, without heroic effort, with rigorous semantic definitions of realistic languages.

 
Fences in Weak Memory Models. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. In CAV 2010. [ bib | doi | pdf ]
We present a class of relaxed memory models, defined in Coq, parameterised by the chosen permitted local reorderings of reads and writes, and the visibility of inter- and intra-processor communications through memory (e.g. store atomicity relaxation). We prove results on the required behaviour and placement of memory fences to restore a given model (such as Sequential Consistency) from a weaker one. Based on this class of models we develop a tool, diy, that systematically and automatically generates and runs litmus tests to determine properties of processor implementations. We detail the results of our experiments on Power and the model we base on them. This work identified a rare implementation error in Power 5 memory barriers (for which IBM is providing a workaround); our results also suggest that Power 6 does not suffer from this problem.

 
Memory, an elusive abstraction. Peter Sewell. In ISMM 2010, Invited talk abstract. [ bib | doi | pdf ]
 
Relaxed memory models must be rigorous. Francesco Zappa Nardelli, Peter Sewell, Jaroslav Ševčík, Susmit Sarkar, Scott Owens, Luc Maranget, Mark Batty, and Jade Alglave. In EC2. [ bib | pdf ]
Multiprocessors and high-level languages generally provide only relaxed (non-sequentially-consistent) memory models, to permit performance optimisations. One has to understand these models to program reliable concurrent systems -- but they are typically ambiguous and incomplete informal-prose documents, sometimes give guarantees that are too weak to be useful, and are sometimes simply unsound. Based on our previous work, we review various problems with some current specifications, for x86 (Intel 64/IA32 and AMD64), and Power and ARM processors, and for the Java and C++ languages. We argue that such specifications should be rigorously defined and tested.

 
A better x86 memory model: x86-TSO (extended version). Scott Owens, Susmit Sarkar, and Peter Sewell. Technical Report UCAM-CL-TR-745, University of Cambridge, Computer Laboratory, March 2009. 52pp. [ bib | pdf ]
Real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory models, typically described in ambiguous prose, which lead to widespread confusion. These are prime targets for mechanized formalization. In previous work we produced a rigorous x86-CC model, formalizing the Intel and AMD architecture specifications of the time, but those turned out to be unsound with respect to actual hardware, as well as arguably too weak to program above. We discuss these issues and present a new x86-TSO model that suffers from neither problem, formalized in HOL4. We believe it is sound with respect to real processors, reflects better the vendor's intentions, and is also better suited for programming. We give two equivalent definitions of x86-TSO: an intuitive operational model based on local write buffers, and an axiomatic total store ordering model, similar to that of the SPARCv8. Both are adapted to handle x86-specific features. We have implemented the axiomatic model in our memevents tool, which calculates the set of all valid executions of test programs, and, for greater confidence, verify the witnesses of such executions directly, with code extracted from a third, more algorithmic, equivalent version of the definition.

 
TCP, UDP, and Sockets: Volume 3: The Service-level Specification. Thomas Ridge, Michael Norrish, and Peter Sewell. Technical Report UCAM-CL-TR-742, University of Cambridge, Computer Laboratory, February 2009. 305pp. [ bib | project page | pdf ]
 
A better x86 memory model: x86-TSO. Scott Owens, Susmit Sarkar, and Peter Sewell. In TPHOLs 2009. [ bib | doi | pdf | http ]
Real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory models, typically described in ambiguous prose, which lead to widespread confusion. These are prime targets for mechanized formalization. In previous work we produced a rigorous x86-CC model, formalizing the Intel and AMD architecture specifications of the time, but those turned out to be unsound with respect to actual hardware, as well as arguably too weak to program above. We discuss these issues and present a new x86-TSO model that suffers from neither problem, formalized in HOL4. We believe it is sound with respect to real processors, reflects better the vendor’s intentions, and is also better suited for programming. We give two equivalent definitions of x86-TSO: an intuitive operational model based on local write buffers, and an axiomatic total store ordering model, similar to that of the SPARCv8. Both are adapted to handle x86-specific features. We have implemented the axiomatic model in our memevents tool, which calculates the set of all valid executions of test programs, and, for greater confidence, verify the witnesses of such executions directly, with code extracted from a third, more algorithmic, equivalent version of the definition.

 
The Semantics of Power and ARM Multiprocessor Machine Code. Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. In DAMP 2009. [ bib | doi | pdf ]
We develop a rigorous semantics for Power and ARM multiprocessor programs, including their relaxed memory model and the behaviour of reasonable fragments of their instruction sets. The semantics is mechanised in the HOL proof assistant. This should provide a good basis for informal reasoning and formal verification of low-level code for these weakly consistent architectures, and, together with our x86 semantics, for the design and compilation of high-level concurrent languages.

 
The Semantics of x86-CC Multiprocessor Machine Code. Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus Myreen, and Jade Alglave. In POPL 2009. [ bib | doi | pdf ]
Multiprocessors are now dominant, but real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have subtle relaxed (or weak) memory models, usually described only in ambiguous prose, leading to widespread confusion.

We develop a rigorous and accurate semantics for x86 multiprocessor programs, from instruction decoding to relaxed memory model, mechanised in HOL. We test the semantics against actual processors and the vendor litmus-test examples, and give an equivalent abstract-machine characterisation of our axiomatic memory model. For programs that are (in some precise sense) data-race free, we prove in HOL that their behaviour is sequentially consistent. We also contrast the x86 model with some aspects of Power and ARM behaviour.

This provides a solid intuition for low-level programming, and a sound foundation for future work on verification, static analysis, and compilation of low-level concurrent code.

 
Multiprocessor Architectures Don't Really Exist (But They Should). Peter Sewell. In MTV 2010, Invited session on Verification issues for multi-core systems. [ bib | pdf ]
Multiprocessors and high-level concurrent languages generally provide only relaxed (non-sequentially-consistent) memory models, to permit performance optimisations. One has to understand these models to program reliable concurrent systems but, despite work in this area over many years, the specifications of real-world multiprocessors and languages are typically ambiguous and incomplete informal-prose documents, cannot be used for testing hardware or software, sometimes give guarantees that are too weak to be useful, and are sometimes simply unsound. Such informal prose is a very poor medium for loose specifications. This talk will review various problems with some current specifications, for x86 (Intel 64/IA32 and AMD64), and Power and ARM processors, and for the Java and C++ languages, and describe ongoing work to produce rigorously defined specifications for some of these.

 
A rigorous approach to networking: TCP, from implementation to protocol to service. Tom Ridge, Michael Norrish, and Peter Sewell. In FM 2008. [ bib | doi | project page | ps | pdf | http ]
Despite more then 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code. In part this is because the scale and complexity of these protocols makes them challenging targets for formalization.

In this paper we show how these difficulties can be addressed. We develop a high-level specification for TCP and the Sockets API, expressed in the HOL proof assistant, describing the byte-stream service that TCP provides to users. This complements our previous low-level specification of the protocol internals, and makes it possible for the first time to state what it means for TCP to be correct: that the protocol implements the service. We define a precise abstraction function between the models and validate it by testing, using verified testing infrastructure within HOL. This is a pragmatic alternative to full proof, providing reasonable confidence at a relatively low entry cost.

Together with our previous validation of the low-level model, this shows how one can rigorously tie together concrete implementations, low-level protocol models, and specifications of the services they claim to provide, dealing with the complexity of real-world protocols throughout.

 
Verifying Overlay Networks for Relocatable Computations (or: Nomadic Pict, relocated). Peter Sewell and Pawel Wojciechowski. In RRDD Workshop, 2008. [ bib | project page | pdf ]
In the late 1990s we developed a calculus, Nomadic Pict, in which to express and verify overlay networks, for reliable communication between relocatable computations. Then, efficient system support for relocation was rare, and the calculus was reified in a prototype high-level programming language. Now, relocatable computation is a pervasive reality, though at the level of virtual machines rather than high-level languages. One can ask whether the semantic theory and algorithms developed for Nomadic Pict can be applied (or adapted) to infrastructure for communication between these virtual machines.

 
Dynamic Rebinding for Marshalling and Update, via Redex-time and Destruct-time Reduction. Peter Sewell, Gareth Stoyle, Michael Hicks, Gavin Bierman, and Keith Wansbrough. Journal of Functional Programming, 18(4):437--502, 2008. [ bib | doi | pdf ]
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example, when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically, it is provided only by ad hoc mechanisms that lack clean semantics. In this paper, we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to the simply typed call-by-value lambda calculus. To do so, we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies. The latter forms the basis for a lambda-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically typed. We sketch an extension of lambda-marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a lambda-update calculus with simple primitives to provide type-safe updating of running code. We show how the ideas of this simple calculus extend to more real-world, module-level dynamic updating in the style of Erlang. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.

 
Ott: Effective Tool Support for the Working Semanticist. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. In ICFP 2007, ACM SIGPLAN Most Influential ICFP Paper Award 2017 (for 2007). [ bib | doi | project page | ps | pdf ]
It is rare to give a semantic definition of a full-scale programming language, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics - usually either LaTeX for informal mathematics, or the formal mathematics of a proof assistant - make it much harder than necessary to work with large definitions.

We present a metalanguage specifically designed for this problem, and a tool, ott, that sanity-checks such definitions and compiles them into proof assistant code for Coq, HOL, Isabelle, and (in progress) Twelf, together with LaTeX code for production-quality typesetting, and OCaml boilerplate. The main innovations are:(1) metalanguage design to make definitions concise, and easy to read and edit;(2) an expressive but intuitive metalanguage for specifying binding structures; and (3) compilation to proof assistant code.

This has been tested in substantial case studies, including modular specifications of calculi from the TAPL text, a Lightweight Java with Java JSR 277/294 module system proposals, and a large fragment of OCaml (around 306 rules), with machine proofs of various soundness results. Our aim with this work is to enable a phase change: making it feasible to work routinely, without heroic effort, with rigorous semantic definitions of realistic languages.

 
The Java Module System: core design and semantic definition. Rok Strniša, Peter Sewell, and Matthew Parkinson. In OOPSLA 2007. [ bib | doi | project page | pdf ]
Java has no module system. Its packages only subdivide the class name space, allowing only a very limited form of component-level information hiding and reuse. Two Java Community Processes have started addressing this problem: one describes the runtime system and has reached an early draft stage, while the other considers the developer's view and only has a straw-man proposal. Both are natural language documents, which inevitably contain ambiguities.

In this work we design and formalize a core module system for Java. Where the JCP documents are complete, we follow them closely; elsewhere we make reasonable choices. We define the syntax, the type system, and the operational semantics of an LJAM language, defining these rigorously in the Isabelle/HOL automated proof assistant. Using this formalization, we identify various issues with the module system. We highlight the underlying design decisions, and discuss several alternatives and their benefits. Our Isabelle/HOL definitions should provide a basis for further consideration of the design alternatives, for reference implementations, and for proofs of soundness.

 
Specifying real-world binding structures. Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. In WMM 2007, 1pp. [ bib | project page | pdf ]
 
Mutatis Mutandis: Safe and predictable dynamic software updating. Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter Sewell, and Iulian Neamtiu. ACM Transactions on Programming Languages and Systems (TOPLAS), 29(4):70pp, August 2007. [ bib | doi | pdf ]
This article presents Proteus, a core calculus that models dynamic software updating, a service for fixing bugs and adding features to a running program. Proteus permits a program's type structure to change dynamically but guarantees the updated program remains type-correct by ensuring a property we call con-freeness. We show how con-freeness can be enforced dynamically, and how it can be approximated via a novel static analysis. This analysis can be used to assess the implications of a program's structure on future updates in order to make update success more predictable. We have implemented Proteus for C, and briefly discuss our implementation which we have tested on several well-known programs.

 
Ott release, version 0.10.9, Peter Sewell and Francesco Zappa Nardelli, August 2007. http://www.cl.cam.ac.uk/~pes20/ott/. [ bib | project page | http ]
 
Acute: High-level programming language design for distributed computation. Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, and Viktor Vafeiadis. Journal of Functional Programming, 17(4--5):547--612, July 2007. Invited submission for an ICFP 2005 special issue. [ bib | doi | project page | ps | pdf | http ]
Existing languages provide good support for typeful programming of stand-alone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct programs, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper, we discuss programming-language support for such systems, focussing on their typing and naming issues. We describe an experimental language, Acute, which extends an ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately built programs. The main features are (1) type-safe marshalling of arbitrary values; (2) type names that are generated (freshly and by hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system; (3) expression-level names generated to ensure that name equality tests suffice for type safety of associated values, for example, values carried on named channels; (4) controlled dynamic rebinding of marshalled values to local resources; and (5) thunkification of threads and mutexes to support computation mobility. These features are a large part of what is needed for typeful distributed programming. They are a relatively lightweight extension of ML, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs. This disentangles the language run-time from communication intricacies. This paper highlights the main design choices in Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype implementation, and by example distribution libraries.

 
Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL. Adam Biltcliffe, Michael Dales, Sam Jansen, Thomas Ridge, and Peter Sewell. In ICNP 2006, See also the SWIFT MAC Protocol: HOL Specification at http://www.cl.cam.ac.uk/~pes20/optical/spec.pdf. [ bib | doi | project page | ps | pdf | http ]
This paper reports on an experiment in network protocol design: we use novel rigorous techniques in the design process of a new protocol, in a close collaboration between systems and theory researchers.

The protocol is a Media Access Control (MAC) protocol for the SWIFT optical network, which uses optical switching and wavelength striping to provide very high bandwidth packet-switched interconnects. The use of optical switching (and the lack of optical buffering) means that the protocol must control the switch within hard timing constraints.

We use higher-order logic to express the protocol design, in the general-purpose HOL automated proof assistant. The specification is thus completely precise, but still concise, readable, and without accidental overspecification. Further, we test conformance between the specification and two implementations of the protocol: an NS-2 simulation model and the VHDL code of the network hardware. This involves: (1) proving, within HOL, that the specification is equivalent to an algorithmically-checkable version; (2) using automatic code-extraction to generate a testing oracle; and (3) applying that oracle to traces of the implementation.

This design-time use of rigorous methods has resulted in a protocol that is better specified and more correct than it would otherwise be, with relatively little effort.

 
Type-Safe Distributed Programming for OCaml. John Billings, Peter Sewell, Mark Shinwell, and Rok Strniša. In ML 2006. [ bib | doi | project page | ps | pdf | http ]
Existing ML-like languages guarantee type-safety, ensuring memory safety and protecting the invariants of abstract types, but only within single executions of single programs. Distributed programming is becoming ever more important, and should benefit even more from such guarantees. In previous work on theoretical calculi and the Acute prototype language we outlined techniques to provide them for simple languages.

In this paper we put these ideas into practice, describing the HashCaml extension to the OCaml bytecode compiler, which supports type-safe and abstraction-safe marshalling, together with related naming constructs. Our contribution is threefold: (1) We show how to define globally meaningful runtime type names for key OCaml type constructs that were not covered in our previous work, dealing with the generativity issues involved: user-defined variant and record types, substructures, functors, arbitrary ascription,separate compilation, and external C functions. (2) We support marshalling within polymorphic functions by type-passing, requiring us to build compositional runtime type names and revisit the OCaml relaxed value restriction. We show that with typed marshalling one must fall back to the SML97 value restriction. (3) We show how the above can be implemented with reasonable performance as an unintrusive modification to the existing OCaml language, implementation, and standard libraries. An alpha release of HashCaml, capable of bootstrapping itself, is available, along with an example type-safe distributed communication library written in the language.

 
HashCaml release, version 3.09.1-alpha-795, John Billings, Peter Sewell, Mark Shinwell, and Rok Strniša, April 2006. http://www.cl.cam.ac.uk/~pes20/hashcaml/index.html. [ bib | project page | .html ]
 
Engineering with Logic: HOL Specification and Symbolic-Evaluation Testing for TCP Implementations. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough. In POPL 2006. [ bib | doi | project page | ps | pdf | http ]
 
Process Calculi: The End of the Beginning? (From Thought Experiments to Experimental Semantics). Peter Sewell. Electr. Notes Theor. Comput. Sci., 162:317--321, 2006. [ bib | doi | http ]
This note reflects, from a Process Calculus point of view, on lessons learned during research modelling the real-world TCP and UDP network protocols.

 
It is Time to Mechanize Programming Language Metatheory. Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, and Steve Zdancewic. In VSTTE 2005, 5pp. [ bib | doi | project page | pdf | http ]
How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and programming language researchers alike? One crucial step towards achieving these goals is mechanized reasoning about language metatheory. The time has come to bring together the theorem proving and programming language communities to address this problem. We have proposed the POPLMark challenge as a concrete set of benchmarks intended both for measuring progress in this area and for stimulating discussion and collaboration. Our goal is to push the boundaries of existing technology to the point where we can achieve mechanized metatheory for the masses.

 
Acute: High-level programming language design for distributed computation. Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, and Viktor Vafeiadis. In ICFP 2005. [ bib | doi | project page | ps | pdf | http ]
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 pro-grams, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper we discuss programming language support for su ch systems, focussing on their typing and naming issues.

We describe an experimental language, Acute, which extends an ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built programs. The main features are: (1) type-safe marshalling of arbitrary values; (2) type names that are generated (freshly and by hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system; (3) expression-level names generated to ensure that name equality tests suffice for type-safety of associated values, e.g. values carried on named channels; (4) controlled dynamic rebinding of marshalled values to local resources; and (5) thunkification of threads and mutexes to support computation mobility.

These features are a large part of what is needed for typeful distributed programming. They are a relatively lightweight extension of ML, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs. This disentangles the language runtime from communication intricacies. This paper highlights the main design choices in Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype implementation, and by example distribution libraries.

 
Mechanized metatheory for the masses: The POPLmark Challenge. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. In TPHOLs 2005. [ bib | doi | project page | ps | pdf | http ]
How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs?

We propose an initial set of benchmarks for measuring progress in this area. Based on the metatheory of System F<:, a typed lambda-calculus with second-order polymorphism, subtyping, and records, these benchmarks embody many aspects of programming languages that are challenging to formalize: variable binding at both the term and type levels, syntactic forms with variable numbers of components (including binders), and proofs demanding complex induction principles. We hope that these benchmarks will help clarify the current state of the art, provide a basis for comparing competing technologies, and motivate further research.

 
Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough. In SIGCOMM 2005. [ bib | doi | project page | ps | pdf | http ]
Network protocols are hard to implement correctly. Despite the existence of RFCs and other standards, implementations often have subtle differences and bugs. One reason for this is that the specifications are typically informal, and hence inevitably contain ambiguities. Conformance testing against such specifications is challenging.

In this paper we present a practical technique for rigorous protocol specification that supports specification-based testing. We have applied it to TCP, UDP, and the Sockets API, developing a detailed ‘post-hoc’ specification that accurately reflects the behaviour of several existing implementations (FreeBSD 4.6, Linux 2.4.20-8, and Windows XP SP1). The development process uncovered a number of differences between and infelicities in these implementations.

Our experience shows for the first time that rigorous specification is feasible for protocols as complex as TCP. We argue that the technique is also applicable ‘pre-hoc’, in the design phase of new protocols. We discuss how such a design-for-test approach should influence protocol development, leading to protocol specifications that are both unambiguous and clear, and to high-quality implementations that can be tested directly against those specifications.

 
Passive-attack analysis for connection-based anonymity systems. Andrei Serjantov and Peter Sewell. International Journal of Information Security, 4(3):172--180, June 2005. Special issue on ESORICS 2003. [ bib | doi | http ]
In this paper we consider low-latency connection-based anonymity systems which can be used for applications like web browsing or SSH. Although several such systems have been designed and built, their anonymity has so far not been adequately evaluated.

We analyse the anonymity of connection-based systems against global passive adversaries. We give a precise description of a packet-counting attack which requires a very low degree of precision from the adversary, evaluate its effectiveness against connection-based systems depending on their size, architecture and configuration, and calculate the amount of traffic necessary to provide a minimum degree of protection. We then present a second attack based on tracking connection starts which gives us another lower bound on traffic volumes required to provide at least some anonymity.

 
TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification. Volume 1: Overview. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough. Technical Report UCAM-CL-TR-624, Computer Laboratory, University of Cambridge, March 2005. 88pp. [ bib | project page | ps | pdf | .html ]
We have developed a mathematically rigorous and experimentally-validated post-hoc specification of the behaviour of TCP, UDP, and the Sockets API. It characterises the API and network-interface interactions of a host, using operational semantics in the higher-order logic of the HOL automated proof assistant. The specification is detailed, covering almost all the information of the real-world communications: it is in terms of individual TCP segments and UDP datagrams, though it abstracts from the internals of IP. It has broad coverage, dealing with arbitrary API call sequences and incoming messages, not just some well-behaved usage. It is also accurate, closely based on the de facto standard of (three of) the widely-deployed implementations. To ensure this we have adopted a novel experimental semantics approach, developing test generation tools and symbolic higher-order-logic model checking techniques that let us validate the specification directly against several thousand traces captured from the implementations.

The resulting specification, which is annotated for the non-HOL-specialist reader, may be useful as an informal reference for TCP/IP stack implementors and Sockets API users, supplementing the existing informal standards and texts. It can also provide a basis for high-fidelity automated testing of future implementations, and a basis for design and formal proof of higher-level communication layers. More generally, the work demonstrates that it is feasible to carry out similar rigorous specification work at design-time for new protocols. We discuss how such a design-for-test approach should influence protocol development, leading to protocol specifications that are both unambiguous and clear, and to high-quality implementations that can be tested directly against those specifications.

This document (Volume 1) gives an overview of the project, discussing the goals and techniques and giving an introduction to the specification. The specification itself is given in the companion Volume 2 (UCAM-CL-TR-625), which is automatically typeset from the (extensively annotated) HOL source. As far as possible we have tried to make the work accessible to four groups of intended readers: workers in networking (implementors of TCP/IP stacks, and designers of new protocols); in distributed systems (implementors of software above the Sockets API); in distributed algorithms (for whom this may make it possible to prove properties about executable implementations of those algorithms); and in semantics and automated reasoning.

 
TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification. Volume 2: The Specification.. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough. Technical Report UCAM-CL-TR-625, Computer Laboratory, University of Cambridge, March 2005. 386pp. [ bib | project page | ps | pdf | .html ]
See Volume 1 (UCAM-CL-TR-624).

 
An approximation to the real TCP state diagram, Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough, March 2005. This is a poster with a version of the "TCP state diagram" extracted from the specification. It is rather more complete than the usual diagram, but is still a very abstract and simplified view of the state space of our specification. It is intended to be printed at A1 size or bigger. [ bib | project page | ps | pdf ]
 
Mutatis Mutandis: Safe and Predictable Dynamic Software Updating. Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter Sewell, and Iulian Neamtiu. In POPL 2005. [ bib | doi | pdf | http ]
Dynamic software updates can be used to fix bugs or add features to a running program without downtime. Essential for some applications and convenient for others, low-level dynamic updating has been used for many years. Perhaps surprisingly, there is little high-level understanding or language support to help programmers write dynamic updates effectively.

To bridge this gap, we present Proteus, a core calculus for dynamic software updating in C-like languages that is flexible, safe, and predictable. Proteus supports dynamic updates to functions (even active ones), to named types and to data, allowing on-line evolution to match source-code evolution as we have observed it in practice. We ensure updates are type-safe by checking for a property we call “con-freeness” for updated types t at the point of update. This means that non-updated code will not use t concretely beyond that point (concrete usages are via explicit coercions) and thus t's representation can safely change. We show how con-freeness can be enforced dynamically for a particular program state. We additionally define a novel and efficient static updateability analysis to establish con-freeness statically, and can thus automatically infer program points at which all future (well-formed) updates will be type-safe. We have implemented our analysis for C and tested it on several well-known programs.

 
Source release of the Acute system, Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-Williams, Francesco Zappa Nardelli, Pierre Habouzit, and Viktor Vafeiadis, January 2005. Available from http://www.cl.cam.ac.uk/users/pes20/acute/distro/acute-0.50-1-src.tar.gz. [ bib | project page | http ]
 
Acute: High-level programming language design for distributed computation. Design rationale and language definition. Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-Williams, Francesco Zappa Nardelli, Pierre Habouzit, and Viktor Vafeiadis. Technical Report UCAM-CL-TR-605, University of Cambridge Computer Laboratory, October 2004. Also published as INRIA RR-5329. 193pp. [ bib | project page | ps | pdf | .html ]
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 extends an OCaml core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built programs. It is expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs, disentangling the language runtime from communication.

This requires a synthesis of novel and existing features: (1) type-safe marshalling of values between programs; (2) dynamic loading and controlled rebinding to local resources; (3) modules and abstract types with abstraction boundaries that are respected by interaction; (4) global names, generated either freshly or based on module hashes: at the type level, as runtime names for abstract types; and at the term level, as channel names and other interaction handles; (5) versions and version constraints, integrated with type identity; (6) local concurrency and thread thunkification; and (7) second-order polymorphism with a namecase construct.

We deal with the interplay among these features and the core, and develop a semantic definition that tracks abstraction boundaries, global names, and hashes throughout compilation and execution, but which still admits an efficient implementation strategy.

 
Cassandra: Distributed Access Control Policies with Tunable Expressiveness. Moritz Y. Becker and Peter Sewell. In POLICY 2004. [ bib | doi | pdf | http ]
We study the specification of access control policy in large-scale distributed systems. Our work on real-world policies has shown that standard policy idioms such as role hierarchy or role delegation occur in practice in many subtle variants. A policy specification language should therefore be able to express this variety of features smoothly, rather than add them as specific features in an ad hoc way, as is the case in many existing languages. We present Cassandra, a role-based trust management system with an elegant and readable policy specification language based on Datalog with constraints. The expressiveness (and computational complexity) of the language can be adjusted by choosing an appropriate constraint domain. With just five special predicates, we can easily express a wide range of policies including role hierarchy, role delegation, separation of duties, cascading revocation, automatic credential discovery and trust negotiation. Cassandra has a formal semantics for query evaluation and for the access control enforcement engine. We use a goal-oriented distributed policy evaluation algorithm that is efficient and guarantees termination. Initial performance results for our prototype implementation have been promising.

 
Cassandra: Flexible Trust Management, Applied to Electronic Health Records. Moritz Y. Becker and Peter Sewell. In CSFW 2004. [ bib | doi | ps | pdf | http ]
We study the specification of access control policy in large-scale distributed systems. We present Cassandra, a language and system for expressing policy, and the results of a substantial case study, a security policy for a national Electronic Health Record system, based on the requirements for the ongoing UK National Health Service procurementexercise.

Cassandra policies are expressed in a language based on Datalog with constraints. The expressiveness of the language (and its computational complexity) can be tuned by choosing an appropriate constraint domain.

Cassandra is role-based; it supports credential-based access control (e.g. between administrative domains); and rules can refer to remote policies (for automatic credential retrieval and trust negotiation). Moreover, the policy language is small, and it has a formal semantics for query evaluation and for the access control engine. For the case study we choose a constraint domain C0 thatis sufficiently expressive to encode many policy idioms. The case study turns out to require many subtle variants of these; it is important to express this variety smoothly, rather than add them as ad hoc features. By ensuring only a constraint compact fragment of C0 is used, we guarantee a finite and computable fixed-point model. We use a top-down evaluation algorithm, for efficiency and to guarantee termination.

The case study (with some 310 rules and 58 roles) demonstrates that this language is expressive enough for a real-world application; preliminary results suggest that the per-formance should be acceptable.

 
Models for Name-Passing Processes: Interleaving and Causal. Gian Luca Cattani and Peter Sewell. Information and Computation, 190(2):136--178, May 2004. [ bib | doi | http ]
We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual π-calculus operations, defining Indexed Labelled Transition Systems. For non-interleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. We establish completeness properties of, and adjunctions between, categories of the two models. Alternative indexing structures and possible applications are also discussed. These are first steps towards a uniform understanding of the semantics and operations of name-passing calculi.

 
Acute and TCP: specifying and developing abstractions for global computation. James Leifer, Michael Norrish, Peter Sewell, and Keith Wansbrough. In APPSEM II Workshop, 2004, 2pp. [ bib ]
 
Dynamic Rebinding for Marshalling and Update, with Destruct-time λ. Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, and Keith Wansbrough. Technical Report UCAM-CL-TR-568, University of Cambridge Computer Laboratory, February 2004. 85pp. [ bib | ps | pdf | .html ]
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically it is provided only by ad-hoc mechanisms that lack clean semantics.

In this paper we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to the simply-typed call-by-value λ-calculus. To do so we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies. The latter forms the basis for a λ-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically-typed. We sketch an extension of λ-marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a λ-update calculus with simple primitives to provide type-safe updating of running code. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.

 
Applied Semantics: Specifying and Developing Abstractions for Distributed Computation (Grand Challenge Discussion Paper -- GC2, GC4, and GC6), Peter Sewell and Keith Wansbrough. Position paper for Grand Challenge meeting (Newcastle). 5pp, 2004. [ bib | pdf ]
 
The TCP Specification: A Quick Introduction, Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, and Keith Wansbrough, 2004. [ bib | project page | ps | pdf ]
 
Passive Attack Analysis for Connection-Based Anonymity Systems. Andrei Serjantov and Peter Sewell. In ESORICS 2003. [ bib | doi | ps | pdf | http ]
In this paper we consider low latency connection-based anonymity system which can be used for applications like web browsing or SSH. Although several such sys tems have been designed and built, their anonymity has so far not been adequatel y evaluated.

We analyse the anonymity of connection-based systems against passive adversaries. We give a precise description of two attacks, evaluate their effectiveness, and calculate the amount of traffic necessary to render the attacks useless.

 
Global abstraction-safe marshalling with hash types. James Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough. In ICFP 2003. [ bib | doi | ps | pdf | http ]
Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent stores. In this paper we combine the two, developing compile-time and run-time semantics for marshalling, that guarantee abstraction-safety between separately-built programs. We obtain a namespace for abstract types that is global, i.e. meaningful between programs, by hashing module declarations. We examine the scenarios in which values of abstract types are communicated from one program to another, and ensure, by constructing hashes appropriately, that the dynamic and static notions of type equality mirror each other. We use singleton kinds to express abstraction in the static semantics; abstraction is tracked in the dynamic semantics by coloured brackets. These allow us to prove preservation, erasure, and coincidence results. We argue that our proposal is a good basis for extensions to existing ML-like languages, pragmatically straightforward for language users and for implementors.

 
Dynamic Rebinding for Marshalling and Update, with Destruct-time lambda. Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, and Keith Wansbrough. In ICFP 2003. [ bib | doi | ps | pdf | http ]
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically it is provided only by ad-hoc mechanisms that lack clean semantics. In this paper we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to simply-typed call-by-value lambda-calculus. To do so we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies. The latter forms the basis for a lambda-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically-typed. We sketch an extension of lambda-marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a lambda-update calculus with simple primitives to provide type-safe updating of running code. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.

 
Global abstraction-safe marshalling with hash types. James Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough. Technical Report UCAM-CL-TR-569, University of Cambridge Computer Laboratory, June 2003. Also published as INRIA Rocquencourt report RR-4851. 86pp. [ bib | ps | pdf | .html ]
Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent stores. In this paper we combine the two, developing compile-time and run-time semantics for marshalling, that guarantee abstraction-safety between separately-built programs.

We obtain a namespace for abstract types that is global, ie meaningful between programs, by hashing module declarations. We examine the scenarios in which values of abstract types are communicated from one program to another, and ensure, by constructing hashes appropriately, that the dynamic and static notions of type equality mirror each other. We use singleton kinds to express abstraction in the static semantics; abstraction is tracked in the dynamic semantics by coloured brackets. These allow us to prove preservation, erasure, and coincidence results. We argue that our proposal is a good basis for extensions to existing ML-like languages, pragmatically straightforward for language users and for implementors.

 
Formalizing Dynamic Software Updating. Gavin Bierman, Michael Hicks, Peter Sewell, and Gareth Stoyle. In USE 2003, 17pp. [ bib | ps | pdf ]
Dynamic software updating (DSU) enables running programs to be updated with new code and data without interrupting their execution. A number of DSU systems have been designed, but there is still little rigorous und erstanding of how to use DSU technology so that updates are safe. As a first step in this direction, we introduce a small update calculus with a precise mathematical semantics. The calculus is formulated as an extension of a typed lambda calculus, and supports updating technology similar to that of the programming language Erlang [2]. Our goal is to provide a simple yet expressive foundation for reasoning about dynamically updat eable software. In this paper, we present the details of the calculus, give some examples of its expressive power, and discuss how it might be used or extended to guarantee safety properties.

 
Secure Composition of Untrusted Code: Box-π, Wrappers and Causality Types. Peter Sewell and Jan Vitek. Journal of Computer Security, 11(2):135--188, 2003. Invited submission for a CSFW 00 special issue. [ bib | ps | pdf | http ]
Software systems are becoming heterogeneous: instead of a small number of large programs from well-established sources, a user's desktop may now consist of many smaller components that interact in intricate ways. Some components will be downloaded from the network from sources that are only partially trusted. A user would like to know that a number of security properties hold, e.g. that personal data is not leaked to the net, but it is typically infeasible to verify that such components are well-behaved. Instead, they must be executed in a secure environment that provides fine-grain control of the allowable interactions between them, and between components and other system resources.

In this paper, we consider the problem of assembling concurrent software systems from untrusted or partially trusted off-the-shelf components, using wrapper programs to encapsulate components and enforce security policies. We introduce a model programming language, the box-ss calculus, that supports composition of software components and the enforcement of information flow security policies. Several example wrappers are expressed using the calculus; we explore the delicate security properties they guarantee. We present a novel causal type system that statically captures the allowed flows between wrapped possibly-badly-typed components; we use it to prove that an example ordered pipeline wrapper enforces a causal flow property.

 
Iota: A concurrent XML scripting language with applications to Home Area Networking. G. M. Bierman and P. Sewell. Technical Report UCAM-CL-TR-557, Computer Laboratory, University of Cambridge, January 2003. 32pp. [ bib | pdf | .html ]
Iota is a small and simple concurrent language that provides native support for functional XML computation and for typed channel-based communication. It has been designed as a domain-specific language to express device behaviour within the context of Home Area Networking. In this paper we describe Iota, explaining its novel treatment of XML and describing its type system and operational semantics. We give a number of examples including Iota code to program Universal Plug 'n' Play (UPnP) devices.

 
Rigour is good for you, and feasible: reflections on formal treatments of C and UDP sockets.. Michael Norrish, Peter Sewell, and Keith Wansbrough. In SIGOPS EW 2002. [ bib | doi | project page | ps | pdf | http ]
We summarise two projects that formalised complex real world systems: UDP and its sockets API, and the C programming language. We describe their goals and the techniques used in both. We conclude by discussing how such techniques might be applied to other system software and by describing the benefits this may bring.

 
Timing UDP: mechanized semantics for sockets, threads and failures. Keith Wansbrough, Michael Norrish, Peter Sewell, and Andrei Serjantov. In ESOP 2002. [ bib | doi | project page | ps | pdf | http ]
This paper studies the semantics of failure in distributed programming. We present a semantic model for distributed programs that use the standard sockets interface; it covers message loss, host failure and temporary disconnection, and supports reasoning about distributed infrastructure. We consider interaction via the UDP and ICMP protocols. To do this, it has been necessary to: construct an experimentallyvalidated post-hoc specification of the UDP/ICMP sockets interface; develop a timed operational semantics with threads, as such programs are typically multithreaded and depend on timeouts; model the behaviour of partial systems, making explicit the interactions that the infrastructure offers to applications; integrate the above with semantics for an executable fragment of a programming language (OCaml) with OS library primitives; and use tool support to manage complexity, mechanizing the model with the HOL theorem prover. We illustrate the whole with a module providing na¨ıve heartbeat failure detection.

 
From Rewrite Rules to Bisimulation Congruences. Peter Sewell. Theoretical Computer Science, 274(1--2):183--230, March 2002. Invited submission for a CONCUR 98 special issue. [ bib | doi | ps | pdf | http ]
The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. This paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As a test of the theory it is shown that bisimulation for a fragment of CCS is recovered. The transitions generated for a fragment of the Ambient Calculus of Cardelli and Gordon, and for SKI combinators, are also discussed briefly.

 
Chapter 9, Pi Calculus, in the book Formal Methods for Distributed Processing, A Survey of Object Oriented Approaches, edited by Howard Bowman and John Derrick, Peter Sewell. pages 177--197. Cambridge University Press, December 2001. ISBN 0521771846. The links are to the TR498 extended version of the book chapter. [ bib | ps | pdf ]
This note provides a brief introduction to π-calculi and their application to concurrent and distributed programming. Chapter 1 introduces a simple π-calculus and discusses the choice of primitives, operational semantics (in terms of reductions and of indexed early labelled transitions), operational equivalences, Pict-style programming and typing. Chapter 2 goes on to discuss the application of these ideas to distributed systems, looking informally at the design of distributed π-calculi with grouping and interaction primitives. Chapter 3 returns to typing, giving precise definitions for a simple type system and soundness results for the labelled transition semantics. Finally, Chapters 4 and 5 provide a model development of the metatheory, giving first an outline and then detailed proofs of the results stated earlier. The note can be read in the partial order 1.(2+3+4.5).

 
The UDP Calculus: Rigorous Semantics for Real Networking. Andrei Serjantov, Peter Sewell, and Keith Wansbrough. In TACS 2001. [ bib | doi | project page | ps | pdf | http ]
Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP, UDP, TCP etc), concurrency, packet loss, host failure, timeouts, the complex sockets interface to the protocols, and subtle portability issues. Moreover, the behavioural prope rties of operating systems and the network are not well documented.

A few of these issues have been addressed in the process calculus and distributed algorithm communities, but there remains a wide gulf between what ha s been captured in semantic models and what is required for a precise understanding of the behaviour of practical distributed programs t hat use these protocols.

In this paper we demonstrate (in a preliminary way) that the gulf can be bridged. We give an operational model for socket programming with a substantial fraction of UDP and ICMP, including loss and failure. The model has been validated by experiment against actual systems. It is not tied to a particular programming language, but can be used with any language equipped with an operational semantics for system calls - here we give such a language binding for an OCaml fragment. We illustrate the model with a few small network programs.

 
The UDP Calculus: Rigorous Semantics for Real Networking. Andrei Serjantov, Peter Sewell, and Keith Wansbrough. Technical Report UCAM-CL-TR-515, Computer Laboratory, University of Cambridge, July 2001. iv+70pp. [ bib | project page | ps | pdf | .html ]
Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP, UDP, TCP, etc.), concurrency, packet loss, host failure, timeouts, the complex sockets interface to the protocols, and subtle protability issues. Moreover, the behavioural properties of operating systems and the network are not well documented.

A few of these issues have been addressed in the process calculus and distributed algorithm communities, but there remains a wide gulf between what has been captured in semantic models and what is required for a precise understanding of the behaviour of practical distributed programs that use these protocols.

In this paper we demonstrate (in a preliminary way) that the gulf can be bridged. We give an operational model for socket programming with a substantial fraction of UDP and ICMP, including loss and failure. The model has been validated by experiment against actual systems. It is not tied to a particular programming language, but can be used with any language equipped with an operational semantics for system calls – here we give such a language binding for an OCaml fragment. We illustrate the model with a few small network programs.

 
Timing UDP: The HOL Model, Michael Norrish, Andrei Serjantov, Peter Sewell, and Keith Wansbrough, July 2001. http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html. [ bib | project page | .html ]
 
Modules, Abstract Types, and Distributed Versioning. Peter Sewell. In POPL 2001. [ bib | doi | errata | pdf | http ]
In a wide-area distributed system it is often impractical to synchronise software updates, so one must deal with many coexisting versions. We study static typing support for modular wide-area programming, modelling separate compilation/linking and execution of programs that interact along typed channels. Interaction may involve communication of values of abstract types; we provide the developer with finegrain versioning control of these types to support interoperation of old and new code. The system makes use of a second-class module system with singleton kinds; we give a novel operational semantics for separate compilation/linking and execution and prove soundness.

 
Nomadic Pict: Correct Communication Infrastructure for Mobile Computation. Asis Unyapoth and Peter Sewell. In POPL 2001. [ bib | doi | project page | ps | pdf | http ]
This paper addresses the design and verification of infrastructure for mobile computation. In particular, we study language primitives for communication between mobile agents. They can be classified into two groups. At a low level there are location dependent primitives that require a programmer to know the current site of a mobile agent in order to communicate with it. At a high level there are location independent primitives that allow communication with a mobile agent irrespective of any migrations. Implementation of the high level requires delicate distributed infrastructure algorithms. In earlier work with Wojciechowski and Pierce we made the two levels precise as process calculi, allowing such algorithms to be expressed as encodings of the high level into the low level; we built Nomadic Pict, a distributed programming language for experimenting with such encodings. In this paper we turn to semantics, giving a definition of the core language and proving correctness of an example infrastructure. This requires novel techniques: we develop equivalences that take migration into account, and reasoning principles for agents that are temporarily immobile (eg. waiting on a lock elsewhere in the system).

 
Modules, Abstract Types, and Distributed Versioning. Peter Sewell. Technical Report UCAM-CL-TR-506, University of Cambridge, September 2000. 46pp. [ bib | errata | ps | pdf | .html ]
In a wide-area distributed system it is often impractical to synchronise software updates, so one must deal with many coexisting versions. We study static typing support for modular wide-area programming, modelling separate compilation/linking and execution of programs that interact along typed channels. Interaction may involve communication of values of abstract types; we provide the developer with fine-grain versioning control of these types to support interoperation of old and new code. The system makes use of a second-class module system with singleton kinds; we give a novel operational semantics for separate compilation/linking and execution and prove soundness.

 
Models for Name-Passing Processes: Interleaving and Causal. Gian Luca Cattani and Peter Sewell. Technical Report UCAM-CL-TR-505, Computer Laboratory, University of Cambridge, September 2000. 42pp. [ bib | ps | pdf | .html ]
We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual π-calculus operations, defining Indexed Labelled Transition Systems. For noninterleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. We establish completeness properties of, and adjunctions between, categories of the two models. Alternative indexing structures and possible applications are also discussed. These are first steps towards a uniform understanding of the semantics and operations of name-passing calculi.

 
Applied π -- A Brief Tutorial. Peter Sewell. Technical Report UCAM-CL-TR-498, Computer Laboratory, University of Cambridge, August 2000. 65pp. [ bib | ps | pdf | .html ]
This note provides a brief introduction to π-calculi and their application to concurrent and distributed programming. Chapter 1 introduces a simple π-calculus and discusses the choice of primitives, operational semantics (in terms of reductions and of indexed early labelled transitions), operational equivalences, Pict-style programming and typing. Chapter 2 goes on to discuss the application of these ideas to distributed systems, looking informally at the design of distributed π-calculi with grouping and interaction primitives. Chapter 3 returns to typing, giving precise definitions for a simple type system and soundness results for the labelled transition semantics. Finally, Chapters 4 and 5 provide a model development of the metatheory, giving first an outline and then detailed proofs of the results stated earlier. The note can be read in the partial order 1.(2+3+4.5).

 
Secure Composition of Untrusted Code: Wrappers and Causality Types. Peter Sewell and Jan Vitek. In CSFW 2000. [ bib | doi | ps | pdf | http ]
We consider the problem of assembling concurrent software systems from untrusted or partially trusted off-the-shelf components, using wrapper programs to encapsulate components and enforce security policies. In previous work we introduced the box-π process calculus with constrained interaction to express wrappers and discussed the rigorous formulation of their security properties. This paper addresses the verification of wrapper information flow properties. We present a novel causal type system that statically captures the allowed flows between wrapped possiblybadly-typed components; we use it to prove that an example unidirectional-flow wrapper enforces a causal flow property.

 
Models for Name-Passing Processes: Interleaving and Causal (Extended Abstract). Gian Luca Cattani and Peter Sewell. In LICS 2000. [ bib | doi | ps | pdf | http ]
We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual π-calculus operations, defining Indexed Labelled Transition Systems. For non-interleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. This is a first step towards a uniform understanding of the semantics and operations of name-passing calculi.

 
Nomadic Pict: Language and Infrastructure Design for Mobile Agents. Pawel T. Wojciechowski and Peter Sewell. IEEE Concurrency, 8(2):42--52, April--June 2000. Invited submission for ASA/MA 99. [ bib | doi | project page | http ]
Location-independent communication between migrating agents requires a distributed infrastructure. The authors describe their Nomadic Pict distributed programming language and use it to develop an infrastructure for an example application.

 
Secure Composition of Untrusted Code: Wrappers and Causality Types. Peter Sewell and Jan Vitek. Technical Report UCAM-CL-TR-478, Computer Laboratory, University of Cambridge, November 1999. 36pp. [ bib | ps | pdf | .html ]
We consider the problem of assembling concurrent software systems from untrusted or partially trusted off-the-shelf components, using wrapper programs to encapsulate components and enforce security policies. In previous work we introduced the box-π process calculus with constrained interaction to express wrappers and discussed the rigorous formulation of their security properties. This paper addresses the verification of wrapper information flow properties. We present a novel causal type system that statically captures the allowed flows between wrapped possibly-badly-typed components; we use it to prove that a unidirectional-flow wrapper enforces a causal flow property.

 
Nomadic Pict: Language and Infrastructure Design for Mobile Agents. Pawel T. Wojciechowski and Peter Sewell. In ASA/MA 1999, Best paper award. [ bib | doi | project page | ps | pdf | http ]
We study the distributed infrastructures required for location-independent communication between migrating agents. These infrastructures are problematic: different applications may have very different patterns of migration and communication, and require different performance and robustness properties; algorithms must be designed with these in mind. To study this problem we introduce an agent programming language --- Nomadic Pict. It is designed to allow infrastructure algorithms to be expressed as clearly as possible, as translations from a high-level language to a low level. The levels are based on rigorously-defined process calculi, they provide sharp levels of abstraction. In this paper we describe the language and use it to develop an infrastructure for an example application. The language and examples have been implemented; we conclude with a description of the compiler and runtime.

 
Location-Independent Communication for Mobile Agents: a Two-Level Architecture, Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce. pages 1--31. Springer-Verlag, October 1999. [ bib | doi | project page | ps | pdf | .html ]
We study communication primitives for interaction between mobile agents. They can be classified into two groups. At a low level there are location dependent primitives that require a programmer to know the current site of a mobile agent in order to communicate with it. At a high level there are location independent primitives that allow communication with a mobile agent irrespective of its current site and of any migrations. Implementation of these requires delicate distributed infrastructure. We propose a simple calculus of agents that allows implementation of such distributed infrastructure algorithms to be expressed as encodings, or compilations, of the whole calculus into the fragment with only location dependent communication. These encodings give executable descriptions of the algorithms, providing a clean implementation strategy for prototype languages. The calculus is equipped with a precise semantics, providing a solid basis for understanding the algorithms and reasoning about their correctness and robustness. Two sample infrastructure algorithms are presented as encodings.

 
Secure Composition of Insecure Components. Peter Sewell and Jan Vitek. In CSFW 1999. [ bib | doi | ps | pdf | http ]
Software systems are becoming heterogeneous: instead of a small number of large programs from well-established sources, a user's desktop may now consist of many smaller components that interact in intricate ways. Some components will be downloaded from the network from sources that are only partially trusted. A user would like to know that a number of security properties hold, e.g. that personal data is not leaked to the net, but it is typically infeasible to verify that such components are well-behaved. Instead, they must be executed in a secure environment, or wrapper, that provides fine-grain control of the allowable interactions between them, and between components and other system resources. In this paper we study such wrappers, focusing on how they can be expressed in a way that enables their security properties to be stated and proved rigorously. We introduce a model programming language, the box-pi calculus, that supports composition of software components and the enforcement of security policies. Several example wrappers are expressed using the calculus; we explore the delicate security properties they guarantee.

 
Secure Composition of Insecure Components. Peter Sewell and Jan Vitek. Technical Report UCAM-CL-TR-463, Computer Laboratory, University of Cambridge, April 1999. 44pp. [ bib | ps | pdf | .html ]
Software systems are becoming heteroheneous: instead of a small number of large programs from well-established sources, a user’s desktop may now consist of many smaller components that interact in intricate ways. Some components will be downloaded from the network from sources that are only partially trusted. A user would like to know that a number of security properties hold, e.g. that personal data is not leaked to the net, but it is typically infaesible to verify that such components are well-behaved. Instead they must be executed in a secure environment, or wrapper, that provides fine-grain control of the allowable interactions between them, and between components and other system resources.

In this paper we study such wrappers, focussing on how they can be expressed in a way that enables their security properties to be stated and proved rigorously. We introduce a model programming language, the box-π calculus, that supports composition of software components and the enforcement of security policies. Several example wrappers are expressed using the calculus; we explore the delicate security properties they guarantee.

 
Location-Independent Communication for Mobile Agents: a Two-Level Architecture. Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce. Technical Report UCAM-CL-TR-462, Computer Laboratory, University of Cambridge, April 1999. 31pp. [ bib | project page | ps | pdf | .html ]
We study communication primitives for interaction between mobile agents. They can be classified into two groups. At a low level there are location dependent primitives that require a programmer to know the current site of a mobile agent in order to communicate with it. At a high level there are location independent primitives that allow communication with a mobile agent irrespective of its current site and of any migrations. Implementation of these requires delicate distributed infrastructure. We propose a simple calculus of agents that allows implementation of such distributed infrastructure algorithms to be expressed as encodings, or compilations, of the whole calculus into the fragment with only location dependent communication. These encodings give executable descriptions of the algorithms, providing a clean implementation strategy for prototype languages. The calculus is equipped with a precise semantics, providing a solid basis for understanding the algorithms and reasoning about their correctness and robustness. Two sample infrastructure algorithms are presented as encodings.

 
A Brief Introduction to Applied π, Peter Sewell, January 1999. Lecture notes for the Mathfit Instructional Meeting on Recent Advances in Semantics and Types for Concurrency: Theory and Practice, July 1998. [ bib | .html ]
 
From Rewrite Rules to Bisimulation Congruences. Peter Sewell. In CONCUR 1998, Subsumed by the TCS 2002 paper. [ bib | doi | ps | pdf | http ]
The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. This paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As a test of the theory it is shown that bisimulation for a fragment of CCS is recovered. The transitions generated for a fragment of the Ambient Calculus of Cardelli and Gordon, and for SKI combinators, are also discussed briefly.

 
Global/Local Subtyping and Capability Inference for a Distributed π-calculus. Peter Sewell. In ICALP 1998, The ps link is to an extended version. [ bib | doi | ps | pdf | http ]
This paper considers how locality restrictions on the use of capabilities can be enforced by a static type system. A distributed π-calculus with a simple reduction semantics is introduced, integrating location and migration primitives from the Distributed Join Calculus with asynchronous π communication. It is given a type system in which the input and output capabilities of channels may be either global, local or absent. This allows compile-time optimization where possible but retains the expressiveness of channel communication. Subtyping allows all communications to be invoked uniformly. We show that the most local possible capabilities for internal channels can be inferred automatically.

 
From Rewrite Rules to Bisimulation Congruences. Peter Sewell. Technical Report UCAM-CL-TR-444, University of Cambridge, June 1998. 72pp. [ bib | ps (cmr) | ps | pdf | .html ]
The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. This paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As a test of the theory it is shown that bisimulation for a fragment of CCS is recovered. The transitions generated for a fragment of the Ambient Calculus of Cardelli and Gordon, and for SKI combinators, are also discussed briefly.

 
Location Independence for Mobile Agents. Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce. In WIPL 1998, 6pp. [ bib | project page | ps | pdf ]
 
Nonaxiomatisability of Equivalences over Finite State Processes. Peter Sewell. Annals of Pure and Applied Logic, 90:163--191, December 1997. Invited submission from LICS '94. [ bib | doi | ps | pdf | http ]
This paper considers the existence of finite equational axiomatisations of behavioural equivalences over a calculus of finite state processes. To express even simple properties such as mu x E = mu x E[E/x] some notation for substitutions is required. Accordingly the calculus is embedded in a simply typed lambda calculus, allowing such schemas to be expressed as equations between terms containing first order variables. A notion of first order trace congruence over such terms is introduced and used to show that no finite set of such equations is sound and complete for any reasonable equivalence finer than trace equivalence. The intermediate results are then applied to give two nonaxiomatisability results over calculi of regular expressions.

 
Global/Local Subtyping for a Distributed π-calculus. Peter Sewell. Technical Report UCAM-CL-TR-435, Computer Laboratory, University of Cambridge, August 1997. 57pp. [ bib | ps (cmr) | ps | pdf | .html ]
In the design of mobile agent programming languages there is a tension between the implementation cost and the expressiveness of the communication mechanisms provided. This paper gives a static type system for a distributed pi-calculus in which the input and output capabilities of channels may be either global or local. This allows compile-time optimization where possible but retains the expressiveness of channel communication. Subtyping allows all communications to be invoked uniformly. Recursive types and products are included. The distributed pi-calculus used integrates location and migration primitives from the Distributed Join Calculus with asynchronous pi communication, taking a simple reduction semantics. Some alternative calculi are discussed.

 
On Implementations and Semantics of a Concurrent Programming Language. Peter Sewell. In CONCUR 1997. [ bib | doi | ps (cmr) | ps | pdf | http ]
The concurrency theory literature contains many proposals for models of process algebras. We consider an example application of the pi-calculus, the programming language Pict of Pierce and Turner, primarily in order to see how far it is possible to argue, from facts about the application, that some model is the most appropriate. We discuss informally the sense in which the semantics of Pict relates to the behaviour of actual implementations. Based on this we give an operational model of the interactions between a Pict implementation (considered as the abstract behaviour of a C program) and its environment (modelling an operating system and user). We then give a class of abstract machines and a definition of abstract machine correctness, using an adapted notion of testing, and prove that a sample abstract machine is indeed correct. We briefly discuss the standard of correctness appropriate for program transformations and the induced precongruence. Many of the semantic choices do indeed turn out to be determined by facts about Pict.

 
Design Rules and Abstractions (from branching and real time). Peter Sewell. In DCC96, ISBN 3--540--76102--0. The links are to an extended version. [ bib | ps | pdf ]
Three simple models of synchronous hardware are given; using linear discrete, branching discrete and branching real time. A simple notion of abstraction is introduced, motivated by the need to ultimately view such models as scientific theories that make empirical predictions. It makes the significance of design rules explicit.

Two abstractions from the branching discrete to the linear discrete model are given. They shed some light on the roles of consistency, deadlock and determinacy. The stronger of the two depends on a notion of dynamic type for processes which ensures deadlock freedom.

A reasonably strong abstraction from the branching real to the branching discrete model is given. This depends on a finer notion of type which is a reasonably physically plausible formalisation of the timing properties of certain real components.

 
The Algebra of Finite State Processes. Peter Michael Sewell. PhD thesis, University of Edinburgh, October 1995. Dept. of Computer Science technical report CST-118-95, also published as LFCS-95-328. [ bib | ps (cmr) | ps | pdf ]
This thesis is concerned with the algebraic theory of finite state processes. The processes we focus on are those given by a signature with prefix, summation and recursion, considered modulo strong bisimulation. We investigate their equational and implicational theories.

We first consider the existence of finite equational axiomatisations. In order to express an interesting class of equational axioms we embed the processes into a simply typed lambda calculus, allowing equation schemes with metasubstitutions to be expressed by pure equations. Two equivalences over the lambda terms are defined, an extensional equality and a higher order bisimulation. Under a restriction to first order variables these are shown to coincide and an examination of the coincidence shows that no finite equational axiomatisation of strong bisimulation can exist. We then encode the processes of Basic Process Algebra with iteration and zero (BPA_δ^*) into this lambda calculus and show that it too is not finitely equationally axiomatisable, in sharp contrast to the extant positive result for the fragment without zero.

For the implicational theory, we show the existence of finite computable complete sets of unifiers for finite sets of equations between processes (with zero order variables). It follows that the soundness of sequents over these is decidable.

Some applications to the theories of higher order process calculi and non-well-founded sets are made explicit.

 
Bisimulation is Not Finitely (First-Order) Equationally Axiomatisable. Peter M. Sewell. In LICS 1994, Subsumed by the APAL 1997 paper. [ bib | doi | ps | pdf | http ]
This paper considers the existence of finite equational axiomatisations of bisimulation over a calculus of finite state processes. To express even simple properties such as mu X E=mu X E[E/X] equationally it is necessary to use some notation for substitutions. Accordingly the calculus is embedded in a simply typed lambda calculus, allowing axioms such as the above to be written as equations of higher type rather than as equation schemes. Notions of higher order transition system and bisimulation are then defined and using them the nonexistence of finite axiomatisations containing at most first order variables is shown.

The same technique is then applied to calculi of star expressions containing a zero process --- in contrast to the positive result given in [FZ93] for BPA*, which differs only in that it does not contain a zero.

 
Investigation of the Wake Due to a Large Probe, using a Spatially Scanning Langmuir Probe. G. F. Matthews, P. C. Stangeby, and P. M. Sewell. J. Nucl. Mater., 145--147:220--224, February 1987. [ bib | http ]
This paper describes direct experimental investigation of the region of plasma perturbed by a probe. Two adjacent probes have been mounted on the DITE tokamak. The large 'disturber' probe is a rectangular graphite plate that creates the main particle flow pattern and can be biased with respect to the torus. The smaller 'search' Langmuir probe is located 0.5 m away on the same magnetic field line. It can be swept back and forth mechanically through the shadow of the main probe many times during each discharge. Through measurements of ion saturation current at many distinct radii, a complete map of the perturbed region has been built up and transformed into radial and poloidal coordinates. A numerical solution of the two-dimensional diffusion equations is compared with experimental data in the limiter shadow. Two zones of substantially different interconnection length are included in the model. The assumption of equal radial and poloidal cross-field diffusion coefficients (Dperpendicularto = 0.18 m2 s-1) is found to give a good fit with the data. (orig.)

 
The Optimisation of Limiter Geometry to Reduce Impurity Influx in Tokamaks. G. F. Matthews, G. M. McCracken, P. C. Stangeby, C. S. Pitcher, P. M. Sewell, and D. H. J. Goodall. Plasma Physics and Controlled Fusion, 29(2):189--203, February 1987. [ bib | http ]
The authors discuss the impurity control limiter (ICL) which has an inverted geometry. The ICL shape is designed to direct the impurities towards the wall. They present the results from a two-dimensional neutral particle code which maps the ionisation of carbon physically sputtered by deuterons from a carbon limiter. This ionisation source is coupled to a one-dimensional impurity transport code which calculates the implied central impurity density. The results demonstrate that the ICL achieves impurity control in two ways. Firstly, many of the sputtered impurities directed towards the wall are not ionised and return to the wall as neutrals. Secondly, much of the ionisation which does occur is located in the scrape-off layer. They conclude that a reduction in central impurity density of a factor of 10 is possible in a Tokamak such as DITE provided that the limiter is the main source of impurities.

 
The Determination of Sheath Potential from Retarding Field Analyser Measurements in Tokamak Edge Plasmas. G. F. Matthews, G. M. McCracken, P. M. Sewell, M. E. Woods, and B. J. Hopkins. J. Nucl. Mater., 145--147:225--230, February 1987. [ bib | http ]
Experimental measurements of the energy distributions of ions and electrons arriving at a surface in the boundary layer of a tokamak have been made with a retarding field analyser. The analyser uses a 9 μm entrance slit which is less than the Debye length for the plasma conditions investigated. The electron energy distributions are Maxwellian and the ion energy distributions are displaced Maxwellians, as expected. The sheath potential is derived from the ion energy distribution and found to be ∼2kTe, slowly decreasing with electron temperature. Measurements of secondary electron emission yield have been made on materials exposed in a tokamak as functions of incident electron energy and angle. This data have been integrated to obtain the effective yield of a full three-dimensional Maxwellian distribution. Using these results the theoretical sheath potentials have been calculated as functions of electron temperature and have been found in good agreement with the values that were measured directly.

 
An Investigation of the Secondary-Electron Emission of Carbon Samples Exposed to a Hydrogen Plasma. M. E. Woods, B. J. Hopkins, G. F. Matthews, G. M. McCracken, P. M. Sewell, and H. Fahrang. J. Physics D: Applied Physics, 20:1136--1142, 1987. [ bib | http ]
Measurements of secondary-electron-emission (SEE) yield are reported for samples of clean 5890 PT graphite and for the same material exposed for some months in the JET Tokamak. The samples exposed in the JET Tokamak give substantially higher values than the clean samples. Controlled experiments show that both implantation with H2+ ions and deposition of thin metal films increase the SEE yield. The experimental data have been integrated over a 3D Maxwellian distribution to obtain the values of effective SEE yield expected from a plasma as a function of electron temperature. From these SEE yields, theoretical values of sheath potential and sheath energy transmission factor have been calculated. The implications for ion sputtering and power loss are discussed.


This file was generated by bibtex2html 1.98.