A Type-System for describing System-on-a-Chip Architectures – Jan De Muijnck-Hughes

Event details

  • When: 5th April 2018 12:00 - 13:00
  • Where: Cole 1.33a
  • Format: Talk


A Type-System for describing System-on-a-Chip Architectures



The protocols that describe the interactions between IP Cores on
System-on-a-Chip (SoC) architectures are well-documented. These
protocols described not only the structural properties of the physical
interfaces but also the behaviour of the emanating signals. However,
there is a disconnect between the design of SoC architectures, their
formal description, and the verification of their implementation in
known hardware description languages.

Within the Border Patrol project we are investigating how to capture
and reason about the structural and behavioural properties of SoC
architectures using state-of-the-art advances in programming language
research. Namely, we are investigating using dependent types and
session types to capture and reason about hardware communication.

In this talk I will discuss my work in designing a dependent type-
system and corresponding language that captures and reasons about the
topological structure of a System-on-a-Chip. This language provides
correct-by-construction guarantees over:

1. the physical structure of an interaction protocol;
1. the adherence of a component’s interface to a given protocol; and
1. the validity of the specified connections made between components. 

We provide these guarantees through the (ab)use of dependent types as
presented in Idris; and abuse of indexed monads to reason about
resource usage.

Given time I will give an account of how this language enables
reasoning about SoC behaviour when considered in conjunction with
Session Types.

Diderot: A Parallel Domain-Specific Language for Image Analysis and Visualization – John Reppy

Event details

  • When: 2nd April 2018 13:00 - 14:00
  • Where: Cole 1.33b
  • Format: Seminar

Diderot: A Parallel Domain-Specific Language for Image Analysis and Visualization

The analysis of structure in three-dimensional images is increasingly valuable for biomedical research and computational science. At the same time, the computational burden of processing images is increasing as devices produce images of higher resolution (e.g., typical CT scans have gone from 128^3 to roughly 512^3 resolutions). With the latest scanning technologies, it is also more common for the the values measured at each sample to be multi-dimensional rather than a single scalar, which further complicates implementing mathematically correct methods.

Diderot is a domain-specific language (DSL) for programming advanced 3D image visualization and analysis algorithms. These algorithms, such as volume rendering, fiber tractography, and particle systems, are naturally defined as computations over continuous tensor fields that are reconstructed from the discrete image data. Diderot combines a high-level mathematical programming notation based on tensor calculus with an abstract bulk-synchronous parallelism model. Diderot is designed to both enable rapid prototyping of new image analysis algorithms and high performance on a range of parallel platforms.

In this talk, I will give an overview of the design of Diderot and examples of its use. I will then describe aspects of its implementation with a focus on how we translate the notation of tensor calculus to efficient code. I will also briefly discuss the automated techniques we use to validate the correctness of the compilation process.

Diderot is joint work with Gordon Kindlmann, Charisee Chiw, Lamont Samuels, and Nick Seltzer.

John Reppy is a Professor of Computer Science and a Senior Fellow of the Computation Institute at the University of Chicago. He received his Ph.D. from Cornell University in 1992 and spent the first eleven years of his career at Bell Labs in Murray Hill NJ. He has been exploring issues in language design and implementation since the late 1980’s, with a focus on higher-order, typed, functional languages. His work includes the invention of Concurrent ML and work on combining object-oriented and functional language features. His current research is on high-level languages for parallel programming, including the Diderot, Manticore, and Nessie projects.

Compositional Coinduction with Sized Types – Dr. Andreas Abel

Event details

  • When: 16th February 2018 12:00 - 13:00
  • Where: Cole 1.33b
  • Format: Seminar


Formal languages and automata are taught to every computer science student.  However, the student will most likely not see the beautiful coalgebraic foundations, which use coindutive reasoning.

In this talk, I recapitulate how infinite tries can represent formal languages (sets of strings).  I explain Agda’s coinduction mechanism based on copatterns and sized types demonstrate that it allows an elegant representation of the usual language constructions like union, concatenation, and Kleene star, with the help of Brzozowski derivatives.

Simplifying ARM concurrency – Prof. Susmit Sarkar

Event details

  • When: 22nd February 2018 12:00 - 13:00
  • Where: Cole 1.33a
  • Format: Talk

ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits. In
particular, the model was originally non-multicopy-atomic: writes could
become visible to some other threads before becoming visible to all —
but this has not been exploited in production implementations, the
corresponding potential hardware optimisations are thought to have
insufficient benefits in the ARM context, and it gives rise to subtle
complications when combined with other ARMv8 features. The ARMv8
architecture has therefore been revised: it now has a multicopy-atomic
model. It has also been simplified in other respects, including more
straightforward notions of dependency, and the architecture now includes
a formal concurrency model.

This is work presented in POPL this year. I will also present some of
the background and context on relaxed memory which is absent from the
necessarily compressed talk format of POPL.

Dr. Vladimir Janjic – Efficient Dynamic Mapping of Parallel Applications to NUMA Architectures by Reinforcement Learning

Event details

  • When: 7th December 2017 12:00 - 12:00
  • Where: Honey 103 - GFB
  • Format: Talk

Title: Efficient Dynamic Mapping of Parallel Applications to NUMA Architectures by Reinforcement Learning


Abstract: We present a dynamic framework for mapping threads and data of parallel applications to computational cores/memory nodes of parallel non-uniform memory architecture (NUMA) systems. We use a feedback-based mechanism where the performance of each thread is collected and used to drive the reinforcement-learning policy of assigning affinities of threads/data to CPU cores/memory nodes. The proposed framework can address different optimisation criteria, such as maximum processing speed and minimum speed variance. We demonstrate that we can achieve an improvement of 12% in execution time compared to the default Linux operating system scheduling/mapping of threads under varying availability of resources (e.g. when multiple applications are running on the same system).

Bidirectional-Curious? – Dr. Conor McBride

Event details

  • When: 22nd November 2017 13:00 - 14:30
  • Where: Cole 1.33b
  • Format: Talk

Type systems are often presented in a declarative style, but with an emphasis on ensuring that there is some sort of type synthesis algorithm. Since Pierce and Turner’s “Local Type Inference” system, however, there has been a small but growing alternative: bidirectional typing, where types are synthesized for variables and elimination forms, but must always be proposed in advance for introduction forms and checked. You can still get away without any type annotations, as long as you write only normal forms. But where’s the fun in that? If you want to write terms that compute, you need to write type annotations at exactly the point where an introduction form collides with its elimination form, showing exactly the type at which computation is happening.

For type systems with some sorts of value dependency, the bidirectional approach seriously cuts down on the amount of annotation required in terms, needed only to achieve type synthesis. We have a real opportunity to reduce clutter and also to give a clearer account of the connections between types and computation.

But it doesn’t stop there. A disciplined approach to the construction of bidirectional type systems makes it easier to get their metatheory right. I’ll show this by reconstructing Martin-Löf’s 1971 type theory (the inconsistent one) in a bidirectional style and show why it has type
preservation, even without normalization.

PhD viva success: Adam Barwell

Congratulations to Adam Barwell, who successfully defended his thesis yesterday. Adam’s thesis was supervised by Professor Kevin Hammond. He is pictured with second supervisor Dr Christopher Brown, Internal examiner Dr Susmit Sarkar and external examiner Professor Susan Eisenbach from Imperial College, London.

Towards Refinement by Resolution in Dependent Type Theory – František Farka

Event details

  • When: 9th November 2017 12:00 - 13:00
  • Where: Cole 1.33b
  • Format: Talk

Dependent types are increasingly used in functional programming languages. The surface syntax of dependent types, as seen by a programmer, is elaborated by a compiler into an internal, type-theoretic representation. In order to perform this step, the compiler needs to infer a nontrivial amount of information to successfully type-check the internal representation. This process—type refinement—is complex, implementation dependent, and very few formal developments currently exist. We discuss a novel and simpler formalisation of type refinement in first order type theory with dependent types. We propose a translation of type-refinement problems to Horn-Clause logic with explicit proof-terms, using proof-relevant resolution as the type inference mechanism.