Programming Languages and Systems: Seminars

Upcoming seminars

No seminars currently planned

Past seminars

Mutual Exclusion by Interpolation
Ms. Jael Kriener, School of Computing (homepage)

Monday 14th May 2012, 16:00 - 17:00, SW101

The question of what constraints must hold for a predicate to behave as a (partial) function, is key to understanding the behaviour of a logic program. It has been shown how this question can be answered by combining backward analysis, a form of analysis that propagates determinacy requirements against the control flow, with a component for deriving so-called mutual exclusion conditions. The latter infers conditions sufficient to ensure that if one clause yields an answer then another cannot. This paper addresses the challenge of how to compute these conditions by showing that this problem can be reformulated as that of vertex enumeration. Whilst directly applicable in logic programming, the method might well also find application in reasoning about type classes.
Comparing Dynamic and Static Language Approaches to Web Frameworks
Dr. Neil Brown, School of Computing (homepage)

Monday 30th April 2012, 16:00 - 17:00, SW101

Most websites have a similar set of technical requirements: generating HTML, mapping URLs to/from actions, accepting input via forms, and manipulating an underlying database. Many web frameworks have been created to aid in developing such sites, to speed-up development and reduce boilerplate. Ruby on Rails is one of the most notable, using Ruby, with dynamic typing and run-time method creation. At the opposite end of the scale, Yesod (a Haskell framework) supports similar functionality but uses Haskell, with static typing, and compile-time metaprogramming. This talk will explore the two different approaches to designing a web framework, and will examine the advantages and pitfalls of both Rails and Yesod.
Hardware-based, high throughput regular expression pattern matching, for network intrusion detection systems
Mr Bala Modi, University of Kent (homepage)

Monday 23rd April 2012, 16:00 - 17:00, SW101

Network attacks or intrusions flow through the firewall or network intrusion detection systems of an organisations’ network, mostly identifiable by strings or patterns of data that they contain. This project seeks to develop a viable automaton, designed to detect variations in these patterns represented by complex regular expressions; at a very high throughput, with minimal overheads. These overhead costs may include; area and resource utilization, in terms of the number of utilized registers, LUTs, Slices etc. The approach here involves exploring a proposed less complex input compression technique, called equivalent class decoding (ECD), by driving the automation using ECD index nunmbers (integers), which then allows the compressed inputs to be fanned out to the NFA (Non-determininistic Finite Automata) tree as opposed to DFA (Deterministic Finite Automata). The preliminary (1st yr) results obtained from the minimized non-ECD-NFAs show promising results in comparison to some previous papers so far.
Experiences of implementing a VM with RPython
Dr Laurence Tratt, King's College London (homepage)

Friday 20th April 2012, 14:00 - 15:00, SW101

Programming language designers face a horrible dilemma when it comes to implementing their languages: too little implementation, and it will be laughed at as too slow; too much, and it will divert energy away from design. Lacking the manpower to make a plausibly fast implementation, many interesting language design ideas have faded unfairly into obscurity.
In this talk I look at a new mode of creating "fast enough virtual machines in fast enough time" Virtual Machines (VMs), using the meta-tracing JIT language RPython. Unlike previous approaches, RPython creates VMs that automatically come with a JIT customised for the language being interpreted. RPython has been used to implement a new VM for Python that gives an average speed-up of 5x over the stock VM, and thus demonstrably scales to "real" languages.
I will share my experiences of creating an RPython VM for the Converge language (http://convergepl.org/) to replace the existing C VM. The new VM executes between 3x and 10x faster than the old VM, despite taking significantly less work to create.
I will outline: how RPython works; what a VM created using it looks like; the trade-offs of using RPython; as well as thoughts for the future of similar approaches.
Practical Typed Lazy Contracts
Dr. Olaf Chitil, School of Computing (homepage)

Monday 20th February 2012, 16:00 - 17:00, SW101

TBA
Self-Verifying Concurrent Programming
Professor Peter Welch, School of Computing (homepage)

Monday 13th February 2012, 16:00 - 17:00, SW101

This is a proposal to enable the formal verification of occam-pi concurrent systems entirely within the programming language. occam-pi will be extended with qualifiers on types and processes (to indicate relevance for verification and/or execution) and assertions about refinement (including deadlock, livelock and determinism). The compiler will abstract a set of CSP equations and assertions, delegate their analysis to the FDR2 model checker and report back in terms related to the occam-pi source. The rules for mapping the extended occam-pi to CSP are given. The full range of CSP model-checking assertions becomes accessible, with no knowledge of CSP algebra required by the (occam-pi) programmer. Program properties will be verified by writing and compiling programs, supported sometimes with modest external reasoning -- the heavy lifting being done by the compiler and model checker. Our ambition is for the formal analysis of computer systems to become part of normal (and, ultimately, required) engineering design and programming practice, thereby significantly improving safety and correctness.
A case-study analysing a new and elegant solution to the Dining Philosophers problem is presented, using the verification extensions proposed for occam-pi. Deadlock-freedom for colleges with any number of philosophers is established by verifying an induction argument. Finally, the careful use of model compression is demonstrated to verify directly the deadlock-freedom of an occam-pi college with 102000 philosophers (in around 10 seconds). All we need is a universe large enough to contain the computer on which to run the system.
Combined with its safe, scalable and dynamic concurrency model, its industrial strength set of support libraries and its ultra-efficient multicore process scheduler, self-verification gives occam-pi a unique set of capabilities for building the massively complex systems needed tomorrow.
Topological Models
Dr. Stefan Kahrs, School of Computing (homepage)

Monday 6th February 2012, 16:00 - 17:00, SW101

Playing around with the semantics for infinitary term rewriting, I noticed that topological spaces are tremendously flexible when it comes to constructing models for pieces of syntax. As these are insights that apply quite widely to the interpretation of other pieces of infinitary syntax (process traces, recursion unfolding, etc.) I thought I might share them with the group.
TBA
Mr. Martin Ellis, School of Computing (homepage)

Monday 30th January 2012, 16:00 - 17:00, SW101

TBA
Addressing Random Effects in Experimental Performance Evaluation
Dr. Tomas Kalibera, School of Computing (homepage)

Monday 23rd January 2012, 16:00 - 17:00, SW101

Experimental performance evaluation is based on running benchmark programs on a system of interest and measuring their execution time. The benchmarks are selected to represent a particular application domain and the hope is that the measured performance would hence be relevant of (most) applications from that domain. Unfortunately, the execution time of a benchmark is not deterministic on current systems. It is prone to random fluctuations coming from the physical world, hardware design, and complex or even randomised algorithms in the operating system or libraries.
Experimental performance evaluation is a prevalent evaluation technique in systems research. It has to take the random fluctuations into account, otherwise results could mislead the field. It turns out that a large proportion of systems research papers published at top venues, however, ignores random fluctuations entirely. Moreover, the current best-recommended practice in the field for conducting experiments has a number of limitations, some of which have been known to statisticians for over seven decades. A better recommendation is needed, and can base on more recent results in statistics and on recommendations in other fields of science. Still, no such recommendations can completely rule out misleading results. As the last line of defence, we can take one more inspiration from the other fields: do and publish independent reproduction studies.
Dynamic Plans for Integration Testing of Self-adaptive Software Systems
Mr. Carlos da Silva, School of Computing (homepage)

Monday 12th December 2011, 16:00 - 17:00, SW101

Self-adaptive software systems are able to modify their own structure and/or behaviour at run-time in order to cope with changes. For example, during software self-adaptation, new components may be incorporated to the software system. One crucial aspect when incorporating new components is to test them for guaranteeing that they can interoperate as specified. However, this aspect has been often neglected when considering architectural reconfiguration.
In this talk, we present an approach for the dynamic generation of plans for conducting the integration testing of self-adaptive software systems. The approach is based on our framework for the automatic generation of processes based on the use of workflows, model-based and artificial intelligence planning techniques.
* This talk is based on our paper presented last May on SEAMS2011.
Cognition, Concurrency Theory and Reverberations in the Brain: In search of a Calculus of Communicating Neural Systems
Professor Howard Bowman, School of Computing (homepage)

Monday 5th December 2011, 16:00 - 17:00, SW101

The brain is clearly a highly parallel, distributed system. In addition, theories of cognition often conceptualise the mind as a set of independent and concurrently executing modules, e.g. Barnard's Interacting Cognitive Subsystems. One might then expect that concurrency theory (e.g. Process Calculi, Communicating Automata and Temporal Logics), as formulated in Computer Science, could be beneficially applied to Cognitive Neuroscience, which attempts to put mind and brain together. In particular, related (although probably far harder) problems of scale arise with the brain, as arise in Computer Systems Engineering. Thus, Concurrency Theory's attempt to address these scale problems should be expected to be of value in Cognitive Neuroscience. Accordingly, I will consider two directions in which such application of Concurrency Theory could be made: 1) compositional construction of neural models, and 2) model checking stability properties of neurophysiologically (more) realistic learning algorithms. My conclusions will centre on the difficulty inherent in the first of these and the promise of the second.
DIY Refactoring in Wrangler
Professor Simon Thompson, School of Computing (homepage)

Monday 28th November 2011, 16:00 - 17:00, SW101

Wrangler is an Erlang refactoring tool which provides a range of refactorings - including renaming, function extraction and generalisation - as well as facilities for clone detection and removal as well as improvement of the module structure of projects. Wrangler is integrated into emacs and Eclipse, via ErlIDE.
Up to now, you could only use the refactorings built into Wrangler, or dive deep into the internals to extend it. The latest version of Wrangler now provides a much easier way of defining and applying refactorings for yourself. All you need to do is implement them as a refactoring behaviour and they are accessible in emacs, and you can write descriptions of what the refactorings do using a combination of Erlang macros and templates that describe the particular changes to be made. You can also use the same facilities write new forms of code inspection equally easily.
As well as being able to write new refactorings from scratch, we're providing a scripting language in which you can build complex refactorings by putting together simpler components: this can, for example, provide a mechanism for migrating from an old to a new API, or for transforming the data type forming the input/output of a collection of functions.
This talk will describe and demonstrate these new additions to Wrangler.
On Instrumenting a JVM: -
Mr. Matthew Mole, School of Computing (homepage)

Monday 21st November 2011, 16:00 - 17:00, SW101

In this talk, I will be talking about the process of instrumenting a Java Virtual Machine. I will discuss my recent instrumentation to a JVM, including how it is done and the problems I have encountered. In the latter part of the talk I will describe what I am logging, why, and how it will be processed.
Paraforming: Forming Parallel Haskell Programs Using Novel Refactoring Techniques: -
Dr Chris Brown, University of St Andrews (homepage)

Monday 14th November 2011, 16:00 - 17:00, SW101

Enabling programmers to "think parallel'' is critical if we are to be able to effectively exploit future multicore/manycore architectures. In this talk I will introduce paraforming: a new approach to constructing parallel functional programs using formally-defined refactoring transformations. I will introduce a number of new refactorings for Parallel Haskell that capture common parallel abstractions, such as divide-and-conquer and data parallelism, and show how these can be used by HaRe, the Haskell Refactorer.
Using a paraforming approach, we are able to easily obtain significant and scalable speedups (up to 7.8 on an 8-core machine).
First-Class Type Classes and Proof Search
Dr Matthieu Sozeau, INRIA, Paris (homepage)

Monday 7th November 2011, 16:00 - 17:00, SW101

Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for specifying with abstract structures by quantification on contexts. However, both systems are limited by second-class implementations of these constructs, and these limitations are only overcomed by ad-hoc extensions to the respective systems. We propose an embedding of type classes into a dependent type theory that is first-class and supports some of the most popular extensions right away. The implementation is correspondingly cheap, general and very well integrated inside the system, as we have experimented in Coq. We show how it can be used to help structured programming and proving by way of examples.
Type classes rely on a general dfs proof-search algorithm, extensible with arbitrary tactics. We're seeking ways to make the system more predictable and efficient, imposing some healthy constraints on selected classes (which can be thought of as predicates). Hence our interest in techniques from logic programming. I'll discuss the current issues we're encountering in this respect.
A Taste of Theorem Proving
Ms. Jael Kriener, School of Computing (homepage)

Monday 31st October 2011, 16:00 - 17:00, SW101

Interactive Theorem Proving is an exiting and growing field. The aim of this talk is to give a you a taste of it. I will begin by briefly presenting some of the main theoretical motivation behind the scenes and then quickly dive in to go through a real-life example of certified programming in Coq.
I'm hoping this will be more of an interactive session than a formal presentation. If you would like to go for the "hands-on experience", I encourage you to install Coq before the seminar (available from: http://coq.inria.fr/) and go through the example with me, so that at 5pm you can claim that you formally verified a piece of code.
Existential Quantification as Incremental SAT
Dr. Andy King, School of Computing (homepage)

Monday 24th October 2011, 16:00 - 17:00, SW101

Elegant ideas and careful engineering have advanced DPLL-based SAT solvers to the point they can rapidly decide the satisfiability of structured problems that involve many thousands of variables. SAT has thus been applied to the problem of existential quantifier elimination, yet existing algorithms are considered to be "inelegant"
In this work we propose a simple algorithm for eliminating variables from a propositional formula that is presented in CNF, which is based on incremental SAT solving and the enumeration of prime implications. The technique does not use BDDs, is embarrassingly simple to implement, and dovetails with modern SAT solvers that are based on learning.
Since the paper appeared in the summer at CAV'11, the algorithm has been deployed by hardware and software engineers at the University of Tuebingen, University of Illinois, NUS University, Singapore University of Technology and Design, Princeton, Irdeto, Northeastern University and the Technical University of Munich.
This is joint work with Joerg Brauer and Jael Kriener
Parallel Programming for Internet Clients
Dr. Adam Welc, Adobe (Advanced Technology Lab) (homepage)

Friday 29th July 2011, 14:00 - 15:00, SW101

In the first part of the talk I present an overview of how parallelism is supported by today's Internet client programming techniques. The description is based on one of the most popular programming languages for Internet clients, namely JavaScript, and set in the context of the emerging HTML5 standard. I will then present some ideas on how certain limitations of the current approach can be addressed. Finally, I will talk about what Adobe is doing to make ActionScript, a close cousin of JavaScript, a programming language of choice for present and future Internet client applications.
Semantics-Based Design of Modular Type Inferences that Deliver Best Types: Hindley-Milner and Beyond
Dr. Axel Simon, TU Muenchen (homepage)

Monday 25th July 2011, 10:00 - 11:00, SW101

The steady increase in expressiveness of type systems tends to clutter code with an excessive amount of type information which calls for the use of type inference. Several people have argued that a type inference should infer the best types possible within the given type discipline. We systematically construct such an inference for the Hindley-Milner type system by recasting type inference as a program analysis problem: We apply abstract interpretation theory to a denotational semantics and obtain typing rules that are correct by construction and abstract-complete in that they infer the best types. The resulting rules are a variant of Henglein's semi-unification--based inference rules. The notion of ``abstract complete'' is weaker than ``principal typings'' but we argue that the former delivers the same advantages and that the latter is not type system-agnostic.
We then observe that the Hindley-Milner type system is modular and reduce this fact to three properties developed in the abstract interpretation literature, namely, complete transfer functions, a complete projection operation and a condensing domain. Given the state-of-the-art, only two abstract domains feature these properties while remaining tractable, namely Herbrand abstractions and Boolean functions. We conclude that any modular type inference that infers principal typings must be based on these two domains.
Applying Agda in Model-Driven Design
Georg Struth, University of Sheffield (homepage)

Monday 20th June 2011, 16:00 - 17:00, SW101

Agda is a dependently typed functional programming language cum interactive theorem prover. Since proofs are programs, it lends itself ideally for formal program development and construction tasks. However, Agda is still at a very experimental stage and user interaction is needed even for the most basic proof obligations.
Our aim is to probe Agda's potential in formal object-oriented software engineering, deriving model transformations from specifications while proving their correctness. The first step of this project has been the integration of the automated theorem prover Waldmeister into Agda. We report on this integration and outline opportunities for future work in this direction. We then present a formalisation of object-oriented meta-model specifications in Agda, as well as first steps towards the development of concrete transformations in this setting. Finally we outline ongoing work intended to enable users to formally develop model transformations that are provably correct, and with a high degree of automation.
This talk is based on joint work with Simon Foster, John Derrick, Tony Simons (Sheffield) and Ondrej Rypacek (Kings College)
Adaptive Structured Parallelism for Heterogeneous Architectures
Dr. Horacio González-Vélez, Robert Gordon University (homepage)

Thursday 26th May 2011, 14:00 - 15:00, SW101

Algorithmic skeletons abstract commonly-used patterns of parallel computation, communication, and interaction. By using skeletons, programmers can code programs regardless of how the computation and communications will be executed, leading to significant savings of human and computing effort.
This talk presents an overview of a methodology to efficiently program parallel applications for heterogeneous architectures such as multicore CPUs and GPUs by introducing adaptivity through resource awareness. It incorporates structural information into a parallel application that helps it to adapt to the most suitable computing resources, minimising the associated costs and time.
Software - Design and Performance
Dr Matthias Hauswirth, University of Lugano (USI), Switzerland (homepage)

Monday 23rd May 2011, 16:00 - 17:00, SW101

This talk consists of two parts: the first part, based on our ECOOP'11 paper on "essence", focuses on software design, and the second part, based on our recently launched ParaBoost project, focuses on using concurrency to improve software performance.
In the first part of this talk we present an approach that partitions a software system into its algorithmically essential parts and the parts that manifest its design. Our approach is inspired by the notion of an algorithm and its asymptotic complexity. However, we do not propose a metric for measuring asymptotic complexity (efficiency). Instead, we use the one aspect of algorithms that drives up their asymptotic complexity -- repetition, in the form of loops and recursions -- to determine the algorithmically essential parts of a software system. Those parts of a system that are not algorithmically essential represent aspects of the design. A large fraction of inessential parts is indicative of "overdesign", while a small fraction indicates a lack of modularization. We present a metric, relative essence, to quantify the fraction of the program that is algorithmically essential. We evaluate our approach by studying the algorithmic essence of a large corpus of software systems, and by comparing the measured essence to an intuitive view of design "overhead".
In the second part of the talk we present the recently launched ParaBoost project in which we are exploring approaches to benefit from the ever increasing core count in modern processors without requiring the explicit parallelization of applications. The project is based on the existing idea of competitive parallel execution (CPE). CPE lets multiple algorithms compete, each on its own core, on solving the same problem. The algorithm that finds the solution first wins the competition. The competition thus takes only as long as the fastest concurrently executing algorithm. In the ParaBoost project, we combine this idea of concurrently competing algorithm variants with the software engineering benefits afforded by modern programming languages. We are creating a managed runtime environment called a multi-variant virtual machine (MVVM), to enable existing Java software to benefit from multi-variant execution. By lifting multi-variant execution into the language runtime, we will gain fine-grained control over the execution of the variants. This control will allow us to go beyond existing CPE approaches: The MVVM will be able to competitively execute software that uses more than one thread, it will improve performance by dynamically allocating more time to more promising variants, and it will learn and use models predicting the performance of variants based on features of their input.
About the speaker:
Matthias Hauswirth is an assistant professor at the Faculty of Informatics at the University of Lugano (Switzerland), where he leads the Software and Programmer Efficiency (Sape) research group. He is interested in performance measurement, understanding, and optimization. Matthias received his PhD from the University of Colorado at Boulder.
Student Project Presentation: A Sound Library for Learning Haskell
Mr. Benedikt Boehm, University of Kent

Monday 4th April 2011, 16:00 - 16:30, SW101

The project is designed to be used by first or second year computer science students that have little or no functional programing experience. Students are to familiarize themselves with Haskell language features and syntax in a light-hearted manner.
The user will be able to generate custom sounds waves. These sound waves or samples are initially represented as a list of Doubles and can be manipulated in several ways. By manipulation the samples, the user is supposed to familiarize him or herself with the Haskell Language. By the use of additional integrated functions, the user can create more interesting samples.
Student Project Presentation: Replicated Process Distribution for Fault Tolerant Systems
Mr. Ross Hayes, University of Kent

Monday 4th April 2011, 16:30 - 17:00, SW101

In this presentation I will discuss my work creating a fault-tolerant process distribution framework for concurrent Java programs using JCSP. The aim of this framework is to enable programmers to take advantage of process distribution over networked computers, without significant modification to standard JCSP code. The presentation will focus on the distribution framework and the rationale for its design.
Investigating the effect of finalisation on barrier locality.
Mr. Matthew Mole, School of Computing (homepage)

Monday 28th March 2011, 16:00 - 17:00, SW101

With concurrent garbage collection mutator threads should be free to make changes to the heap whilst a garbage collector thread is running. To preserve correctness, the garbage collector needs to be informed about these changes. One such strategy is to use barriers.
This work presents an extension to research conducted on barrier locality. If a barrier is triggered, an object must be loaded into the cache. Therefore the barrier strategy may have an effect on the cache. This work focuses on finalisation in Java, how it affects locality, and presents some of the findings so far.
In the second part of the talk, we present some ideas for improving concurrent garbage collection.
Object Store Based Simulation Interworking
Mr. Carl Ritson, School of Computing (homepage)

Monday 21st March 2011, 16:00 - 17:00, SW101

The CoSMoS project is building generic modelling tools and simulation techniques for complex systems. As part of this project a number of simulations have been developed in many programming languages. This paper describes a framework for interconnecting simulation components written in different programming languages. These simulation components are synchronised and coupled using a shared object space. This approach allows us to combine highly concurrent agent-based simulations written in occam-pi, with visualisation and analysis components written in flexible scripting languages such as Python and domain specific languages such as MATLAB
Structuring Design using Viewpoints
Professor Peter Linington, School of Computing (homepage)

Monday 7th March 2011, 16:00 - 17:00, SW101

Many architectures proposed for large systems have used the idea of viewpoints to manage complexity and separate stakeholder concerns. The talk focuses on one such, the Reference Model for Open Distributed Processing, which is a well-known standard framework.
Such frameworks have, in the past, proved to be a fruitful area for the study of consistency between related specifications. Recently, there has been discussion of how different viewpoint ideas ar related, centred on the work of IEEE project 1471.
The talk revisits viewpoints, looking at a broader view of the way correspondences between viewpoints are expressed and interpreted, and how composition of viewpoints can be categorized in terms of patterns of design activity. These can be related to ideas on model driven engineering.
Towards Safer Concurrent Device Drivers.
Mr. Martin Ellis, School of Computing (homepage)

Monday 28th February 2011, 16:00 - 17:00, SW101

Many tools exists for writing safe and correct device drivers for conventional operating systems. From runtime driver management layers which try and detect errors and recover from them, to static analysis systems like SLAM.
Unfortunately these tools do not map well to the concurrent drivers we write for RMoX. My talk will look at how we can build safe and correct device drivers, using the traditional occam analysis tools such as CSP.
Traffic discovery using VANETs
Mr. Mariusz Saternus, School of Computing (homepage)

Monday 21st February 2011, 16:00 - 17:00, SW101

A Vehicular Ad-Hoc Network (VANET) is a form of Mobile ad-hoc network. It is a self-configuring network of vehicles as well as road side infrastucture connected by wireless links. Movement of nodes in such a network is bound by the topology of the underlying road network.
One of the key VANET research areas is traffic detection and dissemination. In my talk I will give a cross section of how this is achieved using various approaches highlighting their advantages and disadvantages. Finally I will present our solution based on the VANET technology to the traffic detection problem.
A DSL for Describing Refactorings [preliminary title]
Mr László Károly Láng, Eötvös Loránd University, Budapest, Hungary

Friday 18th February 2011, 16:00 - 17:00, SW101

Refactorings provide a safe way to improve the structure of our programs. Wrangler like most refactoring tools provides a set of predefined refactorings for programmers, but cannot have every possible refactoring that the users could need. Thus there is a need for a tool that can help programmers to create their own refactorings in a relatively simple way.
In my talk I will describe the high level API (or DSL) I designed for Wrangler, which can be used to define refactorings for Erlang programs. My tool provides queries to gather information about the code, and to select components of the program. Conditions can be added to the refactorings. The modifications on the code are described with transformation rules, which are applied on subtrees of the syntax tree. Finally I will present some refactoring examples created in the API.
Towards a New Language for Concurrent Programming
Dr. Fred Barnes, School of Computing (homepage)

Monday 31st January 2011, 16:00 - 17:00, SW101

In this talk I will discuss the ongoing development of a new concurrent programming language code-named "Guppy". The language itself will be a probable successor to occam and occam-pi, retaining the good features therein while incorporating a wealth of modern programming language ideas such as flexible typing, compile-time polymorphism, exception handling and lower-case keywords.
The language itself provides abstractions for concurrency, including parallelism, channel communication and barrier synchronisation, in much the same way that occam-pi currently does, but without the inconsistencies. Compiler development is still at an early stage but is progressing; the current aim is to generate LLVM (essentially an architecture independent assembler) code that targets the existing high-performance run-time system used by occam-pi in KRoC. Suggestions regarding "better" ways to do or represent things in the language, or entirely new features, would be very welcome.
Supercompilation by Evaluation
Max Bolingbroke, University of Cambridge (homepage)

Monday 24th January 2011, 16:00 - 17:00, SW101

(Joint work with Simon Peyton Jones)
Supercompilation is a powerful program transformation technique which can be used to both automatically prove theorems about programs and greatly improve the efficiency with which they execute. Despite its remarkable power, the transformation is simple, principled and fully automatic. Supercompilation is closely related to partial evaluation, but can achieve strictly more optimising transformations.
I intend to give an introduction to supercompilation for those new to the topic, using the framework from our Haskell Symposium paper. I will also discuss our latest improvements to the supercompilation process: depending on the time available, I will try to cover:
* The use of speculative evaluation strategies to improve information propagation
* Rolling back the supercompilation process when it proves fruitless
* A method of controlling the code bloat caused by the supercompilation process
From Test Cases to FSMs: Augmented Test-driven Development and Property Inference
Professor Simon Thompson, School of Computing (homepage)

Monday 17th January 2011, 16:00 - 16:30, SW101

This paper uses the inference of finite state machines from EUnit test suites for Erlang programs to make two contributions. First, we show that the inferred FSMs provide feedback on the adequacy of the test suite that is developed incrementally during the test-driven development of a system. This is novel because the feedback we give is _independent_ of the implementation of the system.
Secondly, we use FSM inference to develop QuickCheck properties for testing state-based systems. This has the effect of transforming a fixed set of tests into a property which can be tested using randomly generated data, substantially widening the coverage and scope of the tests.
[Joined work with Thomas Arts (Chalmers / Quviq AB). Paper presented at Erlang Workshop 2010]
Transfer Function Synthesis without Quantifier Elimination
Dr. Andy King, School of Computing (homepage)

Monday 13th December 2010, 16:00 - 17:00, SW101

Sometimes the time is right: technologies mature to a point that researchers are able to apply these techniques to a class of problem that was previously considered out of reach. One particular case in point is the problem of transfer function synthesis, and recently researchers have started to hammer away at this problem using SAT solving and elimination algorithms.
Transfer function synthesis is the problem of taking a sequence of arbitrary instructions and working out a function that models their behaviour as a whole. The function is required to map an abstraction to abstraction, where an abstraction might be something such as an interval or a geometric object such as an octagon. The problem is particularly important in reverse engineering and verifying the correctness of assembler programs for embedded applications.
Monniaux, in his recent POPL paper, showed how this problem can tackled by quantifier limitation over linear constraints. King and Brauer showed in their recent SAS paper how this problem can also be solved by quantifier elimination over Boolean formulae which is computationally more attractive. Now these same guys have shown in their forthcoming ESOP paper, how the problem can be reduced to repeated SAT solving, which is embarrassing simple, and enables transfer functions to be automatically synthesised for 32- and 64-bit architectures. We shall illustrate the ideas using AVR assembler, which is popular in embedded systems, though the ideas are completely generic.
Trace-based Just-in-time Compilation - An Introduction
Mr. Thomas Schilling, School of Computing (homepage)

Monday 15th November 2010, 16:00 - 17:00, SW101

Just-in-time compilation, e.g., as popularised by the Java Virtual Machine (JVM), has become a commonly used technique to improve the performance of bytecode languages or so-called ``dynamic'' languages such as Javascript, Python, or Ruby.
The JVM uses a method-based JIT where the compilation unit comprises a single method. Many recent implementations of JIT compilers, like Mozilla's Jaegermonkey, Google's Dalvik VM, and LuaJIT 2, are trace-based JITs. These JITs only compile a single execution path, a trace, at a time which simplifies the JIT compiler and reduces the amount of generated machine code. Multiple traces can be composed into trace trees.
This talk will give an overview of trace-based JIT compilation, its advantages and disadvantages.
Quadtrees as an Abstract Domain
Dr. Andy King, School of Computing (homepage)

Monday 8th November 2010, 16:00 - 16:30, SW101

Quadtrees have proved popular in computer graphics and spatial databases as a way of representing regions in two dimensional space. This hierarchical data-structure is flexible enough to support non- convex and even disconnected regions, therefore it is natural to ask whether this data-structure can form the basis of an abstract domain. This talk explores this question and suggests that quadtrees offer a new approach to weakly relational domains whilst their hierarchical structure naturally lends itself to representation with Boolean functions. This talk will include a lot of diagrams but not much maths.
Research Funding Advice
Dr. Andy King, School of Computing (homepage)

Monday 1st November 2010, 16:00 - 17:00, SW101

Juan and Jo from Research Services will give an introduction to the FP7 Co-operation programme, and explain the basics of STREP applications. Jo will give a summary of the guidance given by UKRO to help you craft a successful proposal, and Juan will be able to answer questions on costings and contracts.
Building Refactoring Tools for Functional Languages
Professor Simon Thompson, School of Computing (homepage)

Monday 25th October 2010, 16:00 - 17:00, SW101

Refactoring is the process of changing the design of a program without changing what it does. Typical refactorings, such as function extraction and generalisation, are intended to make a program more amenable to extension, more comprehensible and so on. Refactorings differ from other sorts of program transformation in being applied to source code (rather than within the bowels of a compiler), and in having an effect across a code base. Because of this, there is a need to give (semi-)automated support to the process.
This talk will reflect on our experience of building tools to refactor functional programs written in Haskell (HaRe) and Erlang (Wrangler). In doing this we will address system design, the pragmatics of system take-up, as well as contrasting the style of refactoring and tooling for Haskell and Erlang.
Range and Set Abstraction using SAT
Mr. Edward Barrett, School of Computing (homepage)

Monday 18th October 2010, 16:00 - 16:40, SW101

When applying static analysis to machine code, a suitable abstraction can simplify the analysis. Abstracting programs into Boolean formulae allows us to describe precisely (at a bit level), the semantics of a program, including the subtle interactions between register values and status flags.
Unfortunately, traditional techniques for enumerating satisfiable models of Boolean formulae do not scale. In this talk, we describe: (a) a way to quickly infer an (over)approximation value ranges a register may assume, and (b) a way to refine this approximation further, to converge onto a precise abstraction when applied repeatedly.
Real-time Java and Real-time Garbage Collection
Dr. Tomas Kalibera, School of Computing (homepage)

Monday 11th October 2010, 16:00 - 17:00, SW101

In real-time systems, timing is part of correctness. As timing is hard to verify, current real-time systems tend to use simple hardware, outdated programming techniques, and outdated languages. This solution however does not scale - the increasing demand for real-time systems and their increasing complexity requires new technologies. Real-time Java might be one of them. The interesting features of Java desirable for real-time systems include dynamic allocation, garbage collection, type safety, and integrated multi-threading. Java is known to a high number of programmers and has a rich library and tool support. Real-time Specification for Java (RTSJ) extends the Java Virtual Machine and Java APIs with support for real-time applications. Despite several successful demonstrator case studies, significant research and engineering challenges remain: repeatability, real-time garbage collection, and footprint.
In standard Java, the garbage collector can stop the application to do its work when memory is replenished. A real-time garbage collector must, however, be interruptible by the application at any time. This includes the time when the collector is moving objects in memory in order to reduce fragmentation. Another hard problem is scheduling. If the collector gets too much CPU, the application may miss its deadlines. If it gets too little, the system may run out of memory and crash.
Infinitary Rewriting Revisited II - Models & Equivalences
Dr. Stefan Kahrs, School of Computing (homepage)

Monday 4th October 2010, 16:00 - 17:00, SW101

Term rewriting is a syntactic world where the objects under our consideration are very syntactic. Although infinitary rewriting changes this slightly by employing semantic constructions to "complete" various syntactic bits, it is still intrinsically syntactic.
However, when reasoning about rewriting we employ models, and this raises questions how well syntax and semantics fit together. The iTRS literature is full of failed attempts for a decent notion of model. The talk will present another one, and discuss links that hark back to the syntax.
Wireless Sensor Networks for River Monitoring
Jo Ueyama, USP Sao Carlos, Brazil

Friday 16th July 2010, 14:00 - 15:00, S110B

Wireless Sensor Networks (WSN) are composed of embedded computers equipped with sensors, actuators and wireless networking facilities. In recent years, WSN have been applied to tackle a number of critical problems including: environmental monitoring, energy conservation and industrial automation. This seminar will discuss the author's previous work in providing middleware support for WSN-based flood monitoring systems in the North West of England. The seminar will conclude with discussion of the author's current work in deploying a flood monitoring and warning system in the state of Sao Paulo. This work has been featured in a number of newspapers and TV programs (in Brazil) reporting our recent results.
The Locality of Concurrent Write Barriers
Mr. Laurence Hellyer, School of Computing (homepage)

Thursday 27th May 2010, 11:00 - 11:30, S110B

Concurrent and incremental collectors require barriers to ensure correct synchronisation between mutator and collector. The overheads imposed by particular barriers on particular systems have been widely studied. Somewhat fewer studies have also compared barriers in terms of their termination properties or the volume of floating garbage they generate. Until now, the consequences for locality of different barrier choices has not been studied, although locality will be of increasing importance for emerging architectures. This talk provides a study of the locality of concurrent write barriers, independent of the processor architecture, virtual machine, compiler or garbage collection algorithm.
The Economics of Garbage Collection
Professor Richard Jones, School of Computing (homepage)

Thursday 27th May 2010, 11:30 - 12:00, S110B

We argue that economic theory can improve our understanding of memory management. We introduce the allocation curve, as an analogue of the demand curve from microeconomics. An allocation curve for a program characterises how the amount of garbage collection activity required during its execution varies in relation to the heap size associated with that program. The standard treatment of microeconomic demand curves (shifts and elasticity) can be applied directly and intuitively to our new allocation curves. As an application of this new theory, we show how allocation elasticity can be used to control the heap growth rate for variable sized heaps in Jikes RVM.
Channel I/O for Modern Virtualisation
Mr. Chris Girling, School of Computing

Thursday 27th May 2010, 16:00 - 16:30, S110B

This seminar gives an overview of the I/O techniques used by current virtual machine software, and looks at ways that they can be improved using concepts taken from the world of mainframes.

Download slides (PDF)
Templated Arithmetic in CXXR
Mr. Sam Nicholls, School of Computing

Thursday 20th May 2010, 16:00 - 16:30, S110B

This seminar is about CXXR - a C++ refactorisation of the existing R software, which is an interpreter for the R statistical computing language. It will outline what R is, the problems with it that lead to the conception of CXXR, then go in to some detail regarding the refactoring of the program's internal arithmetic routines using C++ templates.

Download Slides
Phobos: An operating system teaching aid for undergraduate students
Mr. Matthew Mole, School of Computing

Thursday 13th May 2010, 16:00 - 16:30, S110B

This presentation outlines the current status of Phobos, an operating system intended as a teaching aid for undergraduate students, including the achievements of the project, the outstanding issues, and some potential future extensions.
Re-Envisioning the Haskell Horse
Mr. David Jupp, School of Computing

Thursday 8th April 2010, 16:00 - 16:30, S110B

The computer science department at the University of Kent has for some years been teaching a course on Haskell based on the book 'Haskell: The art of functional programming' written by Simon Thompson. The book discusses the manipulation of ASCII images as a method of introducing functional programming, in particular a simple ASCII graphical representation of a horse. However students are not easily impressed by ASCII art, and replacing it proved to be difficult due to a combination of poor library availability, compatibility, and stability both of execution and of interface. Recently the situation has begun to improve to an extent where it is felt a serious attempt can be made to update the ASCII horse to something more interesting.
Beyond Hierarchical Binning: Improving Radio Signal Propagation in Simulation
Mr. Mariusz Saternus, School of Computing (homepage)

Monday 22nd March 2010, 16:00 - 17:00, S110B

Modelling radio signal propagation in a VANET simulation is computationally a very intensive task. Network simulators such as JiST/SWANS and NS2 use algorithms that are designed to improve this situation. These algorithms however are aimed at MANET simulation scenarios of which VANETs are a specific subset. Therefore we believe that a different approach to radio signal propagation could be taken, one designed with VANET specific characteristics in mind.
In this talk I will outline the existing solutions to the above problem and present our own altogether with any relevant terminology. This concept is part of a VANET simulator which we are currently writing and planning to use for future research, therefore any feedback will be most welcome.
Homicidal Code: Static Detection and GC Exploitation
Mr. Robert Bunyan, School of Computing (homepage)

Monday 15th March 2010, 16:00 - 17:00, S110B

Generational Garbage Collection handles short-lived objects very successfully, but does less well with longer lived objects, which may either be processed many times or are left in older generations long after they are dead, thereby wasting space. Ideally, a generational collector should process an object only once. We attempt to improve generational garbage collection by guiding the collector to areas of the mature space that contain a high proportion of dead objects which can be collected without a full heap collection. We use a static analysis to find groups of allocation sites that create objects that may die together and identify program statements ("kill points") that overwrite reference to these objects. By grouping objects that share kill points, and monitoring kills executed, we try to detect the phase change behaviour of a group of objects and guide the collector's attention to regions of the mature space expected to yield the most free space.
Equivalences in Infinitary Rewriting
Dr. Stefan Kahrs, School of Computing (homepage)

Monday 8th March 2010, 16:00 - 17:00, S110B

Term Rewriting came into prominence 40 years ago when Donald Knuth pointed out several connections between equational reasoning and rewriting. 20 years later the subject of infinitary rewriting was established as a way of modelling e.g. infinitary computations in lazy functional programming.
However, the connection to equational reasoning was totally overlooked then: if rewriting can get to infinite terms "in the limit" then so should equational reasoning. But how does it actually work? And what happens to those connections between rewriting and equational reasoning?
I will give an introduction to all these areas and give some answers to these questions.
Vehicular Ad-Hoc Networks (VANETs)
Dr. Gareth Owen, School of Computing (homepage)

Monday 1st March 2010, 16:00 - 17:00, S110B

Vehicular communication networks are an active and challenging research area. They promise to improve road safety by alerting drivers of upcoming accidents and traffic delays as well as providing in-vehicle internet and multimedia. In this talk, I will outline in detail some of the challenges of vehicular networks. We are interested in traffic information dissemination systems; that is protocols for disseminating information on current road speeds and accidents so that drivers can take alternative routes. There are two main challenges: (a) how can we disseminate, in a timely fashion, relevant information to a particular vehicle; and, (b) how can we detect when congestion exists. I will discuss a research proposal I am writing about a possible solution and hope to receive some feedback on the idea.

Download Slides
Relational Concurrent Refinement: the story so far
Dr. Eerke Boiten, School of Computing (homepage)

Thursday 25th February 2010, 16:00 - 17:00, S110B

The relation between state-based (relational) formalisms and process algebra has been a research topic in this department since the 1990s Viewpoint Consistency projects. A general idea in this work was the close relation between semantics and refinement, and thus relating refinement notions in these two areas was a main thrust of the work. Since 2002, we have been exploring what we called "Relational Concurrent Refinement", which considers encodings of concurrency semantics in a relational model. This seminar gives an introduction to the core ideas and an overview of the main results and future perspectives.

Download Slides
CoSMoS: An Agile Process for Complex Systems Simulation
Paul Andrews, Department of Computer Science, University of York (homepage)

Monday 22nd February 2010, 16:00 - 17:00, S110B

The CoSMoS project, funded by the EPSRC between the Universities of York and Kent, aims to develop a modelling and simulation process and infrastructure to allow complex systems exhibiting emergent properties to be explored, analysed, and designed within a uniform framework. In this talk I will focus on our attempt towards describing an agile process to guide the construction and use of such complex system, which has been distilled from a number of agent-based biological case-studies. I will describe how we can view simulation as a scientific tool; the phases of simulation discovery, development and exploration; generic process activities; and the artefacts that are created when following the CoSMoS approach to developing and using complex systems simulation.

Download Slides
QuickChecking Refactoring Tools
Dániel Horpácsi, Eötvös Loránd University and Dániel Drienyovszky, Eötvös Loránd University

Monday 15th February 2010, 16:00 - 16:30, S110B

Refactorings are behaviour preserving transformations of program source code. Many tools exist for automating large parts of refactoring steps, but these tools are often poorly tested. We present a method for testing Wrangler, an Erlang refactoring tool, using Quviq's Quickcheck. As the input for the refactoring tools is Erlang source code, to generate random test data we should create a large number of data generators that describe the Erlang language and generate random Erlang source code. This talk will demonstrate a better solution: we will introduce a metalanguage above the QuickCheck generators, which provides an easy way to create generators from L-Attributed Grammar descriptions. We will also present a way to test a large subset of Erlang for behavioural equivalence.

Download Slides
Exploring Tracing
Judit Köszegi, Eötvös Loránd University

Monday 15th February 2010, 16:30 - 17:00, S110B

Existing tools for tracing and debugging in Erlang provide only severely limited interactive trace exploration. The talk will be about a tool that provides free navigation through the trace, so we can explore the generated trace events independent of the time arrow, concentrating on casual relationships instead. Processes are at the heart of any Erlang system, thus we will focus on them instead of function definitions and try to localise faults up to purely functional code.

Download Slides
Robot wars: studying the behaviour of hardware and software based robot systems developed from formal models
Dan Slipper, Department of Engineering, University of Leicester

Friday 12th February 2010, 14:00 - 15:00, S110B

Modelling of systems is a robust way of ensuring parallel programs will behave as designed, by ensuring the code will not contain any deadlocks or race hazards. With a range of programming languages available supporting concurrency on different platforms, does developing a system from a CSP model always produce the same results? This presentation reviews the work to date on a project to produce a simple robot system on the LEGO Mindstorms NXT hardware, making use of the Transterpreter to allow concurrent programming on the processor with the occam language. It then explores methods of controlling the same sensors and actuators from the NXT system via a Xilinx Spartan-3A FPGA using Handel-C and experiments possible after developing systems on both platforms following the same CSP model to try to unearth any platform specific issues that may arise.

Download Slides
Automatic Abstraction for Congruences: A Story of Beauty and the Beast
Dr. Andy King, School of Computing (homepage)

Monday 8th February 2010, 16:00 - 17:00, S110B

Just when we thought that verification was a dead topic, the subject has bounced back with forums such as Verification, Model Checking and Abstract Interpretation (VMCAI) attracting record numbers of submissions. This is because model checking offers push button bug finding whereas abstract interpretation gives push button invariant discovery. As these methods find more and more application (recall Byron Cook's talk), yet more tricky practical problems have emerged (recall Byron's lots of papers slide on just termination).
This talk is the second output of my work at Portcullis which focuses on deriving invariants from binaries to support white-hats. It explains how bit-level operations can be automatically transformed into operations over matrices of linear congruence equations. By composing the matrices (something that is beautifully simple), the invariants in the binary then just drop-out, giving a way to discover what a program actually does without even running it (a problem that one would initially think to be an utter beast).
This work was ranked as top paper at VMCAI in January 2010.

Download Slides
Checking Process-Oriented Operating System Behaviour using CSP and Refinement
Dr. Fred Barnes, School of Computing (homepage)

Monday 1st February 2010, 16:00 - 17:00, S110B

Process orientation is an approach to concurrency that uses concepts of processes and message-passing communication, with whole systems constructed from layered and dynamically evolving networks of communicating processes. The work described in this talk relates to the automatic model generation and verification of systems developed in process-oriented languages, in particular occam-pi. Some early applications of this technique to our experimental operating system RMoX are described.

Download Slides
Similar Code Detection and Elimination for Erlang Programs
Professor Simon Thompson, School of Computing (homepage)

Monday 25th January 2010, 16:00 - 17:00, S110B

A well-known bad code smell in refactoring and software maintenance is duplicated code, that is the existence of code clones, which are code fragments that are identical or similar to one another. Unjustified code clones increase code size, make maintenance and comprehension more difficult, and also indicate design problems such as a lack of encapsulation or abstraction. This paper describes an approach to detecting "similar" code based on the notion of anti-unification, or least-general common abstraction. This mechanism is used for detecting code clones in Erlang programs, and is supplemented by a collection of refactorings to support user-controlled automatic clone removal. The similar code detection algorithm and refactorings are integrated within Wrangler, a tool developed at the University of Kent for interactive refactoring of Erlang programs. We conclude with a report on case studies and comparisons with other tools.

Download Slides
Physical Parallel Programming
Mr. Adam Sampson, School of Computing (homepage)

Monday 18th January 2010, 16:00 - 17:00, S110B

The Arduino is an open-source "physical computing" development system with a large, active user community. Arduino applications are usually developed in a subset of C++ with no concurrency facilities, which makes it difficult to build systems that must respond to a variety of external stimuli. We present an implementation of occam for the Arduino based on the Transterpreter portable runtime, adapted to make efficient use of the small Harvard-architecture microcontrollers typically used on devices like the Arduino. In addition, we describe the library of processes -- "Plumbing" -- that we provide to ease the development of physical computing applications.
(This is an expanded version of a presentation from CPA 2009, presenting work done with Matt Jadud and Christian Jacobsen.)

Download Slides
An Object Oriented Programming Technology for Multi-Core Architectures
Stuart Smith, Connective Logic Systems (homepage)

Monday 14th December 2009, 16:00 - 17:00, S110B

The Moore's Law free lunch is over: today's programmers must write parallel programs in order to make use of multi-core systems. The degree of parallelism available in commodity hardware is constantly increasing, and the next generation of systems will make increasing use of non-uniform memory architectures and distributed memory -- so existing applications built to use shared-memory approaches will need reengineering in a few years.
The Blueprint toolset from Connective Logic Systems allows correct, concurrent, object-oriented programs to be constructed by connecting encapsulated components using CDL, a visual programming language. Blueprint includes an efficient multicore runtime, a graphical editor for CDL designs, and tools to analyse and identify concurrency errors in programs.
This seminar will describe the Blueprint approach to the design and implementation of concurrent software, and show how CLS's tools can be used to design several different kinds of concurrent system.
Stuart Smith is the CEO of Connective Logic Systems.
Process Combinators: Capturing Common Patterns in Process-Oriented Programming
Dr. Neil Brown, School of Computing (homepage)

Monday 7th December 2009, 16:00 - 17:00, S110B

The Communicating Haskell Processes library facilitates the construction of concurrent programs in a compositional style from simple elements, primarily: processes, channels and barriers. In this talk, I show how Haskell's expressive power and flexible type system can be used to enable compositional concurrent programming at a higher level of abstraction using process combinators. They allow the user to express complex process behaviours as compositions of simple behaviours, and complex process networks in terms of common patterns. This makes the code more concise and readable, and shows the utility of higher-order processes.

Download Slides
Concurrent Garbage Collection: Why you want it and why it's hard
Mr. Laurence Hellyer, School of Computing (homepage)

Monday 30th November 2009, 16:00 - 17:00, S110B

The world used to be a simple place with just one CPU core, but nowdays multithreaded applications and multicore machines demand the use of ever more complex garbage collection algorithms to give high performance. This talk will provide a quick overview of Stop-The-World GC before moving onto discussing the challenges and benefits of concurrent GC. Tried and tested concurrent GC algorithms will be discussed as well as current work in progress.

Download Slides
Syntactic Type Error Slice Construction
Mr. Thomas Schilling, School of Computing (homepage)

Monday 23rd November 2009, 16:00 - 17:00, S110B

Type error messages for ML-based languages typically suffer from imprecise error locations -- the type checker reports only one of many possible locations of an error. The notion of type error slices corrects this and instead reports all the locations that contribute to a given error (and no more).
Previous work on producing type error slices required the use of a constaint-based type checker. For most legacy systems this would require substantial changes to well-tested and subtle pieces of code. In this work we therefore show how to produce useful type error slices without the need to modify the type checker. Other tools, such as automatic correction systems, can easily be layered on top of our system.

Download Slides
Proving the Correctness of Abstract Concurrency Control and Recovery
Dr. Eliot Moss, Department of Computer Science, University of Massachusetts (homepage)

Monday 16th November 2009, 16:00 - 17:00, S110B

Transactional programming is an attractive paradigm for concurrent programming. However, standard closed nesting is insufficiently flexible. Conservative conflict detection can cause spurious aborts, which negatively impact performance; and integration with concurrent, but non-transactional, code is problematic. Extensions to closed nesting to address these problems have been proposed (such as open nesting and transactional boosting), however such solutions require the programmer to annotate code with locking information and compensating actions (undo code to execute in the case of an abort). It is vital that these specifications be correct, but there are subtleties that can make concurrency control and recovery difficult to reason about. Our work addresses the correctness concerns by allowing the programmer to specify an abstract state model for the data structure in question as well as the proposed conflict predicates and the proposed compensating actions. Our system translates this description into a SAT problem which is then automatically verified by a stock SAT solver. Our tool allows the programmer to reason about their data structure in an abstract context, divorced from implementation details, thus removing much of the burden that transactional extensions impose.
Note: This presents work that is part of the dissertation research of Trek Palmer, a graduate student in Computer Science at UMass under my direction. I offer the talk with his knowledge and encouragement.

Download Recording
Download Slides
Nesting Transactions: Why and What Do We Need?
Dr. Eliot Moss, Department of Computer Science, University of Massachusetts (homepage)

Tuesday 10th November 2009, 16:00 - 17:30, SW101

We are seeing many proposals supporting atomic transactions in programming languages, software libraries, and hardware, some with and some without support for nested transactions. I argue that (in the long run) it is important to support nesting, and to go beyond closed nesting to open nesting. I will argue as to the general form open nesting should take and why, namely that it is a property of classes (data types) not code regions, and must include support for programmed concurrency control as well as programmed rollback. I will also touch on the implications for software or hardware transactional memory in order to support open nesting of this kind.

Download Recording
Download Slides
GIST: Generating Instruction SelecTors Automatically
Dr. Eliot Moss, Department of Computer Science, University of Massachusetts (homepage)

Monday 9th November 2009, 16:00 - 17:00, S110B

Generating code generators automatically is a problem with a venerable history, yet no previous scheme was widely adopted. We contend that this is because previous work was all tied tightly to particular compiler systems, and we present GIST, a tool that can produce the instruction selector (code generator) component for virtually any retargetable compiler system and virtually any target. GIST addresses the key problem of processing relatively machine-independent intermediate representation code (IR) to sequences of relatively machine-specific target instructions. Combined with separately generated components for register allocation, peephole optimization, and instruction scheduling, GIST helps achieve the dream of automatic generation of entire compiler back-ends.
We discuss how GIST represents descriptions of IRs and targets, how it uses compiler writer design directives to map IR memory resources to corresponding target resources, how it employs expression canonicalization and heuristic search, and how it can exploit user-supplied axioms to find additional instruction selection rules. We also touch on how GIST users adapt GIST output to the compiler frameworks they use, and offer results on how well and how quickly GIST finds instruction selection rules for a variety of IR-target pairs.
This talk reports work of PhD student Tim Richards on his dissertation.

Download Slides
Download Recording
AiptasiaWiki: Graphical Pipeline Processing for Community-Driven DNA Analysis
Dr. Marc L. Smith, Computer Science Department, Vassar College (homepage)

Friday 6th November 2009, 14:00 - 15:00, S110B

We designed and built a wiki-based graphical user interface, AiptasiaWiki, which allows bioinformatics researchers to upload their own tools and datasets. Researchers can then analyze their data with complex automated tool pipelines that they compose, using their contributions as well as existing community resources previously added to AiptasiaWiki. In our proof of concept, we engineered a system that allows the creation of both linear pipelines and more sophisticated pipelines that can fork, converge, and run in parallel. To facilitate this system, we developed the domain specific language BIPSL (BioInformatic Pipeline Specification Language) using XML standards. The wiki implementation allows all uploaded data, tools and pipelines to be shared freely amongst the bioinformatics community and encourages open discussion and collaboration on AiptasiaWiki.

Download Slides
Translating ETC to LLVM Assembly
Mr. Carl Ritson, School of Computing (homepage)

Thursday 29th October 2009, 16:00 - 16:30, S110B

The LLVM compiler infrastructure project provides a machine independent virtual instruction set, along with tools for its optimisation and compilation to a wide range of machine architectures. Compiler writers can use the LLVM's tools and instruction set to simplify the task of supporting multiple hardware/software platforms. In this paper we present an exploration of translation from stack-based Extended Transputer Code (ETC) to SSA-based LLVM assembly language. This work is intended to be a stepping stone towards direct compilation of occam-pi and similar languages to LLVM's instruction set.

Download Slides
Auto-Mobiles: Optimised Message-Passing
Dr. Neil Brown, School of Computing (homepage)

Thursday 29th October 2009, 16:30 - 17:00, S110B

Some message-passing concurrent systems, such as occam 2, prohibit aliasing of data objects. Communicated data must thus be copied, which can be time-intensive for large data packets such as video frames. We introduce automatic mobility, a compiler optimisation that performs communications by reference and deduces when these communications can be performed without copying. We discuss bounds for speed-up and memory use, and benchmark the automatic mobility optimisation. We show that in the best case it can transform an operation from being linear with respect to packet size into constant-time.

Download Slides
Mobile Escape Analysis for occam-pi
Dr. Fred Barnes, School of Computing (homepage)

Monday 26th October 2009, 16:00 - 16:30, S110B

Escape analysis is the process of discovering boundaries of dynamically allocated objects in programming languages. For object-oriented languages such as C++ and Java, this analysis leads to an understanding of which program objects interact directly, as well as what objects hold references to other objects. Such information can be used to help verify the correctness of an implementation with respect to its design, or provide information to a run-time system about which objects can be allocated on the stack (because they do not "escape" the method in which they are declared). For existing object-oriented languages, this analysis is typically made difficult by aliasing endemic to the language, and is further complicated by inheritance and polymorphism. In contrast, the occam-pi programming language is a process-oriented language, with systems built from layered networks of communicating concurrent processes. The language has a strong relationship with the CSP process algebra, that can be used to reason formally about the correctness of occam-pi programs. This paper presents early work on a compositional escape analysis technique for mobiles in the occam-pi programming language, in a style not dissimilar to existing CSP analyses. The primary aim is to discover the boundaries of mobiles within the communication graph, and to determine whether or not they escape any particular process or network of processes. The technique is demonstrated by analysing some typical occam-pi processes and networks, giving a formal understanding of their mobile escape behaviour.

Download Slides
Toward Process Architectures for Behavioural Robotics
Mr. Jon Simpson, School of Computing (homepage)

Monday 26th October 2009, 16:30 - 17:00, S110B

Building robot control programs which function as intended is a challenging task. Roboticists have developed architectures to provide principles, constraints and primitives which simplify the building of these correct, well structured systems. A number of established and prevalent behavioural architectures for robot control make use of explicit parallelism with message passing. Expressing these architectures in terms of a process-oriented programming language, such as occam-pi, allows us to distil design rules, structures and primitives for use in the development of process architectures for robot control.

Download Slides
Improving reliability and expressiveness of real-time model-checkers
Dr. Rodolfo Gomez, School of Computing (homepage)

Monday 19th October 2009, 16:00 - 17:00, S110B

We give an overview of our work during the past 3 years, as part of an EPSRC funded postdoctoral fellowship.
The context of the project is formal verification of real-time systems (real-time model-checking), where the system is represented by a network of concurrent, communicating timed automata, and the property to verify is expressed in a temporal logic. The objective of the project is to improve the reliability and expressiveness of real-time model-checkers. In particular, we have developed methods and tools to enhance the functionality of the (widely-used) model-checker Uppaal:
- we developed efficient algorithms to detect Zeno runs in Uppaal models. Zeno runs are the result of timing anomalies in the model, and compromise the soundness of verification algorithms. This analysis is implemented in our ZENOCHECKER tool.
- we developed a compositional translation from Timed Automata with Deadlines (TAD) to Uppaal models. The semantics of urgent actions and synchronization in TAD is safer and more natural than in standard timed automata with invariants (timed safety automata). In particular, TAD models are time-reactive, which ensures that the progress of time can only be interrupted by urgent actions. Our translation allows Uppaal to be used for the design and automatic verification of TAD models (making Uppaal one of the few tools available for TAD). This translation is implemented in our TAD2TA tool.
- we developed a reduction from an expressive real-time interval temporal logic into deterministic timed automata. This allows the specification and verification of complex requirements that cannot be expressed in the TCTL fragment supported by Uppaal. Verification is reduced to reachability analysis wrt observers (the timed automata that accept the models of the property to verify), which can be performed efficiently by Uppaal. This reduction is implemented in our LIDLmd2TA tool
We will close this talk with a brief discussion on future work.

Download Slides
Alloy: Fast Generic Transformations for Haskell
Dr. Neil Brown, School of Computing (homepage)

Monday 12th October 2009, 16:00 - 17:00, S110B

Data-type generic programming can be used to traverse and manipulate specific parts of large heterogeneously-typed tree structures, without the need for tedious boilerplate. Generic programming is often approached from a theoretical perspective, where the emphasis lies on the power of the representation rather than on efficiency. We describe use cases for a generic system derived from our work here at Kent on our nanopass compiler, Tock, where efficiency is a real concern, and detail a new generics approach (Alloy) that we have developed in Haskell to allow our compiler passes to traverse the abstract syntax tree quickly. Benchmarks show that Alloy is fastest on heterogeneously-typed trees compared to several other Haskell generics approaches.
(This talk was previously given at the ICFP Haskell Symposium 2009.)

Download Slides
Logahedra: A New Weakly Relational Domain
Dr. Andy King, School of Computing (homepage)

Monday 5th October 2009, 16:00 - 17:00, S110B

A polyhedron is a higher-dimensional shape that has flat sides, or said another way, can be expressed as a system of linear inequalities. Polyhedra are deployed in vectorisation and verification, but suffer from fundamental scalability problems which relate to size of the coefficients in the linear inequalities. The double whammy is that big coefficients need to be represented with big numbers which not only take time to manipulate but increase the memory footprint of an analyser (verification tool). However, for some verification tasks, for example, those that relate to buffer overflow analysis, the coefficients are often powers of two. This motivates representing a coefficient as its logarithm, hence the name logahedra. The talk will use a series of diagrams to show how logahedra can be used for verification, and then reflect on some experimental work.

Download Slides
A Model for the Transmission of Multimedia Data Flow Based on the Use of Shared Memory Mechanism
Dr. Adilson Barboza Lopes, Federal University of Rio Grande do Norte, Brazil (homepage)

Tuesday 29th September 2009, 14:00 - 15:00, S110B

Distributed multimedia systems must provide support for the efficient interaction of their components, and this can be done by using different communication strategies and mechanisms. A way of identifying efficient communication mechanisms is to consider the location of the involved components. This talk discusses a model to provide flexible and adaptive mechanisms for communication between the components involved in a distributed multimedia data stream. The model considers some Quality of Service (QoS) parameters for supporting the automatic selection of communication mechanisms during run-time. The focus of this talk is related to the location of the involved components. In particular, our concern is with the inter-component communication model that we have proposed, which is based on the shared memory primitives offered by different operating systems. The model can be used on different middleware platforms.

Download Slides
Formal Models of Traversal Strategies
Markus Kaiser, Uni Koblenz

Friday 18th September 2009, 14:00 - 15:00, S110B

Traversal strategies are at the heart of transformational programming with rewriting-based frameworks such as Stratego/XT or Tom and specific approaches for generic functional programming such as Strafunski or "Scrap your boilerplate". Such traversal strategies are distinctively based on one-layer traversal primitives from which traversal schemes are derived by recursive closure.
In the talk, I describe a mechanized, formal model of such strategies. The model covers two different semantics of strategies, strategic programming laws, termination conditions for strategy combinators as well as properties related to the success/failure behavior of strategies. The model has been mechanized in Isabelle/HOL.

Download Slides
Dynamic Evolution of Software Architectures using Aspects
Mr. Cristóbal Costa, Dapartment of Information Systems and Computation, Polytechnic University of Valencia (Spain)

Tuesday 25th August 2009, 16:00 - 17:00, SW101

Nowadays, software systems are more and more complex. This entails that such systems must frequently undergo subsequent revisions in order to correct errors or to add new unforeseen functionalities. However, the intrinsic nature of some systems makes unfeasible their stopping to integrate changes (i.e. critical or autonomous systems). It is while using (and maintaining) such kind of systems when the need for dynamic evolution emerges.
Software architecture provides a good abstraction level to describe such complex systems, in terms of architectural elements (components and connectors) and their interrelations (attachments). Dynamic evolution can be of two kinds, depending on what is changed: the architecture configuration, or the types that compose this architecture. The first kind of evolution, called dynamic reconfiguration, enables a software architecture to change its configuration (i.e. structure) at runtime. This is frequently used to provide systems with fault-tolerance mechanisms or context-adaptations. The second kind of evolution, called dynamic evolution of architectural types allows either a software architecture or a single architectural element to change completely its type (i.e. its specification) at runtime. This kind of dynamism supports the introduction of new architectural element types and connections, the removal of existing element types, or the modification of the way that the different types interact. That is, it supports changing both the composition and behaviour of the software architecture while it is running.
In addition to support the dynamic evolution of software architectures, the maintainability and reuse of both the evolution specifications and mechanisms must be taken into account. The former are dependent on each concrete architecture, whereas the latter are dependent on the underlying technological platform. For this reason, we have isolated these concerns by using aspects, in a way to improve the modularity of the evolvable systems and make easy its design and building.
R, CXXR and Provenance Tracking
Mr. Chris Silles, School of Computing (homepage) and Dr. Andrew Runnalls, School of Computing (homepage)

Thursday 25th June 2009, 16:00 - 16:30, S110B

This seminar is mainly an opportunity for Chris Silles to have a dry-run of a talk 'Provenance Tracking in CXXR' that he is presenting at the useR! 2009 conference in July, in which he will describe his work on adapting the R/CXXR interpreter to track the provenance of data objects, and relate this to the increasing interest in data provenance in other fields of computing.
Before this, Andrew Runnalls will give a brief introduction to the R language for statistical computing, and describe his work on CXXR, an experimental version of the R interpreter in which the current C code is being progressively refactored into C++. This will include material he will be presenting at the upcoming conference on Directions in Statistical Computing, DSC2009.
Homicidal Code: Static Detection and GC Exploitation
Mr. Robert Bunyan, School of Computing (homepage)

Thursday 11th June 2009, 14:00 - 14:30, S110B

Generational Garbage Collection handles short-lived objects very successfully, but does less well with longer lived objects, which may either be processed many times or are left in older generations long after they are dead, thereby wasting space. Ideally, a generational collector should process an object only once. We propose to improve generational garbage collection by guiding the collector to areas of the mature space that contain a high proportion of dead objects which can be collected without a full heap collection. We use a static analysis to find groups of allocations sites that create objects that may die together and identify program statements ('kill points') that overwrite reference to these objects. By grouping objects that share kill points, and monitoring kills executed, we can detect the phase change behaviour of a group of objects and guide the collector's attention to regions of the mature space expected to yield the most free space.
A Framework for Debugging Barriers in Concurrent Systems
Mr. Laurence Hellyer, School of Computing (homepage)

Thursday 11th June 2009, 14:30 - 15:00, S110B

Read and write barriers are used within managed language runtimes to achieve a number of desirable effects. These runtimes can be complex and it is difficult to ensure that all memory operations are correct. A direct memory operation bypassing a barrier may cause an error that is not detectable until much later. This talk demonstrates a novel framework that (i) Ensures all desired memory operations go via a barrier, (ii) If a non-conforming operation occurs the error is immediate allowing for timely debugging, (iii) The overhead of this framework is only incurred when required and still allows good developer productivity.
Optimising Disk Performance for Virtualised Systems: CO620 project presentation
Mr. Andrew Cassidy, CO620 project student

Thursday 7th May 2009, 16:00 - 16:30, S110B

Virtualisation is increasingly used to leverage available computing power, sharing the resources of a single physical system between multiple virtualised computing environments, primarily for reasons of cost. However, this increased sharing leads to increased contention. In a virtualised environment, this can result in a situation where many or all virtualised systems are stalled, waiting for requests on the underlying physical disk to complete.
This presentation will cover the ideas and underlying technologies used in the development of a simple disk reorganisation framework, with an aim to reduce these problems.

Download slides (PDF)
Towards the use of Dynamic Workflows for Coordinating Self-adaptation of Software Systems
Mr. Carlos da Silva, School of Computing (homepage)

Thursday 30th April 2009, 16:00 - 16:20, S110B

The self-adaptation of software system is a complex process that depends on several factors that may change during the system operational lifetime. Hence, the process for coordinating the self-adaptation should also be adaptable to changes that may occur during run-time. As the means for coordinating the self-adaptation process of software systems, we are applying workflows that are dynamically generated for dealing with the variability associated with the self-adaptation process. In this context, this research aims to define and develop techniques for automatically generate workflows for coordinating the self-adaptation of software systems. For demonstrating the feasibility of the proposed approach, architectural reconfiguration of software systems is used as an example, whereby the reconfiguration is managed by workflows that are dynamically generated depending on the availability of resources.
This is a 10 minutes talk, followed by questions and suggestions, as a rehearsal for a talk at the ICSE 2009 Doctoral Symposium on the end of May.
A Review of Current Compile Time Garbage Techniques
Mr. Robert Bunyan, School of Computing (homepage)

Thursday 2nd April 2009, 16:00 - 17:00, S110B

One of the main arguments against using garbage collection (GC), as opposed to explicit memory management, is the runtime costs garbage collection incurs, both in memory overhead and execution time. However, explicit memory management has its own set of problems, including memory leaks and an increased load on the programmer. Compile-time GC aims to remove the overheads of GC while retaining its advantages over explicit memory management.
This talk will cover three types of current compile-time GC: region based memory management, compile-time stack allocation and the automatic insertion of free statements.
Large Scale Ad-Hoc Networks
Dr. Gareth Owen, School of Computing (homepage)

Thursday 19th March 2009, 16:00 - 17:00, S110B

Ad hoc wireless networks are formed of many nodes and require no preexisting configuration to take advantage of any possible routes for packets. Routing in such networks can be challenging and fraught with problems, ranging from capacity limitations to route discovery difficulties. This talk will examine some of the challenges in this field, existing approaches to solving them and future directions. Particularly I will talk about very large networks which may in future facilitate ubiquitously computing, vehicular traffic information systems, etc.

Download slides (PDF)
Using workflows for coordinating self-adaptation of software systems
Mr. Carlos da Silva, School of Computing (homepage)

Thursday 11th December 2008, 16:00 - 17:00, S110B

Self-adaptive software systems can configure and reconfigure themselves to deal with faults, changing of requirements or/and operational environment and resource variability. Workflow management technology coordinates and controls the flow of work and information associated to a process. In the context of self-adaptive software systems, workflow management technology can be used to coordinate the process of self-adaptation. Since this process depends on the system requirements, the system operational state and its environment, which may change during its operation, the process for coordinating the self-adaptation should also adapt depending on the changes that may occur. Thus, to deal with this variability, the workflows that coordinate this process need to be dynamically generated.
In this context, our aim is to design and develop mechanisms for automatic workflow generation for coordinating self-adaptation of software systems. As a case study, we have developed a web service application that relies on the dynamic reconfiguration of its architecture for the provision of dependable services.
Modelling dimensions for self-adaptive software systems
Dr. Rogerio de Lemos, School of Computing (homepage)

Thursday 20th November 2008, 16:00 - 17:00, S110B

Software's ability to adapt at run-time to changing user needs, system intrusions or faults, changing operational environment, and resource variability has been proposed as a means to cope with the complexity of today's software-intensive systems. Such self-adaptive systems can configure and reconfigure themselves, augment their functionality, continually optimize themselves, protect themselves, and recover themselves, while keeping most of their complexity hidden from the user and administrator.
In this talk, we present, from the perspective of software engineering, what are the current challenges in the field, and we discuss a classification of modelling dimensions for self-adaptive software systems. Each modelling dimension describes a particular facet of the system that is relevant to self-adaptation. The modelling dimensions provide the engineers with a common set of vocabulary for specifying the self-adaptive properties under consideration and select suitable solutions.
Generics in Small Doses: Part of TCS's Fun in the Afternoon
Mr. Adam Sampson, School of Computing (homepage)

Monday 17th November 2008, 16:30 - 17:00, SW101

Tock is a new compiler for concurrent imperative programming languages, designed using nanopass techniques. Nanopass compilers transform a program from source code to the target form through the application of a series of transformation passes. Because these passes are usually small and self-contained, the resulting compiler is highly modular, and easy to test and extend. We describe the generic programming interface that we have designed for building nanopass compilers in Haskell, and show how it can be implemented efficiently by combining techniques from the "Scrap Your Boilerplate" and Uniplate generic programming systems. The resulting generics system supports operations upon multiple types without recourse to runtime type introspection.
The Manticore project
Professor John Reppy, University of Chicago

Tuesday 11th November 2008, 16:00 - 17:00, SW101

The Manticore project is an effort to design and implement a new language for parallel programming. Our primary motivation is to move parallel programming out of its traditional application areas, such as Scientific Computing, and into a broader range of applications running on commodity hardware. To achieve that goal, Manticore is a heterogeneous language that supports parallelism at multiple levels. We start with a strict functional core (essentially a mutation-free subset of SML) and extend it with both fine-grain implicitly-threaded parallel constructs and course-grain explicit concurrency. To support heterogeneous parallelism, we have developed a novel scheduling architecture. This talk will give an overview of the project, describe our scheduling infrastructure, and discuss some of the aspects of the implementation.
John Reppy has been studying issues in language design and implementation for twenty years. His work includes the invention of Concurrent ML, co-inventor of the Moby programming language, major contributions to the Standard ML of New Jersey system, and co-editing of the Standard ML Basis Library specification. He received his PhD from Cornell University in 1992 and worked at Bell Laboratories, Murray Hill for eleven years. He is currently a Professor at the University of Chicago.

Download John Reppy's slides
Software TM
Dr. Tony Hosking, School of Computing (homepage)

Thursday 6th November 2008, 16:00 - 17:00, SW101

Transactional Memory has become a "hot" topic these days, as the now prevalent multi-core chips force revisiting support for parallel programming. I will survey some of the recent advances in TM, looking at both hardware and software solutions, and examining the gulf that still needs to be bridged between what hardware manufacturers plan to provide and what software abstractions will demand. The first of these talks will focus on hardware support, using the well-regarded Wisconsin LogTM architecture as a case study. The second talk will look at the programming abstractions that are being proposed for writing transactional programs, and how these abstractions map to the existing hardware, and where hybrid hardware/software techniques are needed.
This seminar is part of the Tony Hosking Seminar Series.
Language Extensions for Open Nested Transactions
Dr. Tony Hosking, School of Computing (homepage)

Tuesday 4th November 2008, 16:00 - 17:00, SW101

We are seeing many proposals supporting atomic transactions in programming languages, software libraries, and hardware, some with and some without support for nested transactions. In the long run, it is important to support nesting, and to go beyond closed nesting to open nesting. I will argue as to the general form open nesting should take and why, namely that it is a property of classes (data types) not code regions, and must include support for programmed concurrency control as well as programmed rollback. I will also touch on the implications for software or hardware transactional memory in order to support open nesting of this kind. I will describe a concrete proposal for open nested transactions in Java. We argue that open nesting is most usefully seen as a way to express concurrency abstractions at different levels or granularities within (layered) data structures. To support this, we specify open nesting as a property of the class in Java, since the class is the principal data abstraction mechanism for Java programmers. Concurrency abstractions based on open nesting relax physical (memory-level) serializability while preserving abstract serializability. Abstract serializability is specified by the programmer in terms of abstract locks, which are associated with each of the operations (i.e., methods) operating at a given abstraction level (i.e., class), to specify the logical conflicts among concurrently executing operations. Abstract locks come with a predefined compatibility matrix used by the run-time system to mediate execution of these operations. We will describe the syntax and semantics of open nested classes for Java, and explore the power of the approach with an example. We will also point out possible pitfalls for programmers using open nesting, and discuss rules of thumb for programmers to use to avoid these problems.
This seminar is part of the Tony Hosking Seminar Series.
Hardware TM
Dr. Tony Hosking, School of Computing (homepage)

Thursday 30th October 2008, 16:00 - 17:00, SW101

Transactional Memory has become a "hot" topic these days, as the now prevalent multi-core chips force revisiting support for parallel programming. I will survey some of the recent advances in TM, looking at both hardware and software solutions, and examining the gulf that still needs to be bridged between what hardware manufacturers plan to provide and what software abstractions will demand. The first of these talks will focus on hardware support, using the well-regarded Wisconsin LogTM architecture as a case study. The second talk will look at the programming abstractions that are being proposed for writing transactional programs, and how these abstractions map to the existing hardware, and where hybrid hardware/software techniques are needed.
This seminar is part of the Tony Hosking Seminar Series.
Implementing Choice: Communicating Haskell Processes
Dr. Neil Brown, School of Computing (homepage)

Tuesday 14th October 2008, 15:00 - 15:20, S110B

This talk will outline a "process-oriented" concurrency model centred around encapsulated processes communicating over synchronous channels. We will explain how the ability to choose between communicating on different channels can be very useful, including choosing between different conjoined sets of channel communications. We will give an overview of how this choice has been implemented with Software Transactional Memory.
Communicating Haskell Processes: implementing CSP ideas in Haskell
Dr. Neil Brown, School of Computing (homepage)

Thursday 19th June 2008, 16:00 - 17:00, SW101

Haskell: all-singing, all-dancing higher-order monadic imperative sequential functional lazy language with class. occam-pi: massively-concurrent sequential choice-filled programming. This talk describes what happened when we mixed the two and implemented occam-pi ideas in Haskell using Software Transactional Memory. The simple interface of the resulting library can provide inspiration for future concurrent language design. Haskell's declarative style and higher-order functions allow concurrent programs to be composed more elegantly than in existing languages. We will also explain how to implement multiway synchronisation that any party may withdraw from using STM. Neither Haskell nor occam-pi knowledge is required, but having both would allow you to arrive a few minutes late.

Download slides (PDF)
A Study of Java Object Demographics
Professor Richard Jones, School of Computing (homepage)

Thursday 5th June 2008, 11:00 - 11:40, S110B

Researchers have long strived to exploit program behaviour in order to improve garbage collection efficiency. For example, by using a simple heuristic, generational GC manages short-lived objects well, although longer-lived objects will still be promoted to an older generation and may be processed repeatedly thereafter. In this paper, we provide a detailed study of Java object lifetimes which reveals a richer landscape than the generational view offers. Allocation site has been claimed to be a good predictor for object lifetime, but we show that object lifetime can be categorised more precisely than 'short-lived/ long-lived/immortal'. We show that (i) sites allocate objects with lifetimes in only a small number of narrow ranges, and (ii) sites cluster strongly with respect to the lifetime distributions of the objects they allocate. Furthermore, (iii) these clusterings are robust against the size of the input given to the program and (iv) are likely to allocate objects that are live only in particular phases of the program's execution. Finally, we show that, in contrast to previous studies, (v) allocation site alone is not always sufficient as a predictor of object lifetime distribution but one further level of stack context suffices.
Investigating Memory Access and Energy Consumption on the x86 Platform
Mr. Laurence Hellyer, School of Computing (homepage)

Thursday 5th June 2008, 11:40 - 12:00, S110B

Power consumption is becoming more and more important, yet suitable tools to research power consumption on popular platforms such as x86 are limited or simply not available.
Memory power and the cost of CPU stalls can account for more than 50% of total power consumption. As memory latency continues to increase relative to CPU performance this problem will grow.
I am particularly interested in the opportunities and difficulties managed run-times present. The fastest algorithm is not always the most energy efficient.
I describe the design of a research tool that will consider the complete system energy consumption and allow exploration of energy consumption due to memory accesses on multiple platforms.
Using the SARG web-page management system
Dr. Fred Barnes, School of Computing (homepage)

Thursday 24th April 2008, 16:00 - 17:00, CC02

The Systems Architecture Research Group's new web-pages (which can be found here), are centred around projects and themes, whose information is stored in a database. Unlike the database (CS-web) that feeds the standard CS web-pages, users are able to edit the information associated with themselves, their projects, and suchlike from a basic web-interface. Information kept and managed by this new system includes research-groups, users, projects, postgraduate research project suggestions, publications, supporters (project funding), themes, news items and group seminars. Users can be assigned different levels of access-control, reflecting their roles within the group (e.g. web-master, seminar-organiser) or department as a whole (e.g. head-of-group, head-of-research). As well as generating the group's main web-pages, the system generates small sections of HTML that can be included on a user's home-page (business-card page), showing the projects with which they are involved.
Currently, only the systems architecture group are using this style of pages, but the database behind it is aware of other research groups, permitting users, projects and suchlike to be shared between groups.
This seminar will take place in a terminal-room. In the first part, I will give a brief overview of what the system does and how it works. In the second part, users (principally laboratory staff), will have the opportunity to play around with the administrative interface, setting some of their own details (e.g. research-interests) or creating projects with which they are involved.
Re-engineering Legacy Numerical Software
Mr. James Nicolson, CO620 project student

Thursday 27th March 2008, 16:00 - 16:30, S110B

We describe the process used to transform a piece of legacy numerical software, written in Fortran 66, into a Fortran 95 module. The final version is more maintainable, has more user facilities and has fewer errors. We also report on the effect this transformation had on the run-time efficiency of the code.

Download 2-up handouts (PDF)
Active, Provenance-Aware File System
Mr. Chris Silles, CO620 project student

Thursday 20th March 2008, 16:00 - 16:30, SW101

The Active, Provenance-Aware File System aims to present users with only the most up-to-date versions of derived files; by considering files as not only having content, but also a recipe by which that content can be derived. During execution of a file recipe, APAFS monitors exactly which files are requested to accurately determine dependencies of the target file. When an APAFS file is opened, this provenance information is used to establish whether or not the target files and its dependencies are up-to-date with respect to their dependencies, and out-of-date files are rebuilt as necessary according to their recipes.
No Entry Without the Permission of the Surveyor
Mr. Jon Simpson, School of Computing (homepage) and Mr. Carl Ritson, School of Computing (homepage)

Thursday 21st February 2008, 16:00 - 17:00, SW101

The Surveyor Corporation SRV-1 robot, is a small inexpensive robotics platform making in-roads into the enthusiast and education communities. Equiped with a fast micro-processor, camera, motors and wireless networking it provides an excellent platform for explorations into robotic control. In this casual talk, we will detail the SRV-1 robot\'s architecture and recent innovations in the Transterpreter Transputer Virtual Machine to support running the occam-pi concurrent programming language on it. We will also demonstrate a software development environment we have produced to aid teaching using the SRV-1 and occam-pi at Olin Technical College, Boston, MA.

Download slides (PDF)
Tock: Beginning with Omega
Dr. Neil Brown, School of Computing (homepage)

Thursday 31st January 2008, 16:00 - 17:00, SW101

The Omega Test is an automated equation solver that discovers whether there is an integer solution to a set of linear equalities and linear inequalities. We can use it in Tock, our occam compiler, to check whether parallel array indexes can ever overlap (and are thus unsafe). This presentation gives an explanation of how the Omega Test works, and of its limitations. Modulo arithmetic, a potential sticking point, is examined and solutions for dealing with it are detailed. Basic knowledge of algebra and mathematical notation is required.

Download annotated slides (PDF)
Tock: a nanopass presentation
Mr. Adam Sampson, School of Computing (homepage) and Dr. Neil Brown, School of Computing (homepage)

Thursday 6th December 2007, 16:00 - 17:00, SW101

In the second Tock talk, we will examine the various stages of compilation in more detail. We will discuss parser combinators, C/C++ code generation, usage checking, and look at why occam is an interesting language to compile. We will also look at another use of generics, and finally reflect on our experiences with Haskell. Attendance at last week's talk is not required. Knowledge of Haskell and monads will help in parts, but is not essential for all of the talk.

Download slides (PDF)
Tock: every compilation begins with a single pass
Dr. Neil Brown, School of Computing (homepage) and Mr. Adam Sampson, School of Computing (homepage)

Thursday 29th November 2007, 16:00 - 17:00, SW101

Nanopass compilation is a way of structuring a compiler as many small passes, each performing only one simple action. In the first of two talks, we will introduce Tock, our nanopass compiler for concurrent languages. The compiler itself is written in Haskell. We will explain nanopass compilation, and how we have implemented it with the help of Haskell generics. We will then go on to demonstrate a novel use for Haskell generics for pattern-matching in our testing framework. Basic familiarity with Haskell is assumed, but no more.

Download slides (PDF)
Will Virtual Machines Ever Take Off?: A High Integrity VM for Safety-Critical Applications
Mr. Steve Wright, University of Bristol (homepage)

Thursday 22nd November 2007, 16:00 - 17:00, S110B

A Virtual Machine (VM) is a program running on a conventional microprocessor that emulates the binary instruction set, registers, and memory space of an idealized computing machine. At the cost of run-time performance, VMs provide a route for planned hardware obsolescence and early application development and test. Therefore, VMs have been suggested as an evolution of current Integrated Modular Avionics architectures.
MIDAS (Microprocessor Instruction & Data Abstraction System) is a VM capable of running binary executables compiled from languages such as C and ADA, whilst providing run-time executable verification, and being suitable for implementation using Formal Methods.
This presentation covers the features of the MIDAS VM, its place in IMA architectures, and its implementation using Formal Methods.
Decrypting the Java Gene Pool: Object lifetime discovery using Micro-Patterns
Mr. Sebastien Marion, School of Computing (homepage)

Thursday 11th October 2007, 16:00 - 16:30, S110B

Over the years, Garbage Collection (GC) has been a topic of much interest. Some attempts to improve GC throughput have resulted in making use of heuristics, essentially trying to predict how long an object is likely to live. The main drawback of these approaches however is that they require some prior trace recordings of the program's behavior. We present a novel method allowing the prediction of such lifetime by determining the set of micro-patterns associated with each Java class of the program.
Intelligent Selection of Application-Specific Garbage Collectors
Jeremy Singer, University of Manchester (homepage)

Thursday 27th September 2007, 16:00 - 17:00, S110B

Java program execution times vary greatly with different garbage collection algorithms. Until now, it has not been possible to determine the best GC algorithm for a particular program without exhaustively profiling that program for all available GC algorithms. Our new approach uses machine learning techniques to build a prediction model that, given a single profile run of a previously unseen Java program, can predict an optimal GC algorithm for that program.

Download slides (PDF)

CPA-2007 Conference Presentations
Mr. Carl Ritson, School of Computing (homepage), Dr. Fred Barnes, School of Computing (homepage), Professor Peter Welch, School of Computing (homepage), Dr. Neil Brown, School of Computing (homepage), Mr. Jon Simpson, School of Computing (homepage), Mr. Christian Jacobsen, School of Computing (homepage) and Dr. Matthew Jadud, School of Computing

Wednesday 4th July 2007, 14:00 - 17:00, S110B

Approximately 7 research staff and students from the systems research group will be heading off to CPA-2007 next week, armed with a variety of paper presentations. This session will be a "test drive" for these -- all welcome to observe, comment and question. The talks will be:

Carl Ritson and Fred Barnes	A Process Oriented Approach to USB Driver Development
Peter Welch and Neil Brown	Integrating and Extending JCSP
Carl Ritson and Peter Welch	A Process-Oriented Architecture for Complex System Modelling
Neil Brown	C++CSP2: A Many-to-Many Threading Model for Multicore Architectures
Jon Simpson, Christian Jacobsen and Matthew Jadud	A Native Transterpreter for the LEGO Mindstorms RCX

Abstracts for these talks can be found on the CPA-2007 programme page.

C++CSP2 -- Atomic Adventures in a Multi-Core Universe
Dr. Neil Brown, School of Computing (homepage)

Thursday 10th May 2007, 16:00 - 17:00, S110B

The original C++CSP library — an implementation of occam/CSP ideas in C++, was written as an undergraduate project, built on top of co-operatively scheduled user-threads. Faced with the mass-market advent of multi-core processors, I have rewritten the C++CSP library to take advantage of the available parallelism; transforming the library to use many-to-many threading, combining kernel-threads and user-threads. The algorithms are intended to be scalable, ready for a future increase in the number of cores. This talk on my work will involve a mix of algorithms, practical benchmarks, the C++CSP2 API and discussion of issues arising from implementing concurrency in a sequential language.
Dynamic memory management: challenges for today and tomorrow
Professor Richard Jones, School of Computing (homepage)

Thursday 29th March 2007, 16:00 - 17:00, S110B

Garbage collection (GC) is a key component of almost all modern programming languages. The advent of conventional object-oriented languages supported by managed run-times (e.g. Java, C# and even Managed C++) has brought GC into the mainstream and, as memory manager performance is critical for many large applications, brought GC to the attention of programmers outside its traditional functional programming language community.
In this talk, I shall start by reviewing how GC got to where it is today, why it is desirable, what performance you might reasonably expect and I shall outline the directions in which GC research is moving. In particular, I'll look at some of the challenges facing modern GC, in contexts ranging from GC for high-performance, multiprocessor systems to GC for real-time systems and limited devices, from better integrating with its operating environment to supporting specific applications. I shall speculate wildly on future directions for research.
System Monitoring and Control
Mr. Richard Bonner, CO620 project student

Thursday 22nd March 2007, 16:00 - 17:00, S110B

Every network administrator's worst fear is for a server to enter a state where it stops responding to the network (or console), thereby requiring a hard reset before normal operations can resume. Due to the physical location of most servers, this can be a costly and time-consuming task. This seminar presents an inexpensive method for controlling servers remotely, utilising a two-tier software/hardware approach.
A Process-Oriented Approach to Blood Clotting Simulation and Visualisation
Mr. Carl Ritson, School of Computing (homepage)

Wednesday 21st March 2007, 14:00 - 15:00, S110B

Although presented in a generic re-usable form, at this work's core is a fine-grained massively-parallel process-oriented model of platelets within a blood vessel using a CSP inspired design, expressed and implemented using the occam-pi language. The aim being to engineer emergent behaviour from platelet processes. The described case study runs to millions of processes engaged in ever-changing communication topologies. It is free from deadlock, livelock, race hazards and starvation by design, employing a small set of synchronisation patterns for which we have proven safety theorems.
Distributed Information Storage in a Pervasive Peer-to-Peer Network (part 1)
Mr. James Grant, CO620 project student

Thursday 15th March 2007, 16:00 - 16:30, SW101

This talk is the first part of two complementary talks that introduce the problem of dynamically maintaining a population of file replicas in a distributed, ad-hoc peer-to-peer file storage system. The focus of this talk are two very simple algorithms that allow fragments to autonomously respond to changing levels of replica fragments in their local network. The two algorithms were simulated and evaluated using NetLogo, and the overall fragmentation-redundancy-scattering file system was implemented and evaluated in a cluster of computers for evaluating the scalability of the overall approach.
Distributed Information Storage in a Pervasive Peer-to-Peer Network (part 2)
Mr. Jonathan So, CO620 project student

Thursday 15th March 2007, 16:30 - 17:00, SW101

Fragmentation-redundancy-scattering is a fault-tolerance technique for ensuring the availability of information in distributed systems. This talk presents different algorithms that can be combined with FRS to lessen the risk of information loss in a pervasive peer-to-peer storage system. I shall also describe a prototype implementation, written in Java, which was used for simulation of the algorithms. This talk continues from the previous talk by my colleague, James Grant.
A Software Infrastructure for Applications and Networked Services on Embedded Hardware
Mr. Leon Sodhi, CO620 project student

Thursday 8th March 2007, 16:00 - 16:30, SW101

This talk will discuss the creation of an operating system that will use the full processing power of an embedded device (this could be a custom made or an obsolete PC) to execute network services and/or a single application.
An example of both will be included in the form of a basic packet filter with internet sharing capabilities and a command line application. Third parties will also be able to write their own, e.g. a filter service for the SMTP protocol or an application that needs to process a set of data as quickly as possible.

Download slides (PPT)
Garbage Collection for Data Structure Reorganisation
Mr. George Kurian, CO620 project student

Thursday 8th March 2007, 16:30 - 17:00, SW101

Complex programs typically have complex data structures. When used in a language with automatic garbage-collection (Java), a significant portion of collection time can be spent handling such complex structures. This talk discusses the optimisation of such structures, using knowledge gained about these structures from the collector itself, in order to improve garabage-collection (GC) performance.

Download slides (PPT)
A Native Transterpreter for the LEGO MindStorms RCX
Mr. Jon Simpson, CO620 project student (homepage)

Thursday 22nd February 2007, 16:00 - 16:30, S110B

This talk will present a small and maximally concurrent occam-pi operating environment for the LEGO MindStorms RCX robotics platform, implemented using the Transterpreter virtual machine.
After an overview of the platform and virtual machine, I will discuss the difference between this implementation and a previous related one, some of the problems of using the Transterpreter with the Mindstorms RCX and present an advantage to working in a concurrent runtime from the hardware up.

Download slides (PDF)
An IDE Driver for RMoX
Mr. Christian Föecker, CO620 project student

Thursday 22nd February 2007, 16:30 - 17:00, S110B

I will describe my work on a IDE (harddisk) driver for RMoX. This will include an introduction on how to access the hardware as well as concrete code examples showing how this is realised. The talk will finish with a brief outlook of what could be done in the future, building upon this project.

Download slides (PDF)
Making Music with occam-pi
Mr. Adam Sampson, School of Computing (homepage)

Thursday 1st February 2007, 16:00 - 17:00, S110B

In the last twenty years of electronic music, the boundaries between programming and composition have become increasingly blurred. This talk will show how musicians can make use of process-oriented techniques during live performance.

Download slides (PDF)
Region Based Memory Management
Guillaume Salagnac, Laboratoire Verimag, Grenoble (homepage)

Wednesday 17th January 2007, 14:00 - 15:00, S110B

Dynamic memory management is a serious challenge for real-time embedded systems based on Java technology. Contrary to the standard Java paradigm, garbage collection is rarely used in such real-time environments, since the temporal behavior of dynamic memory collection (e.g. pause times) is usually difficult to predict and thus significantly complicates the implementation of real-time scheduling policies. On resource-limited platforms, such as smart cards, the implementation of efficient garbage collectors (GC) is furthermore hindered by hardware limitations, and embedded systems manufacturers frequently omit them completely (see the JavaCard2 platform for instance). Similarly, several GC algorithms have been proposed for real-time applications, but they typically require the programmer to provide a model of the dynamic memory management behaviour of his application, such as the maximum allocation and mortality rates of objects for instance, a difficult task at best (i.e. determine the maximum allocation is undecidable).
This talk will present an efficient static analysis algorithm, combined with a region allocation policy for real-time embedded Java applications. The goal of this work is to provide a static analysis mechanism efficient enough to be integrated in an assisted-development environment, and to implement region-based memory management primitives suited for resource-limited platforms.
occam-pi Masterclass
Mr. Adam Sampson, School of Computing (homepage)

Thursday 16th November 2006, 12:00 - 17:00, SW110A

This short course will introduce participants to the new features of occam-pi.

Download course materials
Improvements to the GCSpy Heap Visualisation Framework
Andy Cheadle, Imperial College, London (homepage)

Thursday 16th November 2006, 16:00 - 17:00, SW101

We will present generic extensions to the GCspy visualisation framework that make it suitable for tracking the way continuous dynamic memory allocators such as malloc or incremental and concurrent garbage collectors make use of heap memory. These extensions include sample-driven client-server communication, incremental stream updates and client-controlled stream update frequency. Additional enhanements to the current GCspy client will also described. These include the grouping of drivers to form hierarchies and the subsequent visualisation of those hierarchies. Additional features such as zooming and tile linking between spaces, will also be demonstrated.
We also introduce some new features that add primitive performance debugging capabilities to GCspy. In particular we will report our experiences with a simple heuristics engine can flip GCspy from its decoupled 'observation' mode to a synchronous 'single-step' mode, and a backtrace facility that can trace the server-side call sequence that led to the triggering of a specified event, such as the allocation or freeing of a block of memory.
We will provide a demonstration of the new framework and will show how the various new features can be combined to provide a visualisation of Doug Lea's 'malloc' (dlmalloc). We will present performance figures for the new framework and will demonstrate how it can be used to explore contrived modifications to dlmalloc's coalescing policy. We will also comment on our plan to extend further CGspy's performance debugging capabilities.
Objects' Lifetime Discovery with Micro-Patterns
Mr. Sebastien Marion, School of Computing (homepage)

Thursday 9th November 2006, 16:00 - 17:00, SW101

Over the years, Garbage Collection (GC) has been a topic of much interest. Some attempts to improve GC throughput have resulted in making use of heuristics, essentially trying to predict how long an object is likely to live. The main drawback of these approaches however is that they require some prior trace recordings of the program's behavior. We present a novel method allowing the prediction of such lifetime by determining the set of micro-patterns associated with each Java class of the program.
An Introduction to Pointer Analysis
Mr. Robert Bunyan, School of Computing (homepage)

Tuesday 17th October 2006, 16:00 - 17:00, S110B

I will introduce the concept of pointer analysis beginning with a brief look at the concept of aliasing and concluding with a step by step example analysis of some code using both the Steensgaard and Andersen pointer analyses. The presentation will also cover some of issues that have to be considered when choosing or designing a pointer analysis, such as the issue of flow sensitivity.
The Doomsday Protocol
David Munro, University of Adelaide (homepage)

Wednesday 30th August 2006, 10:00 - 11:00, SW101

Distributed termination detection (DTD) algorithms are important since they detect globally stable states in distributed computations. Here we introduce a new distributed termination detection protocol, the Doomsday protocol, together with its proof of correctness. We use the term protocol since it is generic, forming the basis for a number of new and existing DTD algorithms for which the correctness proof may be reused. This talk describes the Doomsday protocol, outlines its formal proof, and shows how a new DTD algorithm and how other hitherto unrelated algorithms can be derived from the protocol.
Using a Policy Language to Control Tuple-space Synchronization in a Mobile Environment
Mr. Vorapol Jittamas, School of Computing

Thursday 25th May 2006, 11:00 - 12:00, S110B

Any sharing of information using a distributed platform carries the risk of disconnection because of loss of network access. This is particularly the case when considering mobile communication, either using base stations or by forming ad-hoc networks. Replication of shared data is one way to increase data availability in such an environment, but leads to the problem of inconsistency between copies of data, and so requires some means of data synchronization.
This paper investigates how policies can be used to resolve data conflict in a way that can be tailored to meet the needs of different types of application in different situations. It discusses a range of application requirements, and describes a policy-based pervasive middleware to support the sharing of data using a tuple-space paradigm. Policies maintained within the middleware are used to trigger a wide range of synchronization options to restore the consistency of the data after periods of disconnected operation.
Portable, Mostly-Concurrent, Mostly-Copying Garbage Collection for Multi-Processors
Antony Hosking, Purdue University (homepage)

Friday 19th May 2006, 14:00 - 15:00, S110B

Modern commodity platforms increasingly support thread-level parallelism, which must be exploited by garbage collected applications. We describe the design and implementation of a portable *mostly-concurrent* mostly-copying garbage collector that exhibits scalable performance on multi-processors. We characterize its performance for heap-intensive workloads on two different multi-processor platforms, showing maximum pause times two orders of magnitude shorter than for fully stop-the-world collection at the cost of some total mutator throughput.
Game Algorithms in occam-pi
Mr. Kevin Morgan, CO620 project student

Friday 3rd March 2006, 12:00 - 13:00, S110B

The occGame project is a research project to explore how zero-sum perfect-information game algorithms can be realised in occam-pi. With simpler games, like tic-tac-toe, the game tree is relatively small and can be completely searched, whereas in larger games such as chess this is not possible (at least not in a reasonable time). Using parallel hardware and algorithms would allow for more of the tree to be searched and better results obtained. As such occam-pi seems a highly suitable language to implement these kinds of algorithms. My presentation will give a brief overview of the algorithms that are generally used, what new occam-pi features have been, and may be used for these types of algorithms, the pros and cons of using occam-pi, as well as some of the results obtained so far.
Graphics Library Support for occam-pi
Ms. Samantha Davis, CO620 project student

Tuesday 28th February 2006, 10:00 - 10:30, S110B

In this talk I will be discussing my research involving the occam-pi graphics library. The talk will cover programming Brownian-motion in occam-pi and some performance results. Further developments that could build on this work will also be discussed.

Download slides (PPT)
Intrusion Tolerance in Distributed Systems
Ms. Vicki Spurrett, CO620 project student

Tuesday 28th February 2006, 10:30 - 11:00, S110B

In this talk I will discuss how the intrusion tolerance technique of fragmentation-replication-scattering (FRS) can be used to create a dependable and secure way to store files within a distributed system. I will also talk about how a simulation of the FRS system was designed and implemented and the issues raised during implementation. The talk will finish with details on possible future work.

Download slides (PPT)
An Eclipse Framework for occam-pi
Mr. Alex Mather, CO620 project student

Monday 27th February 2006, 15:00 - 15:30, S110B

In this talk I will discuss an Eclipse framework for occam-pi. The talk will cover the motivations for creating the framework, the Eclipse platform, features included in the framework to improve occam-pi development, its uses as a teaching tool and its implementation. I will also look at possible future work on the project.

Download slides (PPT)
A Video Processing Framework in occam-pi
Mr. Carl Ritson, CO620 project student (homepage)

Tuesday 21st February 2006, 10:00 - 10:30, S110B

In this talk I will describe a video processing framework for the occam-pi language. The talk will cover the motivation for using occam-pi as a multi-media handler, an overview of the protocols involved and a look into developing video players and other tools, exploiting occam-pi's features to provide dynamism and efficiency.

Download slides (PDF)
Tolerating Fault in a Distributed Storage System
Mr. Rudi Ball, CO620 project student

Tuesday 21st February 2006, 10:30 - 11:00, S110B

The talk will describe an approach for tolerating faults in a distributed storage system using the mechanisms of fragmentation, replication and scattering (FRS), keyed digests and encryption. I hope to describe the aims of the system, its structure, prototype implementation (using agents), performance issues and anticipated future work.

Download slides (PPT)
Programming the CELL
Mr. Damian Dimmich, School of Computing (homepage)

Tuesday 7th February 2006, 10:00 - 11:00, S110B

The CELL processor developed by IBM, Sony and Toshiba, is a radically new CPU design. The talk will start with a quick overview of the architecture and primary features of the CELL. Following that details of how to program the CELL will be given along with code examples. I hope to cover at least some of the following: concurrency mechanisms; CELL's internal communication mechanisms (mailboxes); how to make use of the vector units, attaining maximum performance; and possibly going over some of the SPU's (dedicated vector units) assembly language.

Download slides (PDF)
A New Compiler for Parallel Programming
Dr. Fred Barnes, School of Computing (homepage)

Tuesday 31st January 2006, 10:00 - 11:00, S110B

This talk introduces the new occam-pi compiler, a highly dynamic and extensible compiler for parallel programming. Although primarily designed to compile occam-pi, the compiler supports a CSP-like language that also targets the KRoC run-time system. In this talk I will discuss the motivation for writing a new compiler along with its structure and some key features. Amongst the more interesting features are the ability to modify the language grammar at run-time, namespaces and digital-signatures for generated code.

Download slides (PDF)
One size doesn't fit all: exploiting program behaviour
Professor Richard Jones, School of Computing (homepage)

Tuesday 24th January 2006, 10:00 - 11:00, S110B

Modern state of the art garbage collectors are designed to combine high throughput with low pause-times. And they are very successful for typical programmes. However, much GC effort is, in a sense, wasted. Rather than reclaiming memorydirectly (which is what the programmer wants), tracing GC expends effort on preventing the premature and unsafe reclamation of space used by live objects. It has long been known that programs' 'object demographics' are not random. Rather objects are allocated, interact and die in particular patterns. Furthermore, there is no 'one size fits all' strategy: different collectors perform better or worse on different programs. We believe that GC should and can exploit understanding of the program in order to improve performance.
In this talk, I shall review work that has sought to exploit program behaviour. I shall describe three recent aspects of our work in this area. First, we introduce a novel static analysis and heap organisation in order to reduce GC synchronisation. Second, we show that program behaviour is sufficiently predicable to allow us to collect only those regions of the heap in which we expect the vast majority of objects to be dead. Finally, I shall outline a new collection framework that can take advantage of this behaviour.
Exploiting Phases in Execution and Resource Availability for Efficient Program Sampling and VEE Specialization
Dr. Chandra Krintz, University of California, Santa Barbara (homepage)

Monday 19th December 2005, 14:00 - 15:00, SW101

Key to extracting high-performance from programs executed using virtual execution environments (VEEs), is effective dynamic adaptation of the program and runtime to the changing characteristics of program execution and resource availability. To enable aggressive adaptive optimization, VEEs require efficient techniques that track these changes accurately and that exploit them to extract higher-levels of performance.
Our work focuses on two techniques that enable dynamic adaptation in VEEs: efficient performance profiling and dynamic VEE specialization. The unifying factor of our research is our capture, characterization, and exploitation of repeating patterns, i.e., phases, in program behavior and resource availability. Our profiling techniques use phases to guide transparent execution sampling. Our specializations consider not only optimization and specialization of executing programs, but that of the execution environment, as resource consumption and availability changes. In this talk, we overview our research on efficient program sampling and specialization. As examples of the latter, we present two VEE specializations for garbage collection (GC) that improve startup time for generational systems and that improve overall execution time via dynamic switching between GC systems.

Download slides (PPT)
A Fast Analysis for Thread-Local Garbage Collection
Professor Richard Jones, School of Computing (homepage) and Dr. Andy King, School of Computing

Tuesday 6th December 2005, 10:00 - 11:00, SW101

Long-running, heavily multi-threaded, Java server applications make stringent demands of garbage collector (GC) performance. Synchronisation of all application threads before garbage collection is a significant bottleneck for JVMs that use native threads. We present a new static analysis and a novel GC framework designed to address this issue by allowing independent collection of thread-local heaps. In contrast to previous work, our solution safely classifies objects even in the presence of dynamic class loading, requires neither write-barriers that may do unbounded work, nor synchronisation, nor locks during thread-local collections; our analysis is sufficiently fast to permit its integration into a high-performance, production-quality virtual machine.
Death Order Garbage Collection and the Beltway Collector
Dr. Chris Ryder, School of Computing (homepage)

Tuesday 22nd November 2005, 10:00 - 11:00, S110B

In this talk (previously given to the TCS group, updated for the systems group) I will introduce the Beltway garbage collector. Beltway is a very flexible collector which offers many opportunities for tuning the collection strategy. Death order garbage collection is a strategy that takes advantage of predictable behaviour in programs to collect only the regions of the heap in which we expect all objects to be dead. I will discuss work currently being carried out by Richard Jones and myself, funded by IBM, to implement a death order strategy using the Beltway collector and IBM's Jikes RVM Java virtual machine.
Lazy Simulation of Cellular Automaton with Communicating Processes
Mr. Adam Sampson, School of Computing (homepage)

Tuesday 15th November 2005, 10:00 - 11:00, SW101

Cellular automata (CAs) are good examples of systems in which large numbers of autonomous entities exhibit emergent behaviour. Using the occam-pi and JCSP communicating process systems, we show how to construct lazy and just-in-time models of cellular automata, which permit very efficient parallel simulation of sparse CA populations on shared-memory and distributed systems.
pony - The occam-pi Network Environment
Dr. Mario Schweigler, School of Computing

Tuesday 8th November 2005, 10:00 - 11:00, S122A

Although concurrency is generally perceived to be a `hard' subject, it can in fact be very simple - provided that the underlying model is simple. The occam-pi language provides such a simple yet powerful concurrency model that is based on CSP and the pi calculus. This talk presents pony, the network environment for occam-pi. occam-pi and pony provide a new, unified, concurrency model that bridges inter- and intra-processor concurrency. This enables the development of distributed applications in a transparent, dynamic and highly scalable way.
Interfacing C and occam-pi
Dr. Fred Barnes, School of Computing (homepage)

Tuesday 25th October 2005, 14:00 - 15:00, S122A

The occam-pi programming language provides various facilities for interacting with the external environment, e.g. to call external library functions. Although these mechanisms are useful (and sufficient for our needs so far), the handling of foreign data-types in occam-pi is not particularly pleasant. In the majority of cases, such data are pointers to C structures, often containing external state and passed to many different external calls. Although the overheads of these external calls are small, the resulting occam-pi program becomes hard to understand without constant reference to the external functions.
This talk, first presented at CPA-2005, examines a new C interface for occam-pi that allows whole processes to be written in C; complete with channel communication, barrier synchronisation and all the occam-pi features. This provides a way of having processes that can easily make external calls (more or less as any C application would), manipulate their own state in an obvious way, and interact with concurrent processes (through channel communication and other synchronisations).
The applications of this new mechanism are wide-ranging, from providing cleaner handling of external code in occam-pi systems, through to the programming of whole CSP-based concurrent systems in C (with all the features of occam-pi).
Low-level device drivers for RMoX
Mr. Alex Foreman, CO620 project student

Tuesday 19th April 2005, 14:00 - 14:30, SW101

This short talk will discuss the development of a legacy device-driver in occam-pi for the RMoX operating-system. The driver developed is for a standard PC floppy-drive (SA-450 FDC), including basic support for interrupts and DMA (which the driver uses).
Garbage Collection for Servers via Sliding Views
Dr. Erez Petrank, Technion - Israel Institute of Technology (homepage)

Friday 1st April 2005, 11:00 - 12:00, S110B

With concurrent and garbage collected languages like Java and C# becoming popular, the need for a suitable non-intrusive, efficient, and concurrent multiprocessor garbage collector has become acute. Reference counting has traditionally been considered unsuitable for multi-processor systems. According to conventional wisdom, the update of pointers and reference counts required atomic or synchronized operations. In this work we show that this is not the case by presenting a novel reference-counting algorithm suitable for a multi-processor system that does not require any synchronized operation on a pointer modification (not even a compare-and-swap type of synchronization). Furthermore, the new collector eliminates a large fraction of the reference-count updates, thus, drastically reducing the reference-counting traditional overhead.
This garbage collector was implemented on the Jikes research JVM and comparisons against Jikes collectors will be presented. Measurements show extremely low pause times (around 1ms) and excellent throughput.
If time allows, we will discuss several directions of subsequent work building on the techniques developed in this basic work.
This is a joint work with Yossi Levanoni, and Harel Paz.

Navigation menu

School of Computing

Studying

Activities

Local users

About us

Search

School of Computing

Programming Languages and Systems: Seminars

Upcoming seminars

Past seminars